Anthropic: Claude Has Undergone Large-Scale Formal Verification of Open-Source Libraries

On October 22, Frontier Red Team—a research group under AI company Anthropic—released a study demonstrating that large language models (LLMs) now possess the capability to autonomously generate formal proofs at scale. In collaboration with Theorem, the team conducted formal verification of security properties for over 100 real-world open-source libraries—at the RISC-V assembly level—using Claude models. This marks the first time an AI system has performed large-scale formal verification of production-grade software directly at the assembly level. During proof construction, the team unexpectedly uncovered multiple long-standing, previously unknown security vulnerabilities. The methodology involved converting existing compilable fuzz test cases from Google’s OSS-Fuzz into formal specifications, then verifying inputs of arbitrary size up to 64 MB under strict constraints: single-threaded static binary execution, fixed memory budget, RISC-V CPU architecture, and Linux runtime environment.