Exploring the Multiverse
You have written your specification in PlusCal/TLA+, describing how your system should behave. How does that actually find bugs?
You use a tool called the TLC Model Checker, which ships with the TLA+ Toolbox.
TLC takes your specification and systematically plays out every possible scenario. It works like this:
- It starts at your defined Initial State.
- It computes every possible action that could legally happen next (according to your
Nextformula). - It generates all resulting new states and adds them to a queue.
- It repeats this process from each new state, building a massive directed graph of every state your system could ever reach.
- At every state it visits, it checks all your invariants.
This process is called state space exploration or model checking. It is exhaustive — TLC will find every reachable state, no matter how unlikely the sequence of events required to reach it.
Checking Invariants
While exploring, TLC checks Invariants — rules you declare must be true in every reachable state.
For a bank transfer system, you might declare:
Invariant == balance >= 0
This tells TLC: "No matter what sequence of actions occurs, the balance must never go below zero."
If TLC finds a sequence of 50 complex, concurrent steps that ends in a state where balance = -50, it immediately stops and reports an ERROR. Crucially, it prints the exact counterexample trace — the precise sequence of steps, in order, that reproduces the bug. This is enormously valuable: you get a minimal reproduction case for a bug that might only occur once in a billion real executions.
Liveness Properties
Beyond invariants (which are safety properties — "nothing bad ever happens"), TLA+ also supports liveness properties — "something good eventually happens."
For example: "Every transfer request is eventually either committed or rejected." A system that simply freezes and never responds satisfies all safety invariants (it never does anything wrong) but violates liveness. TLC can check both.
The Scalability Limit
TLC's exhaustive approach has a fundamental limitation: state space explosion. As the number of concurrent processes and variables grows, the number of reachable states can grow exponentially. A specification with 5 processes and 10 variables might have billions of states — too many to check exhaustively on a laptop.
Engineers manage this through:
- Symmetry reduction: Treating processes as interchangeable where appropriate.
- Constraint-based bounds: Limiting variable ranges during model checking (e.g., checking with balances 0–10 instead of 0–1,000,000).
- Abstraction: Simplifying parts of the system that are not the focus of the current verification.
The key insight is that bugs in distributed systems almost always manifest with small numbers of processes and steps. If TLC finds no bugs with 3 processes and values bounded to a small range, you have strong evidence (though not a mathematical proof) that the design is correct.
A common interview question is: "What are the limitations of formal verification? Why don't all teams use it?" The honest answer has two parts. First, state space explosion means model checking does not scale to arbitrarily large systems without abstraction. Second, and more importantly, the specification is not the implementation — TLA+ proves your design is correct, but your implementation in Go or Java might still have bugs that deviate from the spec. Formal verification eliminates design-level bugs; it does not replace testing of the implementation.