Anthropic Has Claude Write Formal Proofs for 123 Open-Source Libraries

What happened

It starts with fuzz-test entry points Google's OSS-Fuzz project wrote for open-source libraries. Claude turned each test into a formal specification — 'this test never crashes on inputs under 64 MB' — wrote Rocq proofs against the compiled RISC-V executables, and had the Rocq kernel check them mechanically; Theorem supplied the formal RISC-V and Linux-process semantics. All intermediate proof attempts totaled about a billion lines; the finished proofs run to about 180 million lines, with a typical proof around 600,000 lines for a binary with a median of 18,000 RISC-V instructions.

When a proof would not go through, it often meant a real bug: Claude patched the code, regenerated the specification, and proved again. Examples include a decompressor counter underflow causing an out-of-bounds write only on ~20 MB inputs with a rare layout, an image-decoder out-of-bounds read needing a 64 MB input and over 2 GB of memory, a rediscovery of CVE-2026-56132 in libexpat, and a previously unknown logic bug latent for over a decade. The team also formalized RFC 1950 and proved the Linux kernel's zlib implementation conforms to it at the x86 binary level.

Anthropic has published a subset of the proofs and the RISC-V/OS semantics on GitHub; Theorem says it will run the same pipeline for other open-source projects and has released a Claude skill to help developers verify their own code. The research was done jointly by Anthropic's Frontier Red Team and Theorem, which calls it, to its knowledge, the first large-scale effort to use AI for formal verification of production software at the assembly level.

Key facts

1. Released Oct 22, 2026, on Anthropic's research blog (Frontier Red Team) with formal-verification company Theorem: 'LLMs are making formal software verification feasible at a much larger scale'
2. Scale: 239 test entry points across 123 Google OSS-Fuzz open-source libraries; about 180 million lines of Rocq proofs (a typical proof ~600,000 lines for a binary with a median of 18,000 RISC-V instructions); completed in weeks
3. What was proved: against the compiled RISC-V assembly, under assumptions of inputs under 64 MB, single-threaded static binaries, fixed memory budgets and Linux, the programs exit normally with no memory-safety errors and no failed assertions; checked mechanically by the Rocq kernel
4. Bugs found: hundreds, most hard for fuzzers to hit — a decompressor counter underflow (out-of-bounds write) triggered only by ~20 MB inputs with a rare layout, an image-decoder out-of-bounds read needing a 64 MB input plus 2 GB of memory, a rediscovery of CVE-2026-56132 in libexpat, and a previously unknown logic bug latent for over a decade; one widely used PDF reader yielded in a week as many security bugs as it typically reports in a year
5. For reference: the seL4 microkernel took two person-years to implement and 20 person-years to formally verify; this work compressed a comparable effort into weeks
6. Limitations (Anthropic's own): the proofs cover specific compiled RISC-V programs, not 'bug-free' — most people run these libraries on x86 or ARM dynamically linked against glibc; AddressSanitizer does not catch all memory-safety bugs; not every entry point of each library was verified
7. Next: a subset of the proofs and the RISC-V/OS semantics are public on GitHub; Theorem offers the same pipeline to other open-source projects and has released a Claude skill