Anthropic says Claude has proven security properties of 123 libraries
Anthropic published research on October 22, 2026, stating that in a collaboration with Theorem, Claude generated machine-verified formal proofs of security properties at the RISC-V assembly code level for 239 fuzzing entry points across 123 open-source libraries, and fixed the vulnerabilities found. The method converts compilable fuzzers in the libraries into formal specifications stating that no input smaller than 64 MB will crash the test, verified by the Rocq proof checker. Anthropic stated that the proofs totaled approximately 180 million lines of Rocq code, and that the process found hundreds of vulnerabilities, many of which were unlikely to be found by fuzzers, including CVE-2026-56132 in libexpat and a logic vulnerability that had lain dormant for over a decade.
While giving the scale of the proofs and the vulnerabilities found, the original source also sets out assumptions and limitations, so readers can use this to assess the current actual coverage of AI formal verification.