The nastiest concurrency bugs are not in any function. They are in an order of events: replica B answers before replica A finishes its write; the lock is released between check and use; a crash lands between the two writes that were supposed to be atomic. Unit tests cannot find these because no test calls "the scheduler." The interleaving is the bug.
the order problem
A distributed or concurrent system's behavior is the product of the code and every admissible ordering of its steps. Tests exercise a few orderings at random; adversarial reality exercises the bad ones. The space of interleavings grows combinatorially: three actors with four steps each already outnumber what any test suite will ever run.
TLA+ and tools like it answer by checking a model of the system against all interleavings a state bound permits. 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 then enumerates states until it has seen them all or found one that violates the invariant.
what a spec is
A TLA+ spec is deliberately not the code. It is a protocol skeleton: which messages exist, which states a node can be in, what a step may change. Its fidelity comes from the writer's honesty about which details matter; its power comes from exhaustive enumeration over the space it does model.
The yield is counterexample traces. When the checker finds a violating state, it reports the exact step sequence that reached it: send, crash, retry, ack, in that order. Those traces are gold for two reasons. They name a bug class precisely enough to fix, and they become the regression tests that prove the fix: reproduce the interleaving in the real harness, then keep it in the suite.
how the projects use it
vhalla keeps specifications for the pieces where ordering is the product: delivery and recovery. The private-agent delivery path has a relay, member acceptances, a durable journal, and a controller that can pause; the spec is where the claim "retention is not member acceptance" gets checked against every schedule the model allows. Mutant configurations run the same spec against deliberately wrong variants to confirm the spec can actually catch them: a spec that never fails a mutant is a spec that proves nothing.
Gobstopper keeps vault specifications for the same reason. The vault's promises (a transcript copy preserves structure; a snapshot can be recovered; a compaction does not drop protected recent output) are claims about sequences of reads and writes, not about one call. The spec level is where "recoverable" stops being a word and becomes a checkable property of the operation order.