The transition from mathematics to programming. Leslie Lamport's TLA+ as the bridge from formal reasoning to formal governance. Where axioms become code and specification becomes enforcement.
Everything before this module was mathematics. Everything after is software. This module is the bridge. Lamport's Specifying Systems (2002) showed that the same axiomatic method Euclid used to derive geometry can specify the correctness of concurrent systems. TLA+ doesn't test software — it specifies what correct behavior means, then exhaustively verifies that the specification holds.
Testing checks examples. Specification checks all possibilities. A test suite might verify that your system handles 10,000 cases correctly. A TLA+ specification verifies that every reachable state satisfies the invariant. This is the difference between confidence and certainty. For autonomous AI agents — where a single unchecked state could violate safety constraints — confidence is not sufficient.
SwiftVector inherits TLA+'s vocabulary directly. The mapping is not analogy — it is structural correspondence. What TLA+ calls a State, SwiftVector calls SessionState. What TLA+ calls an Invariant, SwiftVector calls Constraint.evaluate(). The jump from specification language to governance kernel is shorter than it appears.
Lamport's Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers is available as a free PDF from his website. 364 pages. 18 chapters. The intellectual foundation for why deterministic governance is not optional.
— Required readingSpecifying Systems is the pivotal module — where mathematics becomes governance. Interactive TLA+ specification exercises and model-checking walkthroughs are being designed.