---
title: Anthropic and Theorem had Claude write machine-checked no-crash proofs for 239 fuzz entry points in 123 OSS-Fuzz libraries, finding bugs fuzzers likely miss | ctxsec
url: https://ctxsec.com/items/anthropic-theorem-formal-proofs-123-oss-fuzz-libraries
description: ""
status: "confirmed research (Anthropic and Theorem, Oct 22); guarantees hold only under the stated RISC-V/Linux model"
published: 2026-10-23
---

> 

[← AI](/ai) · [markdown](/items/anthropic-theorem-formal-proofs-123-oss-fuzz-libraries.md)

confirmed research (Anthropic and Theorem, Oct 22); guarantees hold only under the stated RISC-V/Linux model

2026-10-23

### Anthropic and Theorem had Claude write machine-checked no-crash proofs for 239 fuzz entry points in 123 OSS-Fuzz libraries, finding bugs fuzzers likely miss

Anthropic says Claude, working with formal-methods firm **Theorem**, turned OSS-Fuzz fuzz targets into formal specs and proved them in the **Rocq** proof assistant. The result covers **239 entry points across 123 libraries**: for every input under 64 MB, the compiled binaries never fault, abort or hit unmodeled behavior.

- **Scope:** the proofs are over compiled **RISC-V** binaries, single-threaded and static, with a fixed memory budget, under Theorem's Linux process semantics, which Theorem calls best-effort and incomplete. They show the ASan-instrumented and normal binaries behave the same. They don't cover other CPUs, threads or properties beyond crashes and memory safety.
- **Size:** about 180 million lines of Rocq, typically about 600,000 per proof, for binaries with a median of 18,000 instructions, done over a few weeks.
- **Bugs found along the way**, which Claude patched before proving: a counter underflow in a bundled decompressor causing an out-of-bounds write only on ~20 MB inputs with one rare layout, an image-decoder out-of-bounds read needing a 64 MB input, and a rediscovery of libexpat CVE-2026-56132.

A subset of proofs and the semantics are public, and Theorem is offering to run the pipeline for other open-source projects (OSS Verify). **Why it matters:** AI-driven bug finding is fueling this month's flood of critical CVEs, and this is the defensive side of the same capability.

Sources: [Anthropic: LLMs are making formal software verification feasible at a much larger scale (Oct 22)](https://www.anthropic.com/research/formal-verification) · [Theorem: oss-verify-proofs, how the proofs were produced](https://github.com/theorem-labs/oss-verify-proofs/blob/main/docs/origin.md)