Anthropic Uses Claude to Prove 239 OSS-Fuzz Targets Can't Crash, Finding Hundreds of Bugs

TL;DR

Anthropic's Frontier Red Team and the verification startup Theorem published results on October 22 in which Claude wrote formal proofs for production code. Anthropic calls it, to its knowledge, the first large-scale effort to formally verify production software at the assembly level with AI. Over a few weeks, Claude proved that 239 fuzzing entry points across 123 libraries in Google's OSS-Fuzz never crash on any input under 64 MB. The proofs cover the compiled RISC-V binaries, not the source, and come to about 180 million lines of Rocq, every one of them checked by the Rocq kernel. Claude found hundreds of bugs on the way and patched them before finishing the proofs. A subset of the proofs is public, and Theorem will run the pipeline for free on open-source projects that qualify.

What was actually proved

A fuzz target is an entry point that developers write so a fuzzer can throw inputs at it. Any input that crashes it counts as a bug. Fuzzing is a brute-force search with no end, because the input space is infinite. Anthropic turned each fuzz target into a theorem instead: for every input under 64 MB, every modeled Linux system-call response and every memory layout, the program exits normally, without a memory-safety error or a failed assertion.

Once that theorem is proved, fuzzing that entry point on that binary can never find anything. Anthropic puts it this way: "A formal no-crash proof over all inputs rules out all crashes along any path reachable from the entry point."

The numbers from the post:

• 239 entry points in 123 OSS-Fuzz libraries, proved over a few weeks.
• About 180 million lines of Rocq in total, with a typical proof around 600,000 lines.
• A median binary of 18,000 RISC-V instructions per proof target.
• Hundreds of bugs surfaced during the attempts, and Claude patched them before re-proving the updated code.

That works out to roughly 33 lines of Rocq per machine instruction, which nobody will ever read by hand. Nobody has to: the Rocq checker confirms the proof meets the specification, so you only need to trust three things: the formal model of RISC-V and Linux processes, the exact theorem statements, and the Rocq checker itself.

Where the spec comes from

Writing the specification is usually the hard part of formal verification. What does "correct" mean for a text editor? Anthropic skipped that question by taking the specs developers had already written: their fuzz tests. "This test never crashes" is a spec you get for free.

It also proves more than memory safety. OSS-Fuzz builds C and C++ targets with AddressSanitizer, so bad memory access crashes the program, and many fuzz tests assert higher-level properties. The post's example is an LZO harness that compresses an input, decompresses it and asserts the result matches. A no-crash proof for that harness is a proof of the round-trip property.

Sometimes the proof dragged in properties nobody asked for. To finish the cpp-httplib proof, Claude had to rule out a stack overflow from recursion in the std::set destructor, which meant proving, on machine code, that libc++'s red-black tree keeps its depth logarithmically bounded. Picture a building inspector who came to check one fire exit and ended up certifying the elevator shaft.

The bugs fuzzers would not find

Fuzzers mutate small inputs, typically capped at 1 MB, and follow code coverage. A proof has to account for every input under 64 MB, so it runs into bugs that live in places fuzzers rarely reach:

• A counter underflow in a bundled decompressor that led to an out-of-bounds write, but only on inputs around 20 MB with one rare, specific layout.
• An out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory.
• An out-of-bounds read in another library that needed a particular sequence of calls across two handles to the same file.
• A rediscovery of CVE-2026-56132 in libexpat, triggered by deeply nested input.

Claude also caught a logic bug that never crashes at all: while proving one library memory-safe, it noticed that a feature for restricting which files an application can load is not always enforced. Outside the OSS-Fuzz run, the team says a verification attempt on a widely used PDF reader found as many security bugs in one week as are typically reported in a year, and another effort found a logic bug latent for more than a decade. Anthropic does not name either project.

The other experiments

Anthropic also tried two other kinds of verification:

• zlib against its RFC. Claude wrote a formal spec of RFC 1950 and proved that the zlib implementation in the Linux kernel follows it, at the x86 binary level, using x86 semantics Claude generated itself. The team repeated this for about half a dozen other widely used libraries and found only minor, unexploitable corner-case bugs.
• A Python interpreter in Rust. Claude built an interpreter for a large subset of Python and proved with Verus that it follows CPython semantics as described in an academic paper. On 1.7 million randomly generated programs, it matched CPython in 99.95% of tests.

According to a footnote, single-stepping through the self-generated x86 semantics can boot an Ubuntu userspace on a Linux kernel Writing them also turned up hundreds of mistakes in the official reference documentation plus a smaller number of hardware bugs.

The cost curve

Anthropic says full proofs can take hundreds of millions of tokens, so token efficiency decides who can afford this. On 36 small verification tasks built from OSS-Fuzz code, Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5. When agents could copy each other's finished proofs from a shared workspace, they needed 17% fewer tokens than agents working alone. Most of any proof covers code every program shares, such as C runtime and AddressSanitizer setup, so very different programs end up with overlapping proofs.

Theorem's own eval, published September 29 and updated October 19, measures the same trend as kilobytes of machine code verified per hour:

Theorem extrapolates from that curve: if the doubling holds, 95% of the machine code in nixpkgs could be verified by the end of 2027 for about $134 million. Shared libraries do most of the work in that model. OpenSSL sits in the runtime closure of nearly 16,000 packages, and Theorem prices its proof at about $220,000, or around $14 per package that reuses it. These are projections, not results, and they depend on a two-month doubling time that has been measured for four months.

What is public and what you can use

The public release is smaller than the headline. The oss-verify-proofs repo (MIT) holds proofs for 60 entry points in 25 libraries, including OpenSSL, zstd, simdjson, bzip2 and libpcap targets. Anthropic says it withheld proofs that could reveal unpatched bugs. Every proof is checked with Rocq 9.2.0 and stated in Theorem's Linux process model for RISC-V binaries.

If you maintain an established open-source project, OSS Verify is the practical part of this news. Theorem says qualifying projects pay nothing. A core maintainer enrolls by opening a pull request against theorem-labs/oss-verify with a project.yaml, a Dockerfile and a build.sh that produce static riscv64 fuzz binaries. The repo ships a Claude skill and a prompt you can paste into Claude Code, Codex or Cursor to do the enrollment for you. Findings go privately to your security contact, with no disclosure deadline. Theorem warns that findings and patches are AI-generated and that no human is promised to review them before they reach you. Read every patch before you merge it.

Limitations

Anthropic's own caveat is "'Formally verified' does not mean 'bug-free.'" The proofs are only as good as their assumptions, and the assumptions are narrow:

• They cover single-threaded, static RISC-V binaries linked against musl (the public repo's are built with clang 20.1.8). Most people run these libraries on x86 or ARM, dynamically linked against glibc.
• They cover the code one entry point reaches, not the whole library, and they do not cover a caller that misuses the API.
• AddressSanitizer does not catch every memory-safety bug, and the proofs say nothing about wrong results or memory leaks.
• The public repo notes that no proof in this release shows the program halts, so an input that makes it loop forever is not ruled out.
• Claude could have cheated by rewriting a program into one that trivially never crashes. Anthropic penalized patches, gave extra credit for proving which inputs a patch changed and how few there were, and logged and audited the patches.

The skeptics on Hacker News mostly raised the spec gap: a perfect proof of the wrong statement is still the wrong statement. Anthropic's appendix concedes a related point for harder code: experience from other agent-based projects such as MachCSL suggests agents may "hit a complexity wall" with this verbose proof style. Still, the trusted base is far smaller than the code it now covers, and it does not grow as more projects get verified.

Key Takeaways

• Claude proved 239 OSS-Fuzz entry points in 123 libraries crash-free for every input under 64 MB, at the compiled RISC-V binary level, in about 180 million lines of kernel-checked Rocq.
• The specs came from existing fuzz tests, which removes the usual bottleneck of hand-writing a spec for each project.
• The proof attempts found hundreds of bugs, including ones that need 20 MB or 64 MB inputs that fuzzers rarely try.
• Cost is still hundreds of millions of tokens per full proof, but Opus 5.5 used about 40% fewer tokens than Opus 5 on small tasks, and shared proofs saved 17%.
• 60 entry points in 25 libraries are public under MIT, and Theorem's OSS Verify offers the pipeline free to qualifying projects.
• The guarantees hold for static, single-threaded RISC-V and musl builds, not the x86 and glibc builds most people ship.

Sources: Anthropic: LLMs are making formal software verification feasible at a much larger scale, theorem-labs/oss-verify-proofs, theorem-labs/oss-verify, Theorem: OSS Verify, Theorem: Bootstrapping the Verified Software Stack, theorem-labs/rocq-linux-process-semantics, Hacker News discussion