Formal Methods and Specification

Describe what a system must do, and why it is correct, before you build it: state machines, invariants, and specify-before-you-code.

1. The Blueprint, Not the Building A specification describes what a system must do and why it's correct, separate from the code that does it — the blueprint, not the building.
2. States, Transitions, and Invariants Model any system as states plus allowed transitions, then pin down what must always be true (invariants) and what must eventually happen (liveness).
3. Checking the Design Before You Build A model checker explores every reachable state of your spec and reports any that break an invariant — finding design bugs before code exists, with TLA+ as the on-ramp.