Anthropic and Theorem Labs Report: LLMs Enable Large-Scale Formal Verification

On October 23, Anthropic and Theorem Labs released a report titled "LLMs are making formal software verification feasible at a much larger scale." According to the report, Anthropic's Claude model generated approximately 180 million lines of Rocq proof code for 239 program entry points across 123 open-source software libraries, discovering and fixing hundreds of bugs, including some that had evaded detection for years despite trillions of tests.

The core breakthrough of the study is extending verification to the assembly instruction level, using the RISC-V instruction set as the basis for proofs. This marks the first time formal verification has been applied to production software at scale using AI at the assembly code level.

Traditional software testing cannot exhaust all possible cases, while formal verification uses mathematical proofs to confirm that programs satisfy specific safety properties under given conditions. Previously, this work was highly dependent on specialists, costly, and time-consuming, making large-scale application difficult. The study demonstrates that advances in large language models have made this work scalable.

Anthropic noted that most software contains vulnerabilities and that mainstream defense methods are no longer sufficient, calling for reliable ways to prove code is bug-free. The research is seen as helping shift security checks earlier into the development stage, though challenges remain, including limited verification scope, asymmetric costs between attackers and defenders, and the reviewability of AI-generated proofs.