Anthropic: Claude proved security properties across 123 libraries

Anthropic said Claude produced machine-checked formal proofs of security properties at the RISC-V assembly level for 239 fuzz-test entry points across 123 open-source libraries, in work with Theorem. About 180 million lines of Rocq passed the checker, which the company calls the first large-scale AI effort to formally verify production software at the assembly level.

• 239 fuzz-test entry points across 123 libraries, proved at RISC-V assembly level
• About 180M lines of Rocq passed the checker out of roughly 1B generated
• Proofs cover inputs under 64 MB and all modeled memory layouts
• Claude found hundreds of bugs, including CVE-2026-56132 in libexpat