Anthropic uses Claude to prove 123 open-source libraries crash-free, with 180 million lines of proof

Anthropic says Claude used formal verification to prove that 123 open-source libraries never crash on any input within set limits. While writing the proofs, it also found and fixed hundreds of bugs that had gone unnoticed for years.

Per a post on Anthropic's Frontier Red Team blog on Oct 22, Claude spent a few weeks proving 239 test entry points across 123 libraries in Google's OSS-Fuzz project: for any input under 64 MB, they finish without memory-safety errors or failed assertions. The proofs target compiled RISC-V machine code and run to about 180 million lines of Rocq. The work was done with the startup Theorem. Claude turned up bugs fuzzers are unlikely to hit, such as a decompressor flaw that fires only on a rare 20 MB input, and in one PDF reader it found as many security bugs in a week as are typically reported in a year.

Formal verification has long been costly: the seL4 kernel took two person-years to build and 20 to verify. Anthropic predicts it "will soon be as practical as fuzzing is today." Opus 5.5 solved its verification tasks with about 40% fewer tokens than Opus 5. Anthropic also flagged limits: a proof can take hundreds of millions of tokens, and the results assume single-threaded, statically linked RISC-V Linux binaries, unlike the x86 and ARM systems most people run. Theorem is offering to run the pipeline for other open-source projects and has released a Claude skill. Anthropic's post on X passed 160,000 views.