Anthropic Uses Claude to Generate Mathematical Proofs That Existing Software Is Correct

Anthropic says it has used its Claude model to mathematically prove that existing software code behaves correctly, a task that has traditionally demanded enormous expert effort. The company presents the work as a step toward making AI-generated software easier to trust, though it also spells out strict limits on what the proofs guarantee.

Formal verification, the practice of proving that software runs without error in all circumstances, has long been prohibitively expensive. Specialists needed 20 person-years to verify seL4, a small operating system kernel, which is why the technique has largely been confined to extreme cases such as Airbus avionics software.

Anthropic's Frontier Red Team worked with a partner, Theorem, to hand the proof work to Claude instead. In a matter of weeks, the model generated about 180 million lines of mathematical proof code. It drew on test programs from 123 open-source libraries in Google's OSS-Fuzz security project.

Claude did not write new software. It verified existing code by turning crash tests into mathematical problems, analyzing the compiled machine code and constructing extensive proofs. A separate verification program called Rocq checks those proofs automatically, and Anthropic says the process needs almost no human reviewers. The researchers describe the proof generation as "fully autonomous," while noting that the tools and formal foundations were built by humans at Theorem.

In the course of the work, Claude encountered hundreds of bugs and was permitted to fix them. The researchers say many would likely have escaped conventional testing because they appear only under narrow conditions, such as unusually large input files or a specific sequence of accesses. In an effort to verify a widely used PDF reader, the team found as many security bugs in one week as are usually reported for that software in a full year. In another application, Claude identified a logical error that had gone unnoticed for more than a decade. Anthropic adds that even when a complete proof fails, the attempt can still reveal real bugs.

The company is careful to note that "formally verified" does not mean "error-free." The proofs hold only under defined conditions: a particular processor architecture, single-threaded programs and inputs smaller than 64 MB. Real-world deployments of these libraries often run on different hardware and configurations.

Cost is another constraint. Individual proofs consume hundreds of millions of tokens, and Anthropic has not published total project costs. Still, the company argues that if AI can verify its own code, developers could trust AI-generated software more and spend less time reviewing it, cutting costs across the coding process. A smaller test run indicated that proofs can be reused, and efficiency is improving: Opus 5.5 solves half the proofs using about 40 percent fewer tokens than Opus 5.

The project, in the researchers' framing, shifts the question from whether AI can program to whether it can prove the code it writes is safe. Anthropic expects formal verification with AI to become as practical as standard testing, and Theorem's roadmap already targets critical infrastructure including glibc, OpenSSL and cURL.