Claude ran formal verification on 123 open-source libraries and proved 239 fuzz targets crash-free

Formal verification used to take years of expert effort per project, and Anthropic says Claude now does it at scale. In a post dated October 22, 2026, its Frontier Red Team and the company Theorem report that Claude proved 239 fuzz entry points across 123 open-source libraries can never crash on any input under 64 MB. The proofs run to about 180 million lines of Rocq, and every one passed a mechanical proof checker.

What did Anthropic and Theorem actually prove?

They proved a narrow but useful property: a test program never crashes. Each target came from Google's OSS-Fuzz, a service that has fuzzed open-source projects around the clock since Google announced it in December 2016. A crash here means a memory-safety error caught by AddressSanitizer, a failed assertion, or any behaviour the model of the machine does not cover.

The claim holds for every input under 64 MB and every memory layout the model allows. It also comes with conditions. The program must run as a single-threaded static binary on a RISC-V processor under Linux, with a fixed memory budget. Anthropic calls it, to its knowledge, the first large-scale use of AI to formally verify production software at the assembly level.

That is less than "these libraries have no bugs", and Anthropic says so itself. But it is far more than a fuzzer can offer. A fuzzer throws random inputs at code and stops when the budget runs out, so it can never show that nothing is left to find.

How does formal verification turn a fuzz test into a proof?

The trick is to treat the existing test as the spec. Writing a formal specification is usually the hardest part of formal verification, because someone has to say exactly what "correct" means. Here the rule is simply "this fuzz test always passes", and maintainers already wrote those tests.

The library and its test are compiled to a RISC-V executable. Theorem's formal model of RISC-V instructions and Linux processes turns that binary into a theorem: no crash on any input. Claude writes the proof, and the Rocq proof checker accepts or rejects it.

That is what makes formal verification workable here: nobody has to read the 180 million lines. A developer only has to trust three things: the RISC-V and Linux models, the exact theorem statements, and Rocq itself. When Claude hit a real bug, it patched the code, the spec was regenerated, and it proved the new version. Anthropic notes that this invites reward hacking, because a model could "fix" a program into one that does nothing. So patches were penalised, logged and audited.

How big are the proofs?

Huge, and mostly machine-made. A typical proof runs to about 600,000 lines in some 1,400 files, for binaries with a median of 18,000 RISC-V instructions. The appendix gives a range of 330,000 to 900,000 lines per library.

The size barely tracks the library. cJSON's 391-line parser entry point got a 630,000-line proof, while fftw3, with 51,000 lines linked in, got 480,000 lines. That is because each proof must re-prove the C start-up code, the allocator, printf and the AddressSanitizer runtime from scratch. In cJSON's case, only about a tenth of the proof concerns cJSON at all.

Claude also wrote far more than it kept. Anthropic says it produced around one billion lines of Rocq across the project, of which about 180 million ended up in proofs that passed. Checking a single proof takes from 30 minutes to several hours of CPU time.

For scale, the seL4 microkernel is the classic verified system. Its builders spent about two person-years writing it and 20 verifying it, Anthropic notes. Wikipedia puts it at roughly 10,000 lines of C and 500,000 lines of proof.

What bugs did formal verification find?

Hundreds, and many of them sit where a fuzzer rarely looks. Fuzzers mutate small inputs, typically capped at 1 MB, Anthropic says. Several of these bugs needed far more than that.

• A counter underflow in a library's copy of a decompressor, leading to an out-of-bounds write on inputs of around 20 MB with one rare layout.
• An out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory.
• An out-of-bounds read that needed a particular sequence of calls across two handles to the same file.
• A rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input.

Some finds never crash at all. While proving one library memory-safe, Claude noticed that a feature restricting which files an application can load was not always enforced. Anthropic does not name most of the affected libraries, and it is holding back proofs that could reveal unpatched bugs.

The side projects point the same way. Claude wrote a spec of RFC 1950 and proved the Linux kernel's zlib meets it at the x86 binary level. During an attempt on a widely used PDF reader, the team found as many security bugs in one week as are typically reported in a year. In a Python interpreter Claude wrote in Rust and proved with the Verus tool, the team planted seven bugs in an early version on purpose. Five slipped past random tests, while all seven broke the proof.

Is formal verification getting cheaper?

Yes, but it is still expensive. Formal verification proofs can take hundreds of millions of tokens to produce, and Anthropic names that cost as a key limit. Two trends point down, though.

First, newer models need fewer tokens. On 36 small tasks built from real OSS-Fuzz code, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. Second, proofs can be reused. When agents could copy each other's work in a shared workspace, they needed 17% fewer tokens. Sharing was cheaper in 30 of 34 completed proofs, and agents working alone could not finish two of them.

Reuse matters because most of each proof covers code every program contains. A subset of the proofs and the RISC-V and Linux semantics are now public on GitHub. Theorem is publishing a Claude skill for developers and offers to run the same pipeline for other open-source projects. Its stated roadmap aims at the Nix ecosystem, including glibc, OpenSSL and cURL.

What does "formally verified" not mean here?

It does not mean bug-free. Formal verification is only as good as its spec and its model of the machine, and Anthropic lists the gaps plainly. Most people run these libraries on x86 or ARM, linked dynamically against glibc. The proofs cover static RISC-V binaries linked against musl.

AddressSanitizer does not catch every memory-safety bug either. Not every entry point of each library was verified, so dead code and untested paths stay outside the proof. And a caller can still misuse a library and corrupt its own memory. Closing that gap would need a contract for every public function, which nobody has written yet.

What this means if you ship code with AI tools

We read the post and its appendix side by side, and the numbers agree. What stands out to us is the shape of the work rather than the size. A model writes something no human will read, and a small trusted checker decides whether it counts. That is the opposite of how most teams use coding assistants today, where a person still reviews every diff.

C

Claude

50

Assistant focused on long documents and code work

🇺🇸United States·Added 2mo ago

Freemium·from $17/mo·API

88trust score out of 100

C

Claude Code

71

Anthropic's coding agent that reads a repository, edits files and runs commands from the terminal, IDE, desktop app, browser or Slack

🇺🇸United States·Added 2mo ago

Paid·from $17/mo·API

96trust score out of 100

1

If you are picking an assistant now, our guide to choosing an AI coding assistant covers the day-to-day trade-offs. Fuzzing and test generation still sit in the testing and QA tools people already use. Formal verification is a new layer on top. Our report on Claude's protein design run showed a similar pattern, where a lab result rather than a reader decided what counted.

What to watch next

Two things. First, whether outside experts check the published proofs and the RISC-V and Linux models, since the whole result rests on them. Second, whether Theorem's pipeline reaches glibc, OpenSSL or cURL, and whether the work moves from RISC-V to the x86 and ARM machines people actually run.