Anthropic and Theorem Deploy Claude to Mathematically Prove Code Correctness

The effort to guarantee that software will never fail has long been one of the most difficult and expensive undertakings in computer science, a task so resource-intensive that it has historically been reserved for only the highest-stakes applications. A new project by Anthropic, however, aims to make this rigorous form of assurance commonplace, using its Claude model to automate the generation of formal proofs that existing software is correct.

The work, conducted in partnership with a company called Theorem, required the model to produce approximately 180 million lines of mathematical proof code in just a few weeks. This large-scale effort focused on 123 open-source libraries, using the test programs from Google's OSS-Fuzz security project. The process did not involve writing new code but instead focused on verifying the safety of existing software by translating crash tests into mathematical problems and analyzing the resulting compiled machine code.

The scale of this undertaking is a significant departure from past practice. For context, a team of specialists once required 20 person-years to formally verify a single, small operating system kernel known as seL4. This extreme cost has historically restricted the use of formal verification to critical systems, such as avionics software for Airbus aircraft, where failure is not an option.

The AI's role in this project extends beyond mere proof generation. During the process of creating the proofs, which are then checked by an independent program called Rocq, the model identified and was permitted to fix hundreds of bugs. Many of these issues had eluded conventional testing for years because they only appear under very specific and unusual conditions, such as a particular sequence of data access or an unusually large input file.

Anthropic's Frontier Red Team reported that in one instance, while attempting to verify a widely used PDF reader, Claude discovered as many security bugs in a single week as are typically reported for that software over an entire year. In another application, the model uncovered a logical error that had gone undetected for more than a decade. Researchers have termed the process 'fully autonomous,' though the formal foundations and tools for the work were built by humans at Theorem.

The company acknowledges that a 'formally verified' label does not equate to a guarantee that software is error-free. The mathematical proofs hold only under a specific and constrained set of circumstances, including a particular processor architecture, single-threaded programs, and inputs under 64 MB. In practice, these libraries are used across a wide range of different hardware and system configurations.

The computational expense for generating these proofs is also substantial, with some individual proof generations running to hundreds of millions of tokens, and Anthropic has not disclosed the total project cost. However, the company points to a potential for significant savings. If AI can verify its own code, developers would need to spend far less time on review, which would reduce costs across the entire software development process.

A smaller test run also indicated that proofs, once created, can be reused, and newer models are becoming more efficient at the task. Anthropic's Opus 5.5 model can solve half of the proofs using about 40 percent fewer tokens than its Opus 5 predecessor. The company expects that formal verification with AI will soon become as routine and practical as standard testing.

The initiative has a direct bearing on the future of software automation. The question, the company suggests, shifts from whether an AI can program to whether an AI can prove that the code it writes is safe. Theorem's roadmap already targets critical infrastructure components such as glibc, OpenSSL, and cURL, signaling a potential expansion of this verification method to foundational software used by a vast number of systems.