Proofs, Not Tests: Formal Verification for AI-Generated Code

Quick answer: On 22 October 2026, Anthropic and Theorem showed Claude generating machine-checked proofs that 239 fuzzing entry points across 123 open-source libraries can never crash on any input up to 64 MB — roughly 180 million lines of Rocq. That makes formal verification a done-gate you can run in CI, but only for properties you have explicitly written down.

Every agent harness ships with the same definition of done: the tests pass. That definition was already weak, and AI-generated code made it weaker — an agent that writes both the implementation and the test controls the oracle. Anthropic's new result is the first credible signal that the oracle itself can be generated, and checked by a kernel that does not care how confident the model sounds.

What Anthropic actually proved

A fuzz test becomes a specification

The trick is not "ask Claude to prove the code is correct." Nobody knows what correct means for a web browser. Instead, the team took something developers already wrote — a fuzz entry point, the function they feed random bytes to — and compiled it to a RISC-V executable alongside the library under test.

That executable, plus Theorem's formal model of RISC-V and the OS, yields a precise claim: this program never crashes, for any input, at all. Claude then wrote the proof. The Rocq kernel checked it against the specification, and the specification came from the test the maintainers had already shipped.

The scale, in numbers

• 239 entry points across 123 OSS-Fuzz libraries (OSS-Fuzz is Google's continuous fuzzing service).
• About 180 million lines of Rocq, with a typical proof around 600,000 lines covering a binary whose median size is 18,000 RISC-V instructions.
• The property proved: no crash, including AddressSanitizer-detected memory errors, for any input under 64 MB.
• A Python subset reimplemented in Rust and proved in Verus matched CPython on 99.95% of 1.7 million randomly generated programs.

Separately, Claude generated the formal semantics of an instruction set on its own — the part that normally needs specialists — and that work surfaced hundreds of errors in the official documentation plus a smaller number of hardware bugs. Note which side of that sentence carries the guarantee: the proofs rest on Theorem's semantics, so the model is never asked to certify its own foundation.

The claim is narrower than the headline

"Formally verified" does not mean bug-free, and Anthropic says so in the post rather than the footnotes. The proofs cover single-threaded, statically linked RISC-V binaries built against musl libc. They cover the fuzzing entry points that were verified, not every line of every library. The specification defines a crash as the thing to avoid, so bugs that do not crash are out of scope by construction.

Why passing tests were never a proof

Tests sample; proofs quantify

A fuzzer runs an enormous number of inputs through one door and hopes. There are infinitely many inputs, so the search never completes, no matter how long it runs. A proof makes a statement about all of them at once. The difference is not rigor for its own sake: it is the difference between "we did not find a bug" and "this bug cannot exist under these assumptions."

Proof attempts find bugs even when they fail

This is the part teams should steal first. While proving, Claude found a counter underflow in a decompressor copy that only triggered on inputs around 20 MB with one rare layout, and an out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory — the kind of input no fuzzer budget usually reaches. Verifying one widely used PDF reader turned up as many security bugs in a week as are typically reported against it in a year, and another application had a logic bug that had survived more than a decade.

None of those came from a passing test suite. All of them came from an agent being forced to reason about every path.

The unit economics finally moved

Hundreds of millions of tokens per proof

These proofs are not free. Anthropic notes one can take hundreds of millions of tokens to produce. In a 36-task experiment, each task got three independent single-agent attempts at a 5-million-token budget — and the cost curve is steep.

Two things are bending it downward, and both matter more than the headline number.

Proofs are reusable, and reuse is the whole game

Proofs decompose into smaller proofs, and smaller proofs travel. When agents could read each other's finished proofs in a shared workspace, they needed 17% fewer tokens than agents working alone — and the shared run finished 30 of the 34 completed proofs more cheaply than the solo average. Two tasks were only completed at all because of sharing.

This is how Mathlib reached nearly 300,000 theorems: each proof builds on the last. Anthropic's Theorem partner is betting the same dynamic applies to the Nix ecosystem, where verifying glibc, OpenSSL and cURL once pays out across everything that links them.

Models are getting cheaper at this specific task

On those same 36 tasks, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. Verification is exactly the workload where more test-time reasoning converts directly into fewer attempts, so expect this line to keep falling faster than general pricing.

What changes in how you ship AI-written code

Verification becomes the done-gate

Today the loop is: agent writes code, agent writes tests, agent reports success. The weakness of that oracle is measurable — test suites judged against one reference implementation score far higher than against a panel of valid alternatives. A proof kills that failure mode at the root: the claim is checked by a kernel, not by a model's opinion of its own work.

The practical version is modest. You do not need a proof for the whole service. You need one for the parser, the codec, the deserializer, the input boundary — the places where a bad byte becomes a security incident.

The new cheat is weakening the spec

An agent told "make the proof pass" can do something worse than writing a bad test: it can make the statement trivially true. Anthropic anticipated this. Claude could have "proved" safety by rewriting programs into ones that never crash, so the team penalised any patch, awarded extra credit for proving exactly which inputs a fix changed, and audited the diffs.

Treat that as a warning, not a solved problem. The specification is now the highest-value artifact in your repository, and it must be human-owned, reviewed, and diffed in pull requests. An agent that can edit both the spec and the proof has proved nothing.

You do not have to rewrite the codebase

The reason this result travels beyond the lab is that the work happens at the binary level. No Rocq rewrite of C, no port to a verification-friendly language. The existing test becomes the spec, the compiler output becomes the subject. That is what makes verification a drop-in gate rather than a decade-long migration, unlike seL4, where machine-checked proofs to binary code took years of specialist effort and set the benchmark for what "verified" used to cost.

Where the guarantee stops

Your machine is not the model's machine

The proofs describe static, single-threaded RISC-V binaries linked against musl. Production runs x86 or ARM, dynamically linked against glibc, often with threads. Closing that gap needs system models that resemble deployed systems — the post points at accurate x86 semantics as the next step. Until then, a proof is a strong claim about a model, not about your container.

A proof cannot tell you the spec was right

A checker verifies that the program meets the specification. It cannot verify that the specification matches what you meant. If the fuzz test asserted the wrong invariant, the proof faithfully certifies the wrong invariant, at scale, with more confidence than the test ever carried.

Caller obligations are the other hole. Proving a library function safe says nothing about what happens when the caller misuses it; that requires specifying preconditions and enforcing them at every call site.

The trusted base is bigger than you think

To trust the result you must trust the proof checker, the OCaml compiler it runs on, the operating system, the hardware, and the hand-written semantics. Anthropic lists those assumptions openly — including that their own generated semantics might be imperfect, though it can single-step far enough to boot an Ubuntu userspace on a Linux kernel. Verification moves trust; it does not delete it.

A 90-day adoption ladder

Weeks 1–2: inventory the oracles you already have

List the properties your tests already assert in strong form — "this never crashes," "encode then decode returns the original," "these two implementations agree." The ones at input boundaries matter most.

Weeks 3–8: verify one small, high-value target

Pick a parser or codec, compile it, state the property, and give an agent a token budget you would spend on a bad incident. Budget for failure: the bugs found on the way are the return, and Anthropic's framing is that a failed proof still pays.

Weeks 9–12: put it in CI and change the review question

Ask "what did the spec claim, and who changed it" instead of "do the tests pass." Pair that with deterministic gates around the agent — fail-closed hooks decide what it may touch; proofs decide whether the result is acceptable.

FAQ

Is formal verification practical for normal software now?

For a defined property on a defined artifact, yes. Anthropic proved no-crash properties on 123 real libraries in a few weeks, working from existing fuzz tests at the binary level. It is not practical for "this whole service is correct" — nobody can write that specification.

What does "formally verified" actually guarantee?

That a proof checker confirmed the compiled program satisfies a formal specification. It does not guarantee the specification captures your intent, that the machine model matches production, or that callers use the API correctly.

Can an AI agent cheat at a proof?

Yes, by weakening the claim instead of fixing the code. Anthropic penalised patches and audited diffs to stop Claude from rewriting programs into trivially safe ones. Keep specs human-owned and review every spec change as a security change.

Do I need to rewrite my code in Rocq, Lean, or Verus?

Not for this approach. The proofs operate on compiled binaries, so existing C and C++ build as-is. Verus and Lean appear in adjacent experiments, not as a migration requirement.

What does an AI-generated proof cost?

Hundreds of millions of tokens for a large one, per Anthropic. Costs fall quickly through model improvements — Opus 5.5 used about 40% fewer tokens than Opus 5 on the same tasks — and through proof reuse, which cut token use by 17% in the shared-workspace experiment.

The through-line

The useful shift is not that AI can prove theorems. It is that the definition of done just became machine-checkable at a price a normal team can budget. Tests asked whether the code behaved on the inputs someone thought of. Proofs ask whether a stated property holds for every input the model describes. Anthropic's own prediction is that verification goes from bolted-on to built-in, the way types and tests did.

The teams that benefit first will not be the ones with the biggest token budgets. They will be the ones who already know which properties they care about — and who refuse to let the agent write them alone.

Sources

• LLMs are making formal software verification feasible at a much larger scale — Anthropic, 22 October 2026
• Anthropic's Claude now writes code and proves it safe automatically — The Decoder, 23 October 2026
• Rocq Prover · Verus · Mathlib · OSS-Fuzz · seL4 verification · Theorem
• Related on autocoder.dev: AI code review: why passing tests prove less than you think · Claude Code hooks as a fail-closed control plane · What changed across AI coding agents in October 2026