Many concurrency bugs live in the order of events rather than in any one function: replica B answers before replica A finishes its write, a lock is released between the check and the use, or a crash lands between two writes that were meant to be atomic. A model checker for TLA+ finds these by trying every ordering of a small model of the protocol, which no test suite can do.
For the language itself, see Hillel Wayne’s Learn TLA+ and Leslie Lamport’s TLA+ page. This lesson covers where vhalla and Gobstopper use it and what a checked spec cannot tell you.
why tests miss ordering bugs
A concurrent system’s behavior depends on its code and on every allowed ordering of its steps. Tests exercise a few orderings, and production eventually exercises the bad ones. The number of orderings grows combinatorially: three actors with four steps each already have more interleavings than a test suite will ever run. Unit tests have no way to call “the scheduler,” so the ordering itself goes untested.
TLA+ and similar tools check a model of the system against all interleavings within a state limit you set. You write the protocol as a state machine: the state variables, the atomic steps, and the invariants that must hold in every reachable state. The model checker enumerates states until it has seen them all or found one that breaks an invariant.
what a spec models
A TLA+ spec is a protocol skeleton: which messages exist, which states a node can be in, and what a step may change. It is only as faithful as the writer’s choice of which details matter, and it is exhaustive over whatever it does model.
When the checker finds a violating state, it reports the step sequence that reached it: send, crash, retry, ack, in that order. A trace like that names the bug precisely enough to fix, and it becomes a regression test once you reproduce the interleaving in the real test harness and keep it in the suite.
where vhalla and Gobstopper use specs
vhalla keeps specifications for delivery and recovery, where ordering decides whether the product works. The private-agent delivery path has a relay, member acceptances, a durable journal, and a controller that can pause. The spec checks the claim “retention is not member acceptance” against every schedule the model allows. Mutant configurations run the same spec against deliberately wrong variants of the protocol to confirm it catches them; a spec that never fails a mutant has shown nothing.
Gobstopper keeps vault specifications for the same reason. The vault promises that a transcript copy preserves structure, that a snapshot can be recovered, and that a compaction does not drop protected recent output. Each promise is about a sequence of reads and writes, and the spec turns “recoverable” into a property of the operation order that the checker can test.