A getting-started guide and an eleven-page tutorial, from an introduction on the
history and purpose of formal verification through the mathematics of TLA, the
DSL, invariants and deadlock, temporal properties, symmetry, Layers 1 and 3,
deriving a specification from a system, what to do when the state space explodes,
and putting a spec in a real project and keeping it true.

Every code block in a guide is compiled from the page itself, and every verdict a
page claims -- status, property, counterexample length, state count, never-enabled
actions, an unsound symmetry, a simulation finding -- is asserted by the test
suite, so a guide that drifts from the tool fails the build. The gate was built
first and a throwaway guide proved it went red, because nobody retrofits a gate to
prose that already passes. A second gate checks every internal link in the BUILT
documentation, which caught ExDoc's sidebar home link 404ing on all 84 generated
pages.

Two library changes travel with it, and they are why this is 0.2.0 rather than the
0.1.1 a documentation release would otherwise be. TLA.Spec.Deps records each
block's read and write variable sets at compile time -- the foundation
property-directed slicing needs, sound by widening rather than by narrowing.
TLA.Trace.validate/3 now requires a safety trace to refute the property it names,
a stricter contract than v0.1.0's and the check that would have caught #112.

Still pre-1.0 deliberately. The public surface may still move, and
spec/06-architecture.md §Deferred is written in terms of "past v1". Not published
to Hex -- that remains a separate decision.

Tagged at 578ff01f, whose own pipeline (#1158) passed all eight jobs.