Anthropic and its partner Theorem have used Claude to check existing software through mathematical proofs. In a project spanning 123 open-source libraries, the model generated roughly 180 million lines of proof code in a few weeks and exposed hundreds of bugs that conventional testing had missed.
The work points toward a new role for AI in software development: checking whether programs behave correctly under defined conditions, not just producing code. But formal verification still has important limits, including high computing costs and assumptions that do not cover every way software is used.
Turning crash tests into formal proofs
Formal verification aims to show mathematically that software behaves as intended, rather than relying only on tests that check selected cases. That level of assurance has traditionally demanded specialist effort. The article notes that verifying the small operating system kernel seL4 took 20 person-years, helping make the approach practical mainly for exceptional cases such as Airbus avionics software.
For this project, Anthropic's Frontier Red Team worked with Theorem to apply Claude to existing code. The work drew on test programs from 123 open-source libraries in Google's OSS-Fuzz security project. Claude translated crash tests into mathematical problems, analyzed compiled machine code, and generated proofs about the software's behavior.
A separate program, Rocq, checks whether the proofs are valid. Anthropic says the workflow needs almost no human reviewers and describes the proof generation as “fully autonomous.” That description has a boundary: people at Theorem built the tools and formal foundations that made the process possible.
Proof work can expose bugs along the way
The project produced more than verification results. As Claude worked through the proofs, it found hundreds of bugs and was allowed to fix them. Some appeared only in unusual situations, such as very large input files or a particular sequence of accesses, which can make them difficult for conventional tests to catch.
One effort focused on a widely used PDF reader. In one week, the team found as many security bugs as are typically reported for that software in an entire year. In another application, Claude identified a logical error that had gone undetected for over a decade.
A proof does not need to be completed for the effort to be useful, according to Anthropic: attempts that fall short can still reveal real bugs. That makes the process potentially valuable as a way to inspect software, even when it cannot establish a complete correctness result.
What a proof does—and does not—establish
Anthropic cautions that “formally verified” does not mean “error-free.” The project’s proofs hold only under specific assumptions: a particular processor architecture, single-threaded programs, and inputs smaller than 64 MB. The libraries may be used on other hardware and in other configurations, so a proof under those conditions does not automatically cover every real-world use.
The computing demands are another constraint. Individual proofs can run up hundreds of millions of tokens, and Anthropic did not report the total cost of the project. The company argues that verification could still reduce time spent reviewing software and lower costs across the coding process if developers can rely more on AI-generated code.
A smaller test run also suggested that proofs can be reused. The article reports that Opus 5.5 solves half the proofs with about 40 percent fewer tokens than Opus 5. That points to improved efficiency in the trial, though it does not remove the broader compute demands described for the project.
Making formal verification more routine
Anthropic sees AI-assisted proof generation as a path toward making formal verification as practical as standard testing. If software can be accompanied by a proof of its behavior within clear limits, developers may have a stronger basis for trusting automated coding. The question then becomes not only whether AI can program, but whether it can demonstrate what its code guarantees.
Theorem's roadmap already targets critical infrastructure, including glibc, OpenSSL, and cURL. Extending the approach to such projects would put its practical limits under greater scrutiny: proofs must match the hardware, input boundaries, and execution assumptions that matter for each use. For now, the project shows both the promise of AI-assisted software verification and the careful conditions required to interpret its results.