Anthropic's Frontier Red Team says Claude wrote formal proofs that security properties hold in the compiled code of 123 open-source libraries, and found hundreds of bugs along the way. The research, published October 22 with formal-methods company Theorem, covers 239 fuzz-test entry points drawn from Google's OSS-Fuzz initiative and roughly 180 million lines of proof written for the Rocq proof assistant.
The authors describe it as the first large-scale effort to use AI for formal verification of production software at the assembly level. Formal verification produces a machine-checked proof that code behaves as specified for every possible input, work that has historically taken experts years per project. Claude completed this run over a few weeks.
The property proven is narrow but demanding: no crashes on any input under 64 MB, across modeled Linux responses and memory layouts. The proofs assume a single-threaded, statically linked RISC-V binary with a fixed memory budget running on Linux. A typical proof runs about 600,000 lines and covers a binary with a median of 18,000 RISC-V instructions.
Key facts
- 01Claude proved no-crash security properties for 239 fuzz-test entry points across 123 open-source libraries from OSS-Fuzz.
- 02The proofs total about 180 million lines of Rocq; a typical proof runs about 600,000 lines.
- 03Hundreds of bugs surfaced, including a rediscovery of CVE-2026-56132 in libexpat.
- 04Opus 5.5 proved half of 36 benchmark tasks using about 40% fewer tokens than Opus 5.
- 05Anthropic's Frontier Red Team published the work on October 22 with formal-methods company Theorem.
The pipeline starts from each project's existing fuzz test, an entry point where any crash counts as a bug. That code is compiled to RISC-V and combined with Theorem's RISC-V and Linux process semantics plus the no-crash property to form a formal specification. Claude writes the proof and the Rocq proof checker verifies it. Once a proof is accepted, the authors say, fuzzing that entry point becomes superfluous, because a proof over all inputs rules out crashes on any path reachable from it.
The bugs surfaced when proof attempts failed. Examples in the post include a counter underflow in a decompressor that caused an out-of-bounds write on roughly 20 MB inputs with one rare memory layout, an out-of-bounds read in an image decoder that required a 64 MB input and more than 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat triggered by deeply nested input. Claude patched the bugs it found, regenerated the specification and then proved the new version.
Anthropic also reported case studies beyond the OSS-Fuzz set. Claude wrote a specification from RFC 1950 and proved the Linux kernel's zlib implementation meets it at the x86 binary level, using x86 semantics Claude generated itself. Using the Verus tool, Claude proved a Python interpreter written in Rust adheres to CPython semantics; across 1.7 million random programs, its behavior matched CPython in 99.95% of tests. In one widely used PDF reader, a week of effort turned up as many security bugs as are typically reported in a year.
Efficiency is improving with newer models. On 36 small verification tasks taken from OSS-Fuzz code, Opus 5.5 proved half while using about 40% fewer tokens than Opus 5. Agents working in a shared workspace needed 17% fewer tokens than agents working alone, and some succeeded after failing solo, partly because they copied and adapted proofs of shared runtime code across programs.
The authors list the limits plainly. Formally verified does not mean bug-free, since a proof checker cannot confirm that a specification matches reality. The proofs cover static RISC-V binaries linked against musl libc, while most deployed software runs on x86 or ARM with dynamically linked glibc. Not every entry point was verified, dead code is not covered, and a single proof can take hundreds of millions of tokens to produce.
The team also guarded against reward hacking, where Claude could make a theorem provable simply by rewriting code so it never crashes. Patches were penalized, logged and audited, and Claude earned extra credit for minimizing and documenting any changes it made.
A subset of the proofs, along with the RISC-V and operating-system semantics, is published on GitHub. Theorem is offering to run the pipeline for other open-source projects and has released a Claude skill to help developers get started. The authors argue that formal verification will become as practical for most production software as fuzzing is today.
Working on something we should cover, or seeing a story we missed? Send leads, documents, or feedback to hello@aichatdaily.com. For sensitive tips, see our secure tips page for Signal and PGP options.
Spotted an error? Email hello@aichatdaily.com with the URL and the issue, or read our full corrections policy.
