Before Amazon shipped a change to DynamoDB, the design had been through everything you are supposed to put a design through. Engineers had reviewed it. The code that implemented it had been reviewed too. It had tests, and the tests passed. By every process a serious team has, it was ready.
Then they ran the design through a model checker, and it found a bug. Not a typo — a sequence of thirty-five steps, a specific interleaving of operations and failures, that drove the system into a state it was never supposed to reach. Thirty-five steps. No reviewer traces thirty-five steps in their head. No test suite generates that particular sequence, because there is a combinatorial ocean of sequences and a test tries a handful of them. The bug was real, it was serious, and it was invisible to every method that had already signed off.
A Bug No Test Could Reach
The reason this keeps happening is that we test the wrong layer. A unit test checks a function. An integration test checks a path. Both of them check the code — and the code, line by line, was fine. The failure did not live in any single function. It lived in the design: in what happens when two operations arrive in an order nobody pictured, when a node dies at the precise moment between two writes, when the retry and the timeout and the partial failure line up just so.
These are the bugs that take down systems, and they share a property that makes testing nearly useless against them: they are not about whether a piece of code is correct, but about whether the interaction of correct pieces is. You can have a system where every component passes every test and the whole thing still deadlocks, loses data, or serves a stale read under a partition — because the bug is in the seams, and a test walks one path through the seams while the failure hides in a path it never walked.
You Model the Design, Not the Code
What Amazon used is a tool called TLA+, and the shift it represents is the whole point. You do not write a TLA+ specification of your code. You write a specification of your system's behavior — the states it can be in, the steps that move between them, the invariant that must never be violated no matter how the steps interleave. Then a model checker explores that state space exhaustively, the way a proof reasons about every input rather than sampling a few. It is not running your program. It is reasoning about your design, before the program exists.
The invariant is a single honest sentence about what must always be true — a committed write is never lost, two clients never both hold the lock — and the checker's job is to try, with mechanical patience, every way the world could conspire to make that sentence false. When it finds one, it hands you the thirty-five steps. When it cannot, you have something a test can never give you: a statement about all the interleavings, not the ones you imagined.
This is not an exotic practice anymore. In the account Amazon published, seven different teams had used TLA+, and all of them found it worth the effort — not to prove their code line by line, but to find the design-level defects that every other method had waved through.
AI Writes Code. It Does Not Write Designs.
Here is why this matters more now than it did when that DynamoDB bug was found. The current generation of coding agents is extraordinarily good at the layer testing already covered: they write functions, they pass tests, they generate plausible implementations at a rate no human can match. They are working, almost entirely, at the level of the code — the level where the line-by-line review already said yes.
They are far weaker, and structurally so, at the level where these bugs live. Asking what states a distributed system can reach under partial failure is not a code-completion problem. It is a question about a space too large to sample and too subtle to pattern-match, the same space the model checker walks exhaustively and the agent can only guess at. An agent will happily write the retry logic. It will not, on its own, tell you that the retry logic plus the timeout plus a node death at step nineteen violates the invariant you forgot to write down.
So the division of labor is becoming clear, and it is not the one the demos suggest. The implementation is increasingly the machine's. The design — the invariant, the claim about what must hold across every interleaving, the judgment about which failures are survivable — stays human. As the code gets cheaper to produce, the design is where the expensive thinking concentrates, and the place where "the AI wrote it and the tests passed" is the most dangerous sentence you can say.
The Tool Outlived Its Inventor's Tenure
There is a small piece of news that, read correctly, says a lot. Leslie Lamport, who created TLA+ and won a Turing Award for the body of work it sits in, retired in 2025. The project did not retire with him. It is now stewarded by the TLA+ Foundation under the Linux Foundation, with AWS, Microsoft, and Oracle among its founding members.
That is the signature of a technique graduating from one researcher's idea into shared infrastructure — the same arc that quietly happened to version control and to fuzzing. When the companies whose systems cannot fail put their names on the foundation, they are telling you where they think the unsurvivable bugs are. They are not testing their way out of the design layer. They are modeling it.
What I Don't Know Yet
Model checking proves the design. It does not prove that the code implements the design — that is a separate gap, and a real one. A flawless TLA+ specification sitting next to an implementation that quietly diverges from it is its own kind of false comfort: the map is correct and the territory wandered off.
What I genuinely don't know is whether agents make that gap better or worse. The optimistic story is that an AI which generates code from a checked design — rather than from a prose ticket — finally closes the distance between the model and the implementation, because the design becomes the prompt. The pessimistic story is that we get beautiful, checked designs and a flood of machine-written code that nobody traces back to them, and the gap between what we proved and what we shipped grows in the dark. I don't know which one we get. I know the deciding factor is not the tooling. It is whether anyone is still paid to hold the design and the code in one head and insist they are the same thing.
→ The companion argument, from the merge gate up: The Right to Merge.
→ See the full framework: The Decision Effectiveness Framework.