# 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. --- # 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](01-the-blueprint-not-the-building.md) 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 1. **[The Blueprint, Not the Building](01-the-blueprint-not-the-building.md)** - a spec describes *what must be true*, separate from the code; coding is to programming what typing is to writing. 2. **[States, Transitions, and Invariants](02-states-transitions-invariants.md)** - model a system as states plus allowed moves, and pin down what must always (and eventually) hold. 3. **[Checking the Design Before You Build](03-checking-before-you-build.md)** - 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](/guides/what-logic-actually-is), the > always/there-exists machinery from > [Predicate Logic and Quantifiers](/guides/predicate-logic-and-quantifiers), and the idea of > a gap-free argument from [What a Proof Is](/guides/what-a-proof-is). --- # The Blueprint, Not the Building Think about the last serious bug you chased. Odds are it wasn't a typo. The code did exactly what you wrote - the problem was that what you wrote was a faithful implementation of a design that was wrong. Two operations could interleave in an order nobody pictured. A retry could fire while the first attempt was still in flight. The logic was sound for the cases you imagined, and broken for one you didn't. Here's the uncomfortable part: no amount of careful coding would have saved you, because the mistake was made before any code existed. It was a flaw in the *idea*. And we almost never write the idea down precisely enough to inspect it. We jump from a fuzzy mental picture straight to implementation, and the implementation becomes the first and only place the design is ever stated in full. ## Coding is not programming There's a line from Leslie Lamport - the computer scientist behind a lot of this field - that reframes the whole thing: > Coding is to programming what typing is to writing. Sit with that. Writing isn't the act of pressing keys. The thinking - what you're going to say, how the argument holds together, where it could fall apart - happens before and around the typing. The typing is the easy, mechanical end. Yet in software we routinely call the typing "the work" and treat the thinking as something that happens informally, in our heads, in a Slack thread, in a whiteboard photo nobody looks at again. A **specification** is where the thinking gets written down. It describes *what the system must do* and *what must always be true of it* - independent of how the code accomplishes that. It's the blueprint. The code is the building. ## Why the blueprint is separate on purpose When you build a house, the architect's drawing is not a tiny house. It's a different kind of artifact, and that difference is the point. The drawing strips away brick and timber so you can reason about the thing that matters - does the load-bearing wall actually bear the load? - without constructing it first and finding out the expensive way. A spec does the same to software. It throws away everything about *how* (which language, which data structure, which loop) and keeps only *what*: the states the system can be in, the moves it's allowed to make, and the properties that must hold no matter what. Stripping the "how" isn't losing detail - it's removing the noise that hides design flaws. ```text THE BUILDING (code) THE BLUEPRINT (spec) ----------------------- -------------------------------- def transfer(a, b, amt): A money transfer never creates a.balance -= amt or destroys money: b.balance += amt total balance is unchanged # locks? retries? A transfer never leaves an # what if b is frozen? account below zero # what if this crashes # between the two lines? <- the spec asks: is this EVER violated, across all orderings and all failures? ``` *What just happened:* the code on the left is one concrete attempt. The spec on the right doesn't care how the transfer is implemented - it states the truths the implementation must respect, so you can ask whether *any* execution could break them, including a crash between the two lines. ## A spec is a blueprint; a test is evidence This is the distinction that makes the whole field click, so let's be precise about it. A **test** is evidence. It takes one specific scenario - these inputs, this order - runs it, and checks the result. A passing test tells you the system behaves correctly *for the case you thought to write*. That's genuinely valuable. But it's a sample. It says nothing about the cases you didn't imagine, and the bugs that hurt most are exactly the cases you didn't imagine. A **spec** is a blueprint. It describes the design as a whole, which means a tool can later examine *every* situation the design permits - not a sample, the complete space - and report any that violate your stated properties. (That's Phase 3.) Tests verify the building, one room at a time. The spec lets you check the blueprint before the building exists. > Neither replaces the other. You still write tests - they catch coding mistakes, the gap between > blueprint and building. The spec catches *design* mistakes, the ones tests structurally can't > reach because you never knew to look. ## This isn't only for rocket scientists The reputation of formal methods is "PhDs proving theorems about chips." Some of it is that. But the everyday version is much humbler and more useful: writing the design down in language precise enough that ambiguity has nowhere to hide. Real engineering teams - at companies running systems you use daily - have caught genuinely fatal bugs in distributed protocols *at the design stage*, before writing the code, because they specified first and let a tool poke holes in it. The bugs were the kind that surface once a year in production and corrupt data when they do. Found on a laptop in an afternoon instead. You don't need heavy machinery to start. The core skill is a way of *thinking* - model the system as states and moves, name what must stay true - and that's exactly what the next phase builds. ## For builders Next time you're about to implement something with real concurrency or failure modes, try this before opening your editor: write down, in plain prose, (1) the pieces of state your system has, (2) the events that can change it, and (3) the one or two things that must *never* stop being true. You've written a baby spec. Even in prose, the act of stating the invariant out loud catches design holes - because now you can ask "could this event break that rule?" for each pair, and that question is where the year-one bug lives. ```quiz [ { "q": "In Lamport's analogy, coding is to programming as typing is to what?", "choices": [ "Reading", "Writing", "Printing", "Editing" ], "answer": 1, "explain": "Coding is to programming what typing is to writing: the typing/coding is the mechanical end; the real thinking - the design - happens before and around it." }, { "q": "What is the core difference between a specification and a test?", "choices": [ "A spec runs faster than a test", "A test describes the whole design; a spec checks one scenario", "A spec describes what must always be true (a blueprint); a test checks one specific scenario (evidence)", "There is no real difference; they are two words for the same thing" ], "answer": 2, "explain": "A spec is a blueprint of the design - it lets you reason about every case. A test is evidence for one case you thought to write. They catch different kinds of bug." }, { "q": "Why can a design flaw escape even very careful coding?", "choices": [ "Because the flaw is in the idea itself, made before any code exists", "Because careful coders make more typos", "Because compilers introduce the bug", "Because tests are always wrong" ], "answer": 0, "explain": "If the design is wrong, faithfully implementing it produces a faithful copy of the wrong design. The mistake predates the code, so coding care can't catch it." } ] ``` --- # States, Transitions, and Invariants In Phase 1 we said a spec describes the design. Good - but "describe the design" is still vague. What, concretely, do you write down? This is the part that turns the idea into a craft, and the craft rests on a single model that's powerful enough to capture almost any system you'll build: **a system is a set of states and the moves allowed between them.** Get fluent in that, add two kinds of property on top, and you can specify real things. ## A system is states plus transitions A **state** is a complete snapshot of everything that matters at one moment - every variable, every flag, every value, frozen. A **transition** is an allowed move from one state to another, triggered by an event. That's the whole model. The system starts in some initial state, and at each step *some* enabled transition fires, carrying it to a new state. The set of all states the system can possibly reach, following the transition rules from the start, is its **reachable state space**. Everything the system can ever do is a path through that space. Take a turnstile - small, but it's a complete example. ```text States: LOCKED, UNLOCKED Transitions: LOCKED --coin--> UNLOCKED (paying unlocks it) UNLOCKED --push--> LOCKED (passing through re-locks it) LOCKED --push--> LOCKED (pushing without paying: nothing) UNLOCKED --coin--> UNLOCKED (paying twice: wasted coin, still open) Initial state: LOCKED ``` *What just happened:* we've fully specified a turnstile without any code. Two states, four transitions, one starting point. Notice the last two transitions - "push while locked" and "coin while unlocked" - loop back to the same state. We had to decide what those do, and writing the model *forced* the decision. That's the value: the model has no room for "we'll figure it out later." ```mermaid stateDiagram-v2 [*] --> LOCKED LOCKED --> UNLOCKED: coin UNLOCKED --> LOCKED: push LOCKED --> LOCKED: push UNLOCKED --> UNLOCKED: coin ``` The diagram and the text say the same thing. For a turnstile you can hold the whole picture in your head. For real systems - many variables, concurrent actors - you can't, and that's precisely why writing the states and transitions down beats keeping them in your head: the model is exhaustive where your imagination is selective. ## Invariants: what must ALWAYS be true A model tells you what the system *can* do. Now you say what it must *never* do. An **invariant** is a property that holds in every reachable state, no matter what path you took to get there. It's a statement with an implicit "for all states" in front of it - the *always* quantifier you met in [predicate logic](/guides/predicate-logic-and-quantifiers), aimed at the state space. Invariants are where you encode the things that, if ever violated, mean disaster: ```text Money transfer system - invariants (must hold in EVERY reachable state): INV1: sum of all account balances == constant (money is never created or destroyed) INV2: for every account a: a.balance >= 0 (no account ever goes negative) INV3: no account is both "frozen" and "processing a transfer" ``` *What just happened:* these three lines say more about correctness than a folder of tests. Each is a claim about *all* reachable states. INV1 in particular is the kind of thing a single mis-ordered operation can break, and stating it explicitly means a checker can later ask "is there any reachable state where the balances don't sum to the constant?" - and answer for *every* path at once. Invariants are also called **safety** properties, summed up as *"nothing bad ever happens."* They're the workhorses - most of the bugs you fear are invariant violations. ## Liveness: what must EVENTUALLY happen Safety alone has a loophole. A system that does *nothing at all* never violates a safety property - it never reaches a bad state because it never reaches any new state. A turnstile welded shut is perfectly "safe." That's clearly not what you want. So there's a second flavor of property. A **liveness** property says something good *eventually* happens - the *there-exists-a-future-moment* quantifier, over time instead of space. Summed up: *"something good eventually happens."* ```text SAFETY (always): "two threads never hold the lock at the same time" -> nothing bad ever happens LIVENESS (eventually): "a thread waiting for the lock eventually gets it" -> something good eventually happens ``` *What just happened:* the two properties guard against opposite failures. Safety stops the system from doing something wrong. Liveness stops it from doing nothing - from deadlocking, starving a waiter, or hanging forever. A correct design usually needs both: never do the bad thing (safety), *and* don't get permanently stuck (liveness). The classic trap is writing a clever locking scheme that's bulletproof on safety - two threads truly never collide - and discovering it can deadlock, where each waits on the other forever. Safety intact, liveness violated. You need to state both or you've only specified half of "correct." ## Putting it together A specification, then, is four things: ```text 1. STATE - the variables; what a snapshot contains 2. INIT - the allowed starting state(s) 3. TRANSITIONS - the moves: from a state, under what condition, to what next state 4. PROPERTIES - invariants (always) and liveness (eventually) that must hold ``` That's it. That's the shape of every spec you'll write, from a turnstile to a distributed consensus protocol. The protocol has more state and trickier transitions, but the skeleton is identical. Once a system is written in this form, it stops being a vague intention and becomes a precise object - one a tool can examine exhaustively, which is exactly where Phase 3 goes. ## For builders You already model state machines constantly; you mostly leave them implicit. An order is `pending -> paid -> shipped -> delivered`. A connection is `connecting -> open -> closed`. The bugs cluster at the transitions you forgot to think about - what happens on `cancel` while `shipped`? what's the move out of `connecting` on timeout? Drawing the states and *every* edge between them, then writing one invariant ("an order is never both refunded and shipped"), surfaces the missing transition before it becomes a 2am page. You don't need a tool to get most of this benefit - the discipline of being exhaustive is the win. ```quiz [ { "q": "What is a 'state' in this model of a system?", "choices": [ "A single line of source code", "A complete snapshot of everything that matters at one moment", "An error message", "The name of a transition" ], "answer": 1, "explain": "A state is a full snapshot - every relevant variable and flag frozen at one instant. Transitions move the system from one such snapshot to another." }, { "q": "An invariant is a property that...", "choices": [ "holds in every reachable state (always true)", "is true at the start but may later break", "eventually becomes true", "is checked only by running tests" ], "answer": 0, "explain": "An invariant (a safety property) must hold in every reachable state, no matter the path. It's an 'always' claim over the whole state space." }, { "q": "A locking scheme guarantees two threads never collide, but two threads can wait on each other forever. Which property does it violate?", "choices": [ "Safety - something bad happened", "Liveness - something good never eventually happens", "Neither; deadlock is fine", "Both safety and liveness equally" ], "answer": 1, "explain": "Never colliding is safety, and it holds. But a waiting thread never getting the lock is a liveness failure: the good thing (eventually acquiring it) never happens." } ] ``` --- # Checking the Design Before You Build So you've done the work of Phase 2: your system is written as states, transitions, and the invariants that must hold. Now comes the payoff that makes the whole effort worth it. Because the spec is precise and finite-shaped, a *tool* can do something you never could by hand - visit every single state the design can reach and check your invariant in each one. Not a sample. Every one. This is **model checking**, and the first time it hands you a bug you'd never have imagined, the value of "specify first" stops being theoretical. ## Why exhaustive beats clever When you reason about concurrency in your head, you trace a few orderings - the obvious one, maybe the nasty one a colleague mentioned - and conclude "looks fine." The trouble is the number of orderings explodes. Three operations across two threads already have more interleavings than you'll patiently enumerate, and the bug always lives in the interleaving you skipped because it seemed absurd. A model checker doesn't get bored and doesn't assume anything is absurd. It starts from your initial state and mechanically explores: ```text INIT / | \ each arrow = an allowed transition A B C each node = a reachable state /| | |\ D E F G H the checker visits ALL of them | | | ... X ... X = a state where an invariant is FALSE ``` *What just happened:* the checker walks the entire reachable graph from `INIT`, applying every enabled transition, and tests each invariant at every node. If it ever reaches a state like `X` where an invariant is false, it stops and shows you exactly how it got there. You didn't have to think of the path to `X` - that's the point. The machine found the case your imagination filtered out. ## The counterexample is the gift Here's the part engineers fall in love with. When a model checker finds a violated invariant, it doesn't merely say "failed." It hands you a **counterexample trace**: the precise sequence of transitions, step by step, from the start to the broken state. ```text INVARIANT VIOLATED: INV1 (total balance == constant) Counterexample trace: Step 0 INIT A=100 B=100 total=200 OK Step 1 A starts transfer of 50 to B A=50 B=100 total=150 <- money in flight Step 2 B reads its balance for ITS OWN transfer A=50 B=100 Step 3 first transfer completes A=50 B=150 total=200 OK so far... Step 4 B's transfer (based on stale read) completes A=50 B=120 total=170 <- INV1 BROKEN ``` *What just happened:* this is a textbook lost-update / race condition, and the checker reconstructed the exact interleaving that triggers it - a stale read in step 2 that the obvious mental model never considers. A counterexample is worth more than a red "FAIL," because it's a recipe: follow these steps and you reproduce the bug every time. It turns "something's wrong somewhere" into "here, line by line." This is the connection back to proof. In [what a proof is](/guides/what-a-proof-is) you saw that one counterexample disproves a universal claim. Your invariant *is* a universal claim - "in all reachable states, money is conserved." The model checker's job is to search for the single counterexample that disproves it. Find one, the design is broken. Find none after exhausting the space, and you have something close to a proof that the property holds for your model. ## A gentle look at TLA+ The most established tool for this is **TLA+** - Lamport's specification language - with its model checker **TLC**. You don't need to learn it today; the goal here is to recognize it and see that it's the same ideas you already have, written in a precise notation. A TLA+ spec is, almost literally, the four-part skeleton from Phase 2: variables, an initial-state predicate, a next-state relation (the transitions), and the properties. Stripped to its essence, a toy counter looks like this: ```text VARIABLES x \* the state Init == x = 0 \* allowed starting state Next == x' = x + 1 \* the transition: x' is x's next value Invariant == x >= 0 \* must hold in every reachable state ``` *What just happened:* `Init` says we start at zero. `Next` describes how the state changes - the prime mark `x'` means "the value of x in the next state," so this reads "next x is current x plus one." `Invariant` is the always-true property. Feed this to TLC and it explores the reachable states and confirms (or refutes) the invariant. It's the turnstile and the transfer system from Phase 2, in the notation a checker can run. > The lesson isn't the syntax - it's that TLA+ is nothing more than the states-transitions-invariants > mental model written down formally. If you understood Phase 2, you already understand what a TLA+ > spec *is*; learning the tool is learning where the brackets go. ## What checking can and can't promise Be clear-eyed about the boundaries, because overselling this is how people get burned. A model checker verifies your **model**, not your code. If your spec says transfers are atomic but your real code isn't, the checker happily blesses a design your implementation doesn't honor. The spec catches *design* bugs; you still need tests and reviews for the gap between blueprint and building. And exhaustive exploration has a ceiling. If the state space is astronomically large (or infinite), the checker can't visit all of it in finite time - you bound the model (say, "up to 4 accounts, up to 3 concurrent transfers") and check that. A clean run over a bounded model isn't a universal proof; it's overwhelming evidence within the bounds you chose. For full mathematical certainty you reach for theorem proving, which is heavier and rarer. For most engineers, bounded model checking is the sweet spot: a few hours of effort, design bugs found that would've cost a production incident. ## The whole arc, in one breath Step back and look at what you've assembled. A **spec is a blueprint, not the building** - you write down what must be true, separate from the code (Phase 1). You express that blueprint as **states, transitions, and properties** - invariants for *always*, liveness for *eventually* (Phase 2). Then a **model checker explores every reachable state** and hands you a counterexample the moment a property breaks, before any code exists (Phase 3). That's the loop real teams use to catch fatal bugs in distributed systems on a laptop, in an afternoon, instead of in production a year later. You don't have to formalize everything you ever build. But the next time you're designing something where order, concurrency, or failure can bite - the situations tests structurally can't cover - you now have a sharper move than "code it carefully and hope." Write the blueprint. Name what must always be true. Then check the design before you build it. ## For builders A pragmatic starting point: don't try to spec your whole service. Pick the one gnarly part - the distributed lock, the state machine with the tricky cancel path, the retry logic - and model only that. Write its states, its transitions, and the single invariant that would ruin your week if it broke. Even sketching it on paper sharpens the design; running it through TLC turns the sketch into a checked guarantee. Small, targeted specs of the scary 5% deliver almost all the value. ```quiz [ { "q": "What does a model checker do that hand-reasoning about concurrency cannot?", "choices": [ "It writes the implementation code for you", "It exhaustively visits every reachable state and checks your invariants in each one", "It guarantees your production code is bug-free", "It speeds up the running program" ], "answer": 1, "explain": "A model checker explores the entire reachable state space - including the interleavings you'd never think to trace - and tests each invariant at every state." }, { "q": "When a model checker finds a violated invariant, what is the most useful thing it gives you?", "choices": [ "A single 'FAILED' message", "A faster version of the spec", "A counterexample trace: the exact step-by-step path to the broken state", "A list of all passing tests" ], "answer": 2, "explain": "The counterexample trace is a reproduction recipe - the precise sequence of transitions that reaches the bad state, turning 'something's wrong' into a line-by-line path." }, { "q": "What is a real limitation of model checking a bounded spec?", "choices": [ "It checks the model, not your actual code, and only within the bounds you set", "It can never find any bugs", "It replaces the need for tests entirely", "It only works on programs written in TLA+" ], "answer": 0, "explain": "A checker verifies the design model, not the implementation, and a clean run over a bounded model is strong evidence within those bounds - not a universal proof. Tests still cover the code." } ] ```