An agent opens a pull request at 2 a.m. The diff is clean. The description is well written. Every test is green — the ones that were already there, plus four new ones it wrote itself. CI is a wall of checkmarks.
Do you let it merge?
A year ago that question was hypothetical. Now it is a Tuesday. The code is plausible, the tests pass, and the only thing standing between the diff and production is your judgment about whether plausible-and-passing is the same as correct. For most of the history of software, we have quietly agreed that it is close enough. The agents are about to make that agreement very expensive.
The Green Check Is a Sample
A passing test is a statement about the inputs you thought to try. It says nothing about the ones you didn't. That is not a flaw in your testing; it is the nature of testing. Dijkstra said it in 1970 and it has not stopped being true: testing shows the presence of bugs, never their absence.
The canonical proof of this is embarrassing. The standard way to find the midpoint of a binary search — (low + high) / 2 — overflows when the array is large enough that low + high exceeds the maximum integer. The bug sat in print in Programming Pearls for two decades and shipped in the Java standard library, where Joshua Bloch eventually wrote it up under the title "Nearly All Binary Searches and Mergesorts Are Broken." Every test passed the entire time, because no test used an array of two billion elements. A proof would have caught it in seconds, because a proof does not sample — it reasons about every input at once. As Leonardo de Moura, who co-created the Z3 solver beneath most of these tools and went on to build the Lean prover, puts it: testing provides confidence; proof provides a guarantee.
The difference between confidence and a guarantee did not matter much when a human wrote the binary search, because a human wrote one binary search a year and felt the weight of it. It matters enormously when an agent writes forty of them before lunch.
Why Proof Lost the First Time
Here is the part the excitement skips. Proof is not new. We have been able to verify code since Hoare logic in 1969. The tools have been usable for a long time. And the overwhelming majority of competent engineering teams have looked at formal verification and rationally declined.
They were not lazy or ignorant. They were doing the math. To prove a program correct, you first have to say what correct means — precisely, formally, in a specification a machine can check against. For most software, writing that specification costs more than the bug it would prevent. A CRUD endpoint that occasionally returns the wrong sort order is annoying; proving it never does is a research project. The cost of the spec exceeded the cost of the bug, so testing won, and it deserved to.
This is why I am wary of the current wave of "formal verification is about to go mainstream." Martin Kleppmann made that prediction in late 2025 and it traveled, because he is right about the mechanism: AI can write the proofs now, and a proof checker rejects a hallucinated proof the way it rejects a hallucinated theorem — it simply does not typecheck. De Moura, from inside the field, has made the same argument. They are both correct, and I want to agree quickly and then say the thing they leave out.
If you stop at "AI makes proof cheap, so prove everything," you have made the same category error the field made for fifty years, just from the other direction. The question was never whether proof is good. It is which code is worth the spec.
The Price of the Proof, Not the Value of It
What AI actually changes is one term in the old equation. It collapses the cost of writing the proof — the mechanical, grinding part, discharging obligations to a solver. It does almost nothing to the cost of writing the specification, because the specification is the part where you decide what you actually mean, and meaning is not a thing you can sample your way into.
So the decision moves. It used to be "is this whole system worth verifying?" — and the answer was almost always no. Now it is "which parts of this system are worth a spec?" — and the answer is no longer nothing. When the proof is nearly free and the spec is the only real cost, you stop asking whether you can afford to verify and start asking where verification earns its keep.
That is a triage question, and it has a good answer.
Verify the Five Percent
You do not prove your codebase. You prove the five percent where a silent bug is not annoying but catastrophic, and where "we tested it" is not a sentence you want to say in the post-mortem. In my experience that five percent is unglamorous and easy to name:
- the authorization check that decides who sees what,
- the arithmetic that moves money,
- the concurrency and ordering that survive a partial failure,
- the data migration that runs once and cannot be un-run.
For that slice, a test is the wrong gate, because the failure you care about is exactly the input no one wrote a test for. For that slice, the gate should be a proof — a statement that this property holds for every input, checked by a machine, against a specification a human wrote on purpose.
A contract is the smallest version of this. It is a spec the compiler enforces:
method Withdraw(balance: nat, amount: nat) returns (newBalance: nat)
requires amount <= balance // you may not overdraw
ensures newBalance == balance - amount
{
newBalance := balance - amount; // checked against the spec, for every input
}
The requires and ensures are not comments. They are the property, and the verifier will not let the method compile unless it holds on every input — including the ones your tests would never have generated. That is what it means for code to carry its own proof. (You can watch a verifier catch a bug a passing test misses, on a real binary search, in the companion lab.)
The Right to Merge
So here is the gate I think we are walking toward, whether we plan it or not. An autonomous agent earns the right to merge into the five percent not by turning CI green — it can always turn CI green — but by producing a proof that the property you specified still holds. Tests pass becomes proof holds. The checkmark stops being a sample and starts being a guarantee.
Notice what that does to the human in the loop. It does not remove them. It moves all of their judgment into one place: the specification. The agent writes the code. The agent, increasingly, writes the proof. What it cannot write — what no amount of sampling produces — is the decision about what "correct" was supposed to mean in the first place. Verification does not take the human out of software. It relocates the human to the one position that was always the real job and was always the easiest to skip: saying, precisely, what you actually want to be true.
What I Don't Know Yet
The clean version of this story ends with the spec as the new merge gate and the human as its author. The honest version has a hole in it, and it is the same hole that has always been there.
A proof guarantees the code matches the spec. It guarantees nothing about whether the spec matches what you meant. A wrong specification, perfectly proven, is a wrong program with a certificate of correctness stapled to it — and that is a more dangerous object than an untested one, because it looks finished. When the agent writes the code and the agent writes the proof, the spec is the last thing a human still has to own. So who audits the spec? And when the agent starts proposing the specification too — confidently, plausibly, in well-written prose — what is the gate on that?
I don't have a gate for it yet. I suspect it is not a tool. I suspect it is taste, and accountability, and a person willing to say "that is not what I meant" — which are exactly the things we have spent every prior wave of automation discovering we could not delegate. Proof moves the judgment. It does not abolish it. The right to merge still ends, somewhere, with a human who has to mean it.
→ Watch a proof catch what a test misses: Does It Actually Hold?
→ See the full framework: The Decision Effectiveness Framework.