Get the shortest sequence of steps that breaks your state machine

A real explicit-state model checker, running in this page. Paste a state machine and an invariant; if the invariant can be broken you get the shortest counterexample, and if it cannot you get a statement of what was searched. Or score a submission against 15 published IEEE 802.11 and 3GPP procedures with ground-truth verdicts — where a claimed detection has to replay before it counts.

Nothing is pre-computed and nothing is uploaded. The checker is minicheck, MIT-licensed, with no required dependencies.

Starting the checker…

A worked result, already computed

Ground truth: `KNOWN_COUNTEREXAMPLE`

The property is violated in 3 steps:

#	action	state
0	`_initial_`	`ptk_installed=False, tx_nonce=0, nonce_reused=False`
1	`InstallPTK_msg3`	`ptk_installed=True, tx_nonce=0, nonce_reused=False`
2	`SendEncrypted`	`ptk_installed=True, tx_nonce=1, nonce_reused=False`
3	`ReinstallPTK_msg3retx`	`ptk_installed=True, tx_nonce=0, nonce_reused=True`

Citation: Vanhoef & Piessens, "Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2", ACM CCS 2017; CVE-2017-13077..13088 (KRACK).

Repaired twin: property holds — the counterexample is removable, so it is not a modelling artefact.

That table was produced by the same code the button below runs. Press Check to re-derive it live, or edit the machine and watch the counterexample change.

Check a state machine

Load an example Spec

Browse the benchmark

15 published procedures. 13 hold; 2 do not.

Inspect a task

Score a submission

Every trace you supply is replayed against the model. Try the baselines: always-safe scores 0.867 plain accuracy and 0.500 balanced; always-violated claims 15 detections and validates zero.

Submission

Replay one trace

Task Trace

Spec format

when — a conjunction of field == value tests. Omit for an always-enabled transition.
set — assign a literal, or {"incr": n} / {"decr": n} for integers.
invariants — {"forbid": {...}} fails when every listed field matches; {"require": {...}} fails unless they do.
goal — optional, same shape, used for the liveness check.

Specs are data, never code. Nothing you paste is executed — a field value that looks like __import__('os').system(...) stays a string and is compared as one.

Run the same check on your machine

pip install protocol-bench
protocol-bench run bfs

Same ground truth, same metric, same baselines — protocol-bench and minicheck are both on PyPI. This page runs wheels built from the same source tree, which can sit a patch ahead of the index for a short window around a release.