Claude wrote 180 million lines of proof so 123 libraries can't crash, and that is the defender's answer this week
Anthropic's Frontier Red Team published a formal verification result on October 22 that is hard to read without blinking. Working with Theorem, Claude proved no-crash properties for 239 entry points across 123 open-source libraries from OSS-Fuzz, checked at the RISC-V binary level. The proofs total about 180 million lines of Rocq, with a typical proof running to about 600,000 lines. Link: https://www.anthropic.com/research/formal-verification
The trust base is small on purpose. You have to believe the RISC-V and Linux models, the theorem statements and the Rocq checker, and nothing else. Claude does not get to grade its own work. Along the way it fixed the bugs that blocked the proofs, including ones fuzzers would almost never hit because they need inputs around 20 MB or memory configurations of 64 MB and 2 GB, and it rediscovered a known libexpat CVE. A side project checked a Rust reimplementation of CPython against the real one and matched on 99.95 percent of 1.7 million random programs.
Two numbers matter for anyone running agents at scale. Opus 5.5 proves half the targets with about 40 percent fewer tokens than Opus 5. And when agents shared a proof workspace, so one agent's lemmas were reusable by the next, total tokens fell 17 percent and the shared setup beat solo cost on 30 of 34 proofs. That is a multi-agent memory result hiding inside a security paper. The proofs and semantics are public at github.com/theorem-labs/oss-verify-proofs, along with a Claude skill to onboard new projects.
Put it next to the rest of the week. PHP2Shell showed models finding exploitable bugs at internet scale, and Microsoft tied a nation-state campaign to an agent framework. The usual defense is to find bugs faster than the other side. This is a different bet: prove whole classes of failure impossible, with a checker that does not care how persuasive the model is. When proving gets cheap enough, tests stop being the ceiling of what a codebase can claim about itself.
← Back to all articles
The trust base is small on purpose. You have to believe the RISC-V and Linux models, the theorem statements and the Rocq checker, and nothing else. Claude does not get to grade its own work. Along the way it fixed the bugs that blocked the proofs, including ones fuzzers would almost never hit because they need inputs around 20 MB or memory configurations of 64 MB and 2 GB, and it rediscovered a known libexpat CVE. A side project checked a Rust reimplementation of CPython against the real one and matched on 99.95 percent of 1.7 million random programs.
Two numbers matter for anyone running agents at scale. Opus 5.5 proves half the targets with about 40 percent fewer tokens than Opus 5. And when agents shared a proof workspace, so one agent's lemmas were reusable by the next, total tokens fell 17 percent and the shared setup beat solo cost on 30 of 34 proofs. That is a multi-agent memory result hiding inside a security paper. The proofs and semantics are public at github.com/theorem-labs/oss-verify-proofs, along with a Claude skill to onboard new projects.
Put it next to the rest of the week. PHP2Shell showed models finding exploitable bugs at internet scale, and Microsoft tied a nation-state campaign to an agent framework. The usual defense is to find bugs faster than the other side. This is a different bet: prove whole classes of failure impossible, with a checker that does not care how persuasive the model is. When proving gets cheap enough, tests stop being the ceiling of what a codebase can claim about itself.
Comments