What happened
- On October 22, 2026, Anthropic published work with the company Theorem in which Claude proved security properties in the compiled code of 123 open-source OSS-Fuzz libraries, across 239 entry points.
- The proofs show those programs exit without memory-safety errors or failed assertions for every input under 64 MB, under assumptions: a single-threaded static binary, a fixed memory budget, a RISC-V processor and Linux.
- They total about 180 million lines of Rocq. A typical proof runs to around 600,000 lines for binaries with a median of 18,000 instructions.
- Along the way, Claude found bugs that had escaped trillions of test runs, including an out-of-bounds read, and rediscovered CVE-2026-56132 in libexpat.
Why it matters
- Formal verification used to be a luxury: according to Anthropic, implementing the seL4 kernel took two person-years and verifying it took 20. If that cost falls, it can reach libraries that any application uses.
- A proof is not a patch. It guarantees only the properties proven, under the stated assumptions; a multithreaded binary or one with a different memory budget is out of scope.
- For development teams, Theorem offers to run the same pipeline on other open projects and is publishing a Claude skill to get started.
The number
180 million. Lines of Rocq proofs the project produced.
Context
Anthropic describes other trials. Claude wrote a formal specification of the zlib format and proved that the Linux kernel’s implementation meets it. It also built a Python interpreter in Rust that matched CPython in 99.95% of 1.7 million random programs.
What’s next
- Anthropic is publishing a subset of the proofs and holding back those that could reveal unpatched bugs.
- The company says Opus 5.5 proves half of 36 verification tasks with about 40% fewer tokens than Opus 5.
Bottom line
PHP fixed two remote-execution flaws stuck for two years, sized with AI. And Cisco documented malware that takes orders from several AI models: the same compute serves to attack and to prove that code holds.
Sources
- Anthropic — LLMs are making formal software verification feasible at a much larger scale (October 22, 2026)
- Cover image: Derrick Coetzee (User:Dcoetzee), CC0, via Wikimedia Commons
Edited by Rodrigo Cornejo. How we select and verify: who writes these notes.
