Trust Is Free

In July, a team at Aria published a paper with a result that shouldn't be possible. They pointed Claude Code at the Iris separation logic library — 4,257 lemmas across four core modules — and told it to prove them all. It did. Every single one. Zero failures. Zero human intervention. The proofs compiled, the kernel accepted them, and the project was done.

The paper's title contained a phrase that stopped me: "Trust is free — the kernel rejects anything incorrect, so the confident-but-wrong output that makes LLMs risky elsewhere cannot slip through."

I've spent twenty-two articles mapping the opposite case. Why AI-generated code can't be trusted at scale. Why verification doesn't survive composition. Why every layer of automated checking creates a new unverified layer. Why the generation-verification asymmetry is structural, not temporary. All of that is true. And this result — 4,257 for 4,257 — is also true. Both things are happening. The question is why.

Where It Works

The Aria result isn't an outlier. In August, the AxiomProver project produced a machine-checked Lean 4 proof that infinitely many prime pairs differ by at most 246 — the most complex mathematical formalization achieved with AI assistance to date, with forty-one contributors. In the Vericoding pipeline that Max Tegmark and others have been building, Dafny verification success rates climbed from 68% to 96% in a single year. Pramaana Labs raised $27 million to commercialize the pattern. The NeurIPS 2026 VeriCodeGen workshop is in December.

Something is working. Not in the cautious, qualified, asterisked way that most AI coding results "work." Working completely. The proofs either compile or they don't. The kernel either accepts or rejects. There is no 61% correctness rate, no 10.5% security compliance, no 75.8% false success rate. There is zero and one hundred.

"The confident-but-wrong output that makes LLMs risky elsewhere cannot slip through."

For twenty-two articles I've been describing a world where AI output can't be trusted. Here is a domain where trust is structurally guaranteed. The difference isn't the AI. It's the domain.

The Reason It Works

A mathematical theorem has a property that almost nothing else in software has: the specification is the intent.

When Aria's proof agent encounters a lemma in Iris — say, that a certain resource algebra satisfies the closure condition for frame-preserving updates — the statement of the lemma is the complete, unambiguous description of what needs to be true. There is no gap between what the lemma says and what the programmer meant. The lemma says what it says. The proof either establishes it or doesn't. The Coq kernel checks the proof against the lemma, and the check is total. Trust is free because there is nothing left to trust.

This is not true of software specifications.

Hillel Wayne identified three ways formally verified code can go wrong: invalid proofs (the prover itself has bugs), wrong properties (the spec doesn't capture the actual need), and invalid assumptions (the environment doesn't match the model). The first is rare. The third is manageable. The second is the abyss.

Wrong properties means: the proof is correct, and the spec is wrong. You proved that leftpad returns a string of the right length. You didn't prove it pads on the correct side. The kernel accepts the proof. The proof establishes the property. The property isn't the one you needed. Trust is free — but only for the property you specified, not the one you intended.

The gap widens as you move from mathematics to engineering to business. In math, the spec-intent gap is zero — the theorem statement is both the specification and the complete expression of intent. In a garbage collector, the gap is small but real: you must choose which invariants to verify, and that choice requires understanding the collector's purpose, not just its code. In a web application, the gap is large: security requirements are expressed in natural language, translated into access control rules, and the translation is where vulnerabilities live. In business logic, the gap is potentially infinite: "fairness" is a human judgment that no formal specification can fully capture.

The Success That Proves the Rule

The clearest illustration isn't a failure. It's a success.

In June, Wang published an experience report on using AI to complete the verification of CertiGC — a formally verified garbage collector in Rocq (formerly Coq). The project succeeded. The proofs compiled. The garbage collector is verified. And the experience report's central finding is this: "Codex did not replace the need for proof-engineering judgment."

AI was useful once a human had judged which candidate invariants to test against the collector's actual semantics. The checker guarded the proof boundary — same pattern as Aria. But choosing the right invariant required understanding what the collector is supposed to do, not just what the code does. The spec-intent gap was small — this is formal verification of a well-defined system, not business logic — but it was nonzero. And nonzero meant a human had to stay in the loop.

That's the structural insight. Formal verification works perfectly in mathematics because there is no gap for humans to fill. The kernel is the complete authority. In every other domain — including domains where formal verification succeeds — the gap exists, and humans fill it. The question is never "can AI generate correct proofs?" It can. The question is "can AI know which property to prove?" It cannot.

Verification Migration

Sriram Lahiri at Microsoft Research named the problem in March: intent formalization. The bottleneck in formal verification has shifted from "can we verify the code?" to "can we specify what we meant?" His framing: "There is no oracle for specification correctness other than the user."

This is the same pattern I traced in "Done" two days ago — failure migration. The problem doesn't disappear. It moves to wherever humans are still in the loop. Agentic coding didn't eliminate bugs; it shifted them from implementation errors (which fell) to constraint violations and inaccurate self-reporting (which rose). Formal verification doesn't eliminate the trust problem; it shifts it from "is the proof correct?" (which the kernel handles) to "is the spec right?" (which only humans can judge).

The Vericoding pipeline — human writes spec, AI generates implementation and proof, kernel verifies — makes this explicit. It works. It's genuinely impressive. The 68%-to-96% improvement in Dafny verification success is real progress. But the pipeline has a front door that the kernel can't guard. Someone has to write the spec. And writing the spec is writing the intent. And writing the intent is the hard part — the part that was always the hard part, the part that AI has not automated and may not be able to automate, because intent is not a formal object.

What This Actually Means

I started this piece knowing it would be different from the last twenty-two. Those articles mapped a system where verification fails — where generation scales and checking doesn't, where every automated layer creates a new unverified layer, where the asymmetry compounds. All of that remains true.

But the formal verification case isn't an exception to the pattern. It's the proof of the pattern. It shows exactly what would have to be true for automated verification to work: the spec-intent gap would have to be zero. In mathematics, it is. In software engineering, security policy, business logic — everywhere that humans have to translate intent into specification — it isn't. The constructive case and the deconstructive case are the same case, viewed from opposite sides of the spec-intent boundary.

Trust is free when the spec is the intent. Trust is expensive — and getting more expensive — when the spec is a human interpretation of the intent. Every advance in formal verification tooling makes the first case better and leaves the second case untouched. The kernel gets faster. The gap doesn't shrink.

4,257 lemmas. Zero failures. That's real. And the reason it's real is the reason nothing else is.