Code Verification: Claude Generates 180 Million Lines of Proof

The task of proving software runs without error has historically required years of specialized labor.

Anthropic reported that its Claude model completed this work in a matter of weeks for 123 open-source libraries. The company collaborated with Theorem to apply formal verification, a method that uses mathematics to guarantee code behavior under specific conditions.

Claude generated approximately 180 million lines of proof code during the project. The model analyzed compiled machine code from libraries in Google's OSS-Fuzz security project. A separate verification program called Rocq automatically checked the results, requiring minimal human review.

The process identified hundreds of bugs in the existing code. Researchers noted that many of these flaws would likely escape standard testing because they appear only under narrow conditions, such as unusually large input files or specific access sequences. In one instance, the team found as many security bugs in a widely used PDF reader in one week as are typically reported in a full year.

Claude also identified a logical error in another application that had gone unnoticed for more than a decade. The model was permitted to fix the bugs it encountered. Anthropic stated that even when a complete proof fails, the attempt can reveal real errors.

The company clarified that the proofs hold only under defined conditions, including a particular processor architecture, single-threaded programs, and inputs smaller than 64 MB. For comparison, specialists previously required 20 person-years to verify seL4, a small operating system kernel.

Individual proofs consume hundreds of millions of tokens, and Anthropic has not published total project costs. A smaller test run showed that Opus 5.5 solves half the proofs using about 40 percent fewer tokens than Opus 5. Theorem's roadmap targets critical infrastructure including glibc, OpenSSL, and cURL.