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

> Anthropic says Claude turned existing fuzz tests into machine-checked proofs that the compiled binary cannot crash on bounded inputs.

- **Severity:** Info: Research, tools, evals or lab claims with no direct exposure. Context, not an alert.
- **Category:** Research, Lab safety
- **Published by:** Anthropic
- **Disclosed:** 2026-10-22
- **Affects:** OSS-Fuzz libraries, Open-source software
- **Research by:** Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, [Anthropic Frontier Red Team](https://www.anthropic.com/research/team/frontier-red-team), [Theorem](https://theorem.dev/oss-verify/) (Theorem)
- **Primary source:** https://www.anthropic.com/research/formal-verification
- **Page:** https://theinjection.dev/items/anthropic-formal-verification-oss-fuzz/

Anthropic's Frontier Red Team reports that Claude produced machine-checked Rocq proofs that 239 fuzz-test entry points across 123 OSS-Fuzz libraries always exit normally on inputs under 64 MB, proven at the RISC-V binary level.

## What 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.

## How 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.

## Who 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.

## What 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.

## Quick facts

- **Proven:** 239 fuzz-test entry points across 123 OSS-Fuzz libraries
- **Property:** The program always exits normally, with no memory-safety error or failing assertion, on inputs under 64 MB
- **Proof system:** Rocq, against Theorem's RISC-V and Linux process semantics, about 180 million lines in total
- **Published subset:** Proofs for 60 entry points in 25 libraries, checked with Rocq 9.2.0, plus 20,164 theorem statements across 427 projects of which 138 are proved
- **Example bug:** A rediscovered flaw in libexpat tracked as CVE-2026-56132
- **Model efficiency:** On 36 small tasks, Anthropic reports Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5

## Questions

### 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

1. [Anthropic Research Post](https://www.anthropic.com/research/formal-verification)
2. [Published Proofs](https://github.com/theorem-labs/oss-verify-proofs)
3. [Theorem OSS Verify](https://theorem.dev/oss-verify/)