Many state bugs appear only after a sequence of operations, such as write, checkpoint, crash, restart, replay. People write the sequences they can already imagine, which are the ones the code already handles. Stateful tests generate the sequences for you and shrink any failure to the shortest one that still breaks, which turns “the system sometimes loses state” into a bug report you can act on.
state bugs live in sequences
Take a real durability bug. A journal commits a pin in two writes: a rename, then a directory sync. Kill the process between them, reopen, and the journal must decide whether the pin committed. A unit test can call commit and recover separately, but the bug only appears when one interrupts the other. Single calls grow linearly; interleaved sequences grow much faster, and that is where systems fail.
A stateful test replaces one case per sequence with three pieces: a model of the operations the system supports, with crash and restart as operations too; a generator that draws sequences of those operations; and assertions that run after every step.
what hegel does
Hegel is the Rust-native stateful testing library the workspace uses. Each property-test case is a sequence of operations against the real system, drawn inside the test loop from a seeded generator. Because the seed is data, a failing sequence reproduces exactly, and the shrinker can reduce it to the smallest sequence that still fails.
Shrinking is what makes the result usable. “Somewhere in a 400-step random sequence the journal lost a pin” is a puzzle. “Rename, kill, recover, retry: pin applied twice” tells you where to look.
the vhalla ledger and Gobstopper vault
vhalla’s ledger tests show the pattern most clearly. recovery_hegel.rs drives the ledger through appends, checkpoints, snapshots, restores, and replay attempts, with every choice drawn inside the loop from the seeded generator. Sixty-four generated sequences run in milliseconds because the ledger is a pure core with no sockets, no wall clock, and no filesystem the test cannot control. That deterministic core, covered in its own lesson, keeps each run cheap, so Hegel can afford to explore many sequences.
Gobstopper’s vault surgery tests are the second case. Compaction, snapshot, and recovery are sequences over an on-disk vault, and the claims that matter (the source is preserved, a copy can be recovered, protected output survives) are properties of sequences. The tests inject a crash at different steps of the same surgery and check the postcondition each time.