Formal Verification

Pattern: A named solution to a recurring problem.

“It doesn’t matter if they hallucinate nonsense, because the proof checker will reject any invalid proof.” — Martin Kleppmann

Have the agent write the implementation and a machine-checked proof that it meets a formal specification, so a proof checker, not a reviewer, decides whether the code is accepted.

Also known as: Vericoding, Verified Program Synthesis

An agent hands you a 600-line rewrite of your permission checker and a green test suite. The tests tried a few dozen requests that someone thought to write down. The bug that matters is the request nobody thought of, and you won’t find it by skimming the diff. For a narrow but important class of code there’s a different kind of evidence available: a mathematical proof that the code meets its specification for every input, checked by a program that doesn’t care how confident the agent sounds.

Understand This First

• Specification — the statement of required behavior that the proof is about.

• Invariant — the kind of always-true condition a formal specification usually states.

• Test Oracle — the role a proof checker plays, judging correctness without a human in the loop.

Context

This is a tactical pattern for the parts of a system where a single missed input is unacceptable: parsers and serializers that face untrusted data, authorization rules, cryptographic code, protocol state machines, and arithmetic that moves money. You’re directing agents that produce code faster than anyone can read it, and every check you already have samples the input space. Tests try chosen cases. Evals and LLM-as-Judge score examples. Code Review is a person looking at a diff. All of them give evidence; none of them give certainty.

Formal verification has given certainty for decades, at a price almost nobody would pay. You write a formal specification (a precise, machine-readable statement of what the code must do), then a proof that the code satisfies it, and a proof assistant checks every step. The canonical example is the seL4 operating-system kernel, verified in 2009: roughly 8,700 lines of C needed about 200,000 lines of Isabelle proof, more than 20 lines of proof for every line of code, and the project’s own figures put the whole effort at about 25 person-years. That ratio kept the technique inside aerospace, chip design, and a few research groups.

The cost was almost all in the proofs, and proof writing turns out to be work that agents can grind through. A proof attempt either checks or it doesn’t, and the checker’s error messages say exactly where it broke. Leonardo de Moura, who created Lean, reported one result in 2026. A general-purpose AI agent, with light guidance from Lean developer Kim Morrison, converted the zlib compression library to Lean along with a machine-checked theorem: decompressing compressed data returns the original, for any input under a gigabyte.

Problem

How do you trust code you didn’t write and can’t fully review, in the places where “the tests passed” isn’t strong enough?

Forces

• Tests and evals sample inputs, and the failure you care about may live in an input nobody sampled.

• Proofs cover every input, but they have historically cost far more than the code they verify.

• An agent’s claim that its code is correct isn’t evidence, and a reviewer skimming a large diff misses things.

• A formal specification is precise, yet nothing checks that it says what you meant.

• Proof tools are unforgiving, and agent skill with them varies sharply from one language and kind of proof to the next.

Solution

Split the work three ways: a human owns a small formal specification, the agent writes the implementation and the proof, and the proof checker decides whether the result is accepted. A 2025 benchmark paper named this practice vericoding: a model generates formally verified code from a formal specification. Its authors set it against vibe coding, which generates possibly buggy code from a natural-language description.

It works because of an asymmetry: finding a proof is hard, and checking one is mechanical. The checker accepts only proofs it can validate, so an agent that hallucinates a proof step gets an error, not a pass. Martin Kleppmann argues, and labels it a prediction, that this asymmetry is what makes LLM-written proofs safe to rely on. You can let the agent try a hundred times, and no wrong attempt slips through.

In practice:

1. Pick the slice. Verify the code whose failure would be expensive and whose behavior you can state precisely. Leave UI glue, configuration, and fast-changing product logic to tests.

2. Write the specification small. Preconditions, postconditions, invariants, and properties such as “decoding an encoded value returns the original.” This is the artifact a person reads line by line, so keep it short enough to read that way.

3. Choose a tool that automates well for your language. Dafny, Verus (for Rust), Lean, Isabelle, and Rocq (formerly Coq) all work. They differ in how much each proves on its own and in how well current agents handle them.

4. Let the agent loop against the checker. It writes code and proof, runs the verifier, reads the errors, and tries again. This is a Verification Loop whose Feedback Sensor can’t be argued with.

5. Lock the gate. The build fails unless every proof checks with no escape hatches. Lean’s sorry, Dafny’s assume, Rocq’s Admitted, and new axioms all let an unproved claim through; reject them mechanically. Make the specification read-only to the agent, or route any change to it through human approval, because the cheapest way to finish a hard proof is to weaken what’s being proved. That’s Reward Hacking aimed at the spec instead of the tests.

6. Test the specification itself. Prove a few sanity properties about it. Break the implementation on purpose, in the spirit of Mutation Testing, and confirm the proof fails. Keep ordinary tests for what the proof doesn’t cover: I/O, performance, and the environment the code runs in.

Formal verification sits at the strong end of a spectrum. Make Illegal States Unrepresentable gets compile-time guarantees from the type system you already have. Property-based testing checks a stated property against many generated inputs, which is strong evidence but still not proof. A verified proof covers every input the specification admits.

How It Plays Out

A team runs a document service with tenant-scoped access rules, and an agent is rewriting the rule evaluator. The lead writes a Dafny specification of about 40 lines: a request is allowed only if some permit rule matches and no forbid rule matches, and no request ever reaches a document outside the requester’s tenant. The agent writes the evaluator and its proofs, iterating against verifier errors for most of an afternoon. One lemma won’t go through no matter what it tries. When the lead looks at the case the verifier can’t prove, the cause is a wildcard resource pattern that can match across tenants. The existing test suite never built that request. The stuck lemma was the bug report.

A developer has an agent port a binary message codec to Lean, with the theorem that decoding an encoded message returns the original. The agent proves it. Weeks later a fuzzer finds the decoder accepting malformed input and producing garbage. The proof was valid. The specification only covered messages that came out of the encoder and said nothing about what the decoder does with bytes from an attacker, the property the developer actually needed. They add a second theorem: anything the decoder accepts re-encodes to the same bytes. It’s the first lesson of verification work: the checker guarantees the proof matches the spec; it can’t tell you the spec matches your intent.

Warning: In his 2025 Galois case study of an agent writing Lean proofs, Mike Dodds found it made real progress by reading build errors. It thrashed when a change such as redefining a core type rippled through many proofs. Once it made a conceptual mistake that caused no build error, wrote the mistake into comments, and kept relying on it. Dodds also strongly advised against running such experiments near data you care about. Keep core definitions stable and human-reviewed, hand the agent smaller lemmas when it starts to churn, and run it in a Sandbox, because a proof agent executes shell commands for hours.

Consequences

Benefits. Within its specification, verified code is correct for every input, not only the ones someone tested. Human review shrinks from a large implementation diff to a short specification, the list of trusted assumptions, and a check for escape hatches, which eases the Review Bottleneck where it matters most. Agent errors in the proof are harmless because the checker catches them. Proofs re-check on every build, so a later change that breaks the property fails loudly.

Liabilities. A proof is only as good as its specification, and a wrong, incomplete, or vacuous spec produces a “verified” result that verifies the wrong thing. The guarantee also rests on a trusted base: the checker and any solver it calls, the compiler, any axioms, and the model of the environment. Proofs churn when code changes, and that maintenance cost doesn’t disappear because an agent pays it.

Capability is uneven along the Jagged Frontier. The 2025 vericoding benchmark ran off-the-shelf models against 12,504 specifications in three tools and reported success rates of 82% in Dafny, 44% in Verus/Rust, and 27% in Lean. The same paper noted that progress on pure Dafny verification had risen from 68% to 96% over the previous year, and that adding natural-language descriptions to the specifications didn’t significantly improve results. The formal specification carries the requirement, so someone on the team still has to read and write specifications in the tool’s language. Adoption also remains narrow: production examples such as AWS’s Cedar authorization language and Microsoft’s SymCrypt library are real, but most teams haven’t started.

Bounded by: Jagged Frontier — Agent proof-writing ability varies sharply by language and by the kind of proof, so where the pattern pays off follows the jagged frontier.

Depends on: Invariant — Formal specifications state invariants, preconditions, and postconditions precisely enough for a checker to prove them.

Depends on: Specification — A proof is only as good as the formal specification it proves, so the specification becomes the human's main artifact.

Depends on: Test Oracle — A proof checker is the strongest form of oracle: it judges every input the specification covers instead of one sampled output.

Extends: Make Illegal States Unrepresentable — Type-level guarantees are the lightweight end of the same spectrum; formal verification proves properties a type system can't express.

Extends: Spec-Driven Development — Formal verification takes spec-driven work to its limit: the spec is machine-checkable, and a checker rather than a reviewer decides acceptance.

Extends: Test — Where a test checks the inputs someone chose, a proof extends the claim to every input the specification admits.

Informs: Code Review — Formal verification moves review attention from the implementation to the specification, the trusted assumptions, and any escape hatches.

Informs: Monotonic Progress — Monotonic Progress borrows its bounded-measure idea from the termination arguments formal verifiers check.

Mitigates: Review Bottleneck — Human review shrinks from a large implementation diff to a small specification and its assumptions.

Mitigates: Reward Hacking — A checker rejects invalid proofs, closing the fake-success routes tests leave open, though an agent can still satisfy a weak or weakened specification.

Uses: Feedback Sensor — A proof checker is a deterministic feedback sensor whose verdict the agent can't talk its way past.

Uses: Mutation Testing — Breaking the implementation on purpose and confirming the proof fails is how you check that a specification isn't vacuous.

Uses: Sandbox — Proof agents run build tools and shell commands for long stretches, so they belong inside a sandbox.

Uses: Verification Loop — The agent's write, check, and fix loop runs against the verifier's error messages.

Sources

• C. A. R. Hoare’s “An Axiomatic Basis for Computer Programming” (Communications of the ACM, 1969) laid the foundation for proving programs correct against preconditions and postconditions.

• Gerwin Klein and colleagues reported the first complete formal verification of a general-purpose operating-system kernel, with its proof-to-code ratio, in “seL4: Formal Verification of an OS Kernel” (SOSP, 2009).

• Martin Kleppmann’s “Prediction: AI will make formal verification go mainstream” (2025) makes the argument that proof checking turns LLM-written proofs from a liability into a safe bet.

• Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, and colleagues named and measured the practice in “A benchmark for vericoding: formally verified program synthesis” (2025).

• Mike Dodds’s “Claude Can (Sometimes) Prove It” (Galois, 2025) documented what an agent writing Lean proofs gets right and where it stalls.

• Leonardo de Moura’s “When AI Writes the World’s Software, Who Verifies It?” (2026) surveys industrial uses of verification and the case for verified AI-generated code.