Anthropic published research on October 22, 2026 showing Claude writing machine-checked proofs that real open-source code cannot crash. Working with Theorem, the Frontier Red Team had Claude prove that 239 fuzz-test entry points across 123 libraries from Google’s OSS-Fuzz never crash on any input under 64 MB.
The opening line of Anthropic’s write-up sets the stakes: “Most software is riddled with bugs, which AI can now easily find and exploit.” Its answer is to prove the code instead of only testing it, at a scale that used to take years of expert work.
On this page · 7 sectionsOpen
Anthropic’s Frontier Red Team and Theorem had Claude prove that 239 fuzz-test entry points across 123 OSS-Fuzz libraries never crash on any input under 64 MB.
The proofs run on the compiled RISC-V machine code, total about 180 million lines of Rocq, and are checked by the Rocq proof kernel, so people do not review them line by line.
Trying to prove the code turned up hundreds of bugs, including an out-of-bounds write that only fires on a rare 20 MB input and a rediscovery of CVE-2026-56132 in libexpat.
Opus 5.5 proves half of a 36-task test set with about 40% fewer tokens than Opus 5, and agents sharing a workspace of proofs needed 17% fewer tokens.
The guarantee has edges: single-threaded static RISC-V binaries on Linux, AddressSanitizer crashes only, and only the entry points that were proved.
§ 01What Claude proved
The trick is the specification. Every fuzz test already defines a bug as any input that makes it crash. Claude turned each fuzz test into a statement about the compiled RISC-V code, that it never crashes for any input under 64 MB, and then wrote a proof of it.
| Measure | Figure |
|---|---|
| Fuzz entry points proved crash-free | 239 |
| OSS-Fuzz libraries covered | 123 |
| Input size covered | Every input under 64 MB |
| Level of the proof | Compiled RISC-V machine code |
| Total proof size | About 180 million lines of Rocq |
| Typical proof | About 600,000 lines |
| Median binary proved | 18,000 RISC-V instructions |
| Time taken | A few weeks |
Nobody reads 180 million lines of proof. Anthropic says “virtually none of it needs to be manually reviewed” because the Rocq proof checker confirms each proof meets its specification. What a developer has to trust shrinks to three things: the models of RISC-V and Linux processes, the exact theorem statements, and the checker itself.
§ 02Why this used to be impractical
Formal verification has worked for decades, but at a price only safety-critical code could pay. Anthropic’s example is seL4, an operating system kernel.
Proving the code took ten times longer than writing it. That ratio is why verification stayed in places like avionics. Claude covering 123 libraries in a few weeks is the change.
§ 03The bugs it found on the way
A proof attempt that fails tells you where the code can break. Claude was allowed to patch what it found, regenerate the specification and keep proving, so the effort turned up hundreds of bugs, many of which a fuzzer would rarely reach because fuzzers usually cap inputs at 1 MB.
| Where | Bug | Why a fuzzer misses it |
|---|---|---|
| A decompressor copy | Counter underflow leading to an out-of-bounds write | Needs an input of about 20 MB with one rare layout |
| An image decoder | Out-of-bounds read | Needs a 64 MB input and over 2 GB of memory |
| Another library | Out-of-bounds read | Needs a specific sequence of calls across two handles to one file |
| libexpat | CVE-2026-56132, rediscovered | Needs deeply nested input |
| A file-loading feature | Restriction not always enforced | A logic bug that never crashes |
The same methods worked outside fuzz tests. Claude wrote a formal spec of RFC 1950 and proved the Linux kernel’s zlib meets it, on the x86 binary. It built a Rust interpreter for a large subset of Python and proved it follows CPython semantics; across 1.7 million random programs it matched CPython in 99.95% of runs. On one widely used PDF reader, the team found as many security bugs in a week as are usually reported in a year.
§ 04What the proof does not cover
Anthropic is direct about the edges. The proofs assume a single-threaded, static RISC-V binary linked against musl, while most people run these libraries on x86 or ARM with glibc. AddressSanitizer does not catch every memory-safety bug, not every entry point of each library was proved, and a caller can still misuse a library correctly proved on its own.
The cost is the other limit: proofs can take hundreds of millions of tokens. Two numbers suggest that falls. On 36 small tasks built from OSS-Fuzz code, Opus 5.5 proves half with about 40% fewer tokens than Opus 5. Agents that could copy each other’s finished proofs needed 17% fewer tokens and cost less than a solo agent on 30 of the 34 proofs they completed.
§ 05What it means if you ship code
- Fuzz tests become specifications. If you already fuzz a library, that harness is the starting point for a proof.
- Proofs are reusable. Most of a proof covers code every C program shares, so each shared dependency only needs proving once.
- Anthropic is publishing a subset of the proofs plus the RISC-V and Linux semantics, and Theorem offers to run the pipeline on other open-source projects.
- Treat “formally verified” as a claim with a stated scope, and read the scope.
CellCog’s AI employees run on Claude Opus 5.5, the model in Anthropic’s token comparison. We had no part in this research.
§ 06Update log
- October 22, 2026: page opened from Anthropic’s research post, with an explainer scene of the proof loop.
§ 07Sources
- Anthropic Frontier Red Team, LLMs are making formal software verification feasible at a much larger scale, October 22, 2026.
- Google OSS-Fuzz, the continuous fuzzing program the libraries come from.
- The Rocq Prover, the proof assistant that checks the proofs.
- seL4, the verified kernel used as the cost reference.
Q1What is formal verification?
Translating code into a mathematical model and proving it always follows a stated rule. If the proof fails, the failure points at where a bug could be.
Q2Why use fuzz tests as the specification?
A fuzz test already says what counts as a bug: any input that crashes it. Proving it never crashes for any input under 64 MB makes running that fuzzer pointless.
Q3How long does this take?
The OSS-Fuzz effort ran over a few weeks. Anthropic says proofs can take hundreds of millions of tokens, which is the main cost limit today.
Q4Who is Theorem?
Anthropic’s collaborator on the project. It supplied the RISC-V and Linux process semantics and is offering to run the same pipeline for other open-source projects.
Q5Which model did the work?
Claude. Anthropic’s token comparison shows Opus 5.5 finishing proofs with about 40% fewer tokens than Opus 5 on its 36-task set.