Claude mathematically proves security of open-source code, finding hundreds of bugs

What this is about

Anthropic worked with its partner Theorem to test whether the AI model Claude can do more than write software: can it also mathematically prove that existing software is correct? To find out, Anthropic's Frontier Red Team had Claude create formal proofs for test programs from 123 open-source libraries. These libraries run in OSS-Fuzz, Google's security project that automatically tests software for crashes. Within a few weeks, the effort produced around 180 million lines of proof code.

Why formal verification has rarely been used

Testing software is laborious, but doable. Proving that a program runs without errors under all circumstances has so far been practically unaffordable. According to Anthropic, a team of specialists needed 20 person-years to formally verify seL4, a small operating system kernel. (Formal verification is the mathematical proof that a program always satisfies a given property.) That's why the method has only been used in extreme cases, such as Airbus avionics software.

How the process works

Existing tests that check software for crashes are translated into a mathematical problem. Claude then works its way through hundreds of thousands of lines of machine code and produces a proof. An independent proof checker called Rocq verifies it automatically. According to Anthropic, human reviewers are hardly needed. The researchers describe the proof generation as "fully autonomous." However, the tools and formal foundations behind it were built by humans at Theorem.

Bugs found

While trying to build the proofs, Claude ran into hundreds of bugs in the software it examined, according to Anthropic, and was allowed to fix them itself. Many of them would hardly have been caught by conventional testing, because they only occur under very specific conditions, such as unusually large input files or a particular sequence of accesses.

• In a widely used PDF reader, the researchers say they found as many security flaws in one week as they would normally find in an entire year.
• In another application, Claude found a logic error that had gone unnoticed for more than ten years.

According to Anthropic, this shows that even attempting a mathematical proof yields useful results, even if the full proof ultimately fails.

Limits and costs

Anthropic concedes that "formally verified" does not mean "bug-free." The proofs only hold under narrow assumptions:

• for one specific processor architecture,
• for single-threaded programs (no parallel execution),
• for inputs under 64 MB.

In practice, the libraries usually run on other hardware and in other configurations. The effort is also considerable: individual proofs can cost hundreds of millions of tokens. (Tokens are the text units in which AI models compute and bill.) Anthropic does not disclose the total cost. A smaller test run showed that newer models need significantly less compute and that proofs can be reused.

Outlook

Anthropic expects formal verification with AI to soon become as practical as today's standard testing. Theorem's roadmap already targets critical infrastructure such as glibc, OpenSSL and cURL.

Our take

The question in the debate over AI and programming is shifting: no longer just "Can AI write code?" but "Can AI prove that its code is secure?" For software development, that could matter more than today's coding assistants. Caveats remain: all of the figures come from Anthropic itself, the conditions for the proofs are narrow, the costs are high and the total spend is unknown. Whether the approach can be extended to multithreading, other hardware and larger inputs is an open question.