Anthropic: Claude wrote proofs for 239 fuzz targets in 123 libraries

01What happened

Anthropic's Frontier Red Team published the result on October 22, 2026, with the verification company Theorem. Fifteen people are named on the work, including Nicholas Carlini and Nickolai Zeldovich. The post says the effort is, to the authors' knowledge, the first large-scale use of AI-driven formal verification on production software at the assembly level, and that attempting the proofs surfaced hundreds of bugs, which Claude then patched.

02How it works

A fuzz test asks whether any input crashes a program; a proof states that none exists. Claude wrote the proofs in Rocq against Theorem's formal model of RISC-V instructions and Linux process behaviour, so each proof covers the compiled binary rather than the source. The proofs total about 180 million lines of Rocq, a typical one runs to about 600,000 lines for a binary with a median of 18,000 RISC-V instructions, and the post says a proof can take hundreds of millions of tokens to produce. The authors flag a reward-hacking risk, that Claude could make a theorem provable by rewriting code so it never crashes, and say they penalized patches and audited them.

03Who is affected

No product is exposed by the finding. The proofs hold only under stated conditions: a single-threaded static binary on RISC-V and Linux, linked against musl libc, a fixed memory budget, and inputs under 64 MB. Anthropic states plainly that formally verified does not mean bug-free, that not every entry point of each library was covered, and that caller misuse is out of scope. The trusted base includes the RISC-V and operating system models, the theorem statements and the Rocq checker.

04What to do

Maintainers of widely shared dependencies can enrol a project with Theorem's free OSS Verify service, which needs static riscv64 builds and reports bugs privately with no disclosure deadline. Theorem states that AI models generate the findings and patches and that it does not promise a person reviews them first, so treat incoming reports as unreviewed. A subset of the proofs and the trusted components are published, listed below.

Questions people ask

Does Anthropic's formal verification work mean the 123 libraries are bug-free?

Anthropic states that formally verified does not mean bug-free. The proofs cover 239 specific fuzz-test entry points, not whole libraries, and hold only for inputs under 64 MB on a single-threaded static RISC-V binary running on Linux against musl libc. Callers misusing a library are out of scope, and the result depends on trusting the RISC-V model, the theorem statements and the Rocq checker.

Can maintainers get their own project verified this way?

Theorem runs a free OSS Verify service for qualifying open-source projects, enrolled through a pull request that adds a project directory with a build file, much as OSS-Fuzz works. Static riscv64 binaries are required and proofs can take several days. Theorem says AI models generate the findings and patches and that it does not promise a person reviews them before they are sent.

How does this compare with Anthropic's earlier bug-finding work?

Anthropic's earlier posts reported Claude finding issues, such as 493 attack surface problems across 25 projects. Formal verification inverts that: instead of searching for a crashing input, Claude proves that none exists within stated limits. The authors argue attempting a proof is useful on its own, because it surfaces real bugs, including ones fuzzers rarely reach, and proofs can be reused across programs.

Sources 3 links, all fetched

1. 1anthropic.comAnthropic Research Post
2. 2github.comPublished Proofs
3. 3theorem.devTheorem OSS Verify