Formal Methods and Specification
You've shipped the bug that no test caught - the one that only happens when two requests land in the wrong order, or a node dies at the exact wrong millisecond. You couldn't have written a test for it because you didn't know the situation existed. That's the gap formal methods fill: instead of checking the code you wrote, you describe the design precisely enough that a tool can hunt down every situation it allows, including the ones you'd never think to test. The relief is real - teams catch fatal design bugs this way before a single line of code exists.
How to read this
- Want the mental shift first? Phase 1 reframes what a spec even is.
- Want to actually model something? Read in order - Phase 2 is states, transitions, and invariants; Phase 3 is checking the design and a gentle look at TLA+.
The phases
- The Blueprint, Not the Building - a spec describes what must be true, separate from the code; coding is to programming what typing is to writing.
- States, Transitions, and Invariants - model a system as states plus allowed moves, and pin down what must always (and eventually) hold.
- Checking the Design Before You Build - let a tool explore every reachable state, why that beats testing, and an on-ramp to TLA+.
This builds on reasoning from What Logic Actually Is, the always/there-exists machinery from Predicate Logic and Quantifiers, and the idea of a gap-free argument from What a Proof Is.