Model-check the algorithm you cannot test your way out of
For a small number of components where a subtle concurrency or fault-tolerance defect would be unrecoverable, writing a formal specification and exhaustively model-checking it finds design errors that review and testing demonstrably do not, at a training cost measured in weeks rather than months.
Do this firstWrite down decisions, with the reasoning and the alternatives
Not for your service. For the replication protocol, the lock manager, the thing whose failure mode is silent data loss discovered a month later.
The honest framing is one of scope. This is the most expensive control on the site and it applies to a vanishingly small fraction of the code most teams write. What makes it worth a page is that within that fraction it does something no other control here does: it examines every reachable state rather than the states someone thought to write a test for.
The decoy
More integration tests. They explore the state space by sampling it, and the defects this control targets are the ones whose shortest reproduction is dozens of steps deep — a region no sampling strategy will reach by accident.
Evidence
- How Amazon Web Services Uses Formal Methods — IIIModel checking found subtle concurrency and fault-tolerance defects in production distributed systems that had already passed design review, code review and testing — including a DynamoDB data-loss bug whose shortest counterexample was 35 steps. Engineers were reported productive in TLA+ within two to three weeks.
Last reviewed 2026-08-19.