Claude Writes Formal Proofs for 123 Open-Source Libraries
The proofs only hold under strict conditions, but the search for them exposed hundreds of bugs that years of fuzz testing had missed, Anthropic says.
Anthropic says Claude has used formal verification to write machine-checked proofs that 123 widely used open-source libraries never crash, working on their compiled code rather than their source. The research, published Oct 22, 2026 with verification startup Theorem, covered 239 entry points from Google’s OSS-Fuzz program and took a few weeks.
The guarantee is narrow. Each proof applies to a single-threaded, statically linked RISC-V build of the library, any input up to 64 MB, and every Linux behavior the team modeled. Most real-world deployments use x86 or ARM chips and a different C library, a gap Anthropic acknowledges, warning that “formally verified” does not mean “bug-free.”
The search for proofs still turned up real problems. Anthropic says Claude ran into hundreds of bugs that years of fuzzing had not caught. One was an out-of-bounds write in a decompressor that only triggered on inputs of about 20 MB. Another was a file-loading restriction that was not always enforced. Claude also rediscovered a known libexpat flaw, CVE-2026-56132.
The method starts from tests maintainers already have. Claude turned each library’s fuzz tests into a formal statement that the test can never crash, then wrote a proof in Rocq, a proof assistant whose small kernel checks every step. When a bug blocked a proof, Claude patched the code and proved it again.
The proofs are huge: about 180 million lines of Rocq in all, with a typical one running to roughly 600,000 lines. They are also expensive. A single proof can consume hundreds of millions of tokens, according to Anthropic, which penalized unnecessary patches and logged and audited every one to stop Claude from gaming the task.
Anthropic is publishing a subset of the proofs but holding back any that could reveal unpatched bugs. Theorem is offering the same pipeline free to established open-source projects, which sign up through a pull request, much as projects join OSS-Fuzz. Bugs go privately to maintainers, and Theorem says its AI-generated findings and patches may reach them without a human review.
Our take
The headline number matters less than the method. Fuzzing tells maintainers that a bug was not found; a proof says that, under stated conditions, one cannot exist, and the hunt for those proofs turned up bugs fuzzing had missed for years. The conditions are real limits: RISC-V builds, a fixed memory budget, and costs counted in hundreds of millions of tokens. The test is simple. If maintainers in Theorem's free program start shipping fixes that came out of failed proofs, this becomes normal security practice. If the reports pile up unread, it stays an impressive research result.
Sahil Khatwa, Editor
How this story was checked
- ResearchedWith AI assistance · 3 sources
- Fact-checkedAgainst the original sources
- EditedAnshul Kumawat, Founder and Editor
- Published
Sources
Sahil Khatwa is an editor at AI News Lead, where he reports on and edits coverage of AI products, business and policy.
