Four implementation phases, complete on the terms spec/06-architecture.md set
for each: the DSL and exhaustive safety checking; liveness with temporal
properties, fairness and symmetry reduction; Layer 1 invariants and the Layer 3
conformance bridge; and level-synchronous parallel exploration at 5.40x on 8
workers.

The acceptance criterion is not that the tests pass but D-9: the checker agrees
with TLC on every entry of the differential corpus -- die_hard,
two_phase_commit, distributed_lock, raft_election, bounded_buffer and paxos --
on distinct states, depth, where the search stops, every invariant, every
temporal property, and the shortest counterexample where one exists. Those
expected.json files are regenerated from TLC on every pipeline, so the column is
measured rather than asserted.

Pre-1.0 deliberately. The public surface may still move, and §Deferred is
written in terms of "past v1". This tag is a reference point, not a
compatibility promise.

Tagged at 04c1f443, whose own pipeline (#953) passed all seven jobs.