Anthropic says Claude proved 239 fuzz targets in 123 open-source libraries cannot crash

What Anthropic announced

Anthropic's Frontier Red Team said on 22 October 2026 that it used Claude to formally verify security properties in 123 open-source libraries, working with Theorem, a start-up that builds formal verification tools. Formal verification means proving mathematically that a program always follows a set of rules, rather than testing it on a sample of inputs and hoping the sample was representative.

The headline claim is specific. For 239 fuzz-test entry points across 123 libraries in Google's OSS-Fuzz programme, Claude produced proofs that the compiled programs exit normally, without memory-safety errors or failed assertions, for every input smaller than 64 MB. Anthropic calls it, to its knowledge, the first large-scale effort to use AI to formally verify production software at the level of assembly code.

Anthropic says the work took a few weeks and that Claude found and patched bugs along the way, some of which had survived years of automated testing. The post lists 15 authors, including Nicholas Carlini.

Turning fuzz tests into proofs

The hard part of formal verification is usually writing the specification, the precise statement of what correct behaviour means. For a PNG decoder that is fairly clear. For a text editor or a browser it is not, and writing complete specifications by hand has kept formal methods confined to a few critical systems.

Anthropic and Theorem sidestepped that problem by reusing tests developers had already written. OSS-Fuzz runs fuzzers, programs that throw huge numbers of random and mutated inputs at a project's chosen entry points and flag any input that causes a crash. OSS-Fuzz builds C and C++ code with AddressSanitizer, a compiler tool that turns improper memory access into an immediate crash.

The team converted each fuzz test into a theorem: this entry point, compiled to RISC-V machine code, never crashes on any input below 64 MB. If Claude can prove that, the fuzzer has nothing left to find for that entry point, no matter how long it runs. RISC-V is an open processor instruction set, a rival to x86 and ARM.

How big the proofs are

The proofs are written in Rocq, the proof assistant formerly known as Coq. Anthropic says they total about 180 million lines, with a typical proof around 600,000 lines, covering binaries with a median length of 18,000 RISC-V instructions. They are built by translating the assembly code into a mathematical model using Theorem's semantics for RISC-V instructions and Linux processes.

No human is expected to read that much proof. The Rocq checker mechanically confirms that each proof establishes its theorem. That is the reason the approach can scale: the cost of checking does not grow with the number of people who would otherwise have to review the work.

Anthropic and Theorem are publishing a subset of the proofs in an MIT-licensed repository, plus the RISC-V and Linux process semantics they were built on, and specifications for fuzz tests they could not prove. Anthropic says it is withholding proofs that could reveal bugs not yet patched upstream.

What you have to trust

Anthropic lists three things a reader still has to trust: the formal models of RISC-V and of Linux processes, the exact theorem statements, and the Rocq proof checker itself. A footnote adds the hardware, operating system and OCaml compiler that Rocq runs on.

That is a much smaller target than the code being verified, and it does not grow as more libraries are proved. But it means a proof is only as good as its model of the machine. If the semantics describe a processor or a system call slightly differently from reality, a verified program could still misbehave in that gap.

The bugs Claude found on the way

To keep the work moving, the team let Claude patch bugs it found, regenerate the specification for the patched code and continue. Anthropic says the effort surfaced hundreds of bugs, many of which a fuzzer would be unlikely to hit because fuzzers usually cap inputs near 1 MB and follow code coverage.

Examples in the post include a counter underflow in a bundled decompressor that caused an out-of-bounds write, but only 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 more than 2 GB of memory; and an out-of-bounds read that needed a particular sequence of calls on two handles to the same file. Claude also rediscovered CVE-2026-56132 in libexpat, which needs deeply nested input.

Some findings were not crashes. While proving one library memory-safe, Claude noticed that a feature meant to restrict which files an application can load was not always enforced.

Letting a model edit the code it is proving creates an obvious shortcut: rewrite the program so it trivially never crashes. Anthropic says it penalised every patch, gave extra credit for proving which inputs a patch changes and how few they are, and logged and audited patches for that kind of reward hacking.

Beyond memory safety

A crash-freedom proof can carry more weight than it first appears. Many fuzz tests crash deliberately when a higher-level property fails, for example when compressing then decompressing data does not return the original. Proving such a test never crashes proves the property itself.

Anthropic describes other experiments too. Claude wrote a formal specification of RFC 1950, the zlib format, and proved that the Linux kernel's zlib implementation meets it, this time on x86 machine code using x86 semantics Claude generated. The team found only minor, unexploitable corner-case bugs there and in half a dozen other libraries, and concluded that heavily tested code is already almost fully correct.

In another, Claude built a Python interpreter in Rust and proved with the Verus tool that it follows CPython semantics from an academic paper; on 1.7 million random programs it matched CPython 99.95% of the time. The work follows Claude's role in writing the con-leche proof checker shipped with Lean 4.35 this month. Anthropic says the details are in a separate appendix.

Theorem's free offer to open-source projects

Theorem is now offering the pipeline as OSS Verify, free for qualifying open-source projects. Enrolment works like OSS-Fuzz: a maintainer opens a pull request adding a project directory with a project.yaml file, a Dockerfile and a build script. Projects already in OSS-Fuzz can start from their existing files, but OSS Verify needs static riscv64 binaries, so builds may need porting.

Maintainers receive a machine-checked proof about the compiled fuzz test, plus private reports of any bugs found along the way, and can choose when proofs are published. Theorem has also released a Claude skill for adding a project and a roadmap for verifying the Nix ecosystem, which includes glibc, OpenSSL and cURL.

Cost is the main obstacle

Anthropic names cost as the key limitation: proofs can take hundreds of millions of tokens. It offers two reasons to expect that to fall. On 36 small verification tasks built from OSS-Fuzz code, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5.

Proofs can also be shared. When agents could copy each other's finished proofs, they needed 17% fewer tokens than working alone, and some succeeded after failing solo. Much of each proof covers code every program contains, such as C runtime start-up and AddressSanitizer, so very different libraries ended up with overlapping proofs.

What the proofs do not cover

Anthropic is direct that formally verified does not mean bug-free. The proofs cover single-threaded, static RISC-V binaries linked against musl libc. Most people run these libraries on x86 or ARM, dynamically linked against glibc, so the guarantee does not transfer directly to the builds in most products.

The claim is also narrow. AddressSanitizer does not catch every memory-safety bug, the team did not verify every entry point in each library, and even all entry points would not cover a whole library. A program that misuses a library can still corrupt memory in the caller. Inputs above 64 MB are outside the theorem, though Anthropic says raising that limit takes little human effort.

Why it matters

AI models are finding vulnerabilities faster than many maintainers can handle. This week PHP patched two critical flaws AI helped researchers find, and the cURL project said it would take low and medium vulnerability reports public to cope with a flood of AI-driven reports. Anthropic itself recently said its automated red-teamer beat human bug bounty hunters.

Anthropic's argument is that finding bugs one at a time cannot keep up, and that proofs are the defence that scales, because a proof says an entire class of bug is gone, not just the ones someone found. The work here is a vendor's own report and has not yet been independently reviewed, but the proofs are published for anyone to check. If the token cost keeps falling, Anthropic expects formal verification to become as routine as fuzzing.