Anthropic 让 Claude 自动为现有代码生成安全证明

Anthropic used Claude to mathematically prove that existing code is correct. The approach tackles a core problem with AI-generated software but comes with strict practical limits.

Proving that software runs error-free under all circumstances has always been prohibitively expensive. A team of specialists needed 20 person-years just to formally verify the small operating system kernel seL4, so the method was reserved for extreme cases like Airbus avionics software.

Anthropic's Frontier Red Team, working with partner Theorem, let Claude take over the proof work instead. The model produced roughly 180 million lines of mathematical proof code in just a few weeks, drawing on test programs from 123 open-source libraries in Google's OSS-Fuzz security project.

Rather than writing new code, Claude verified existing software by translating crash tests into mathematical problems, analyzing the compiled machine code, and producing extensive proofs. An independent verification program called Rocq automatically checks those proofs, and according to Anthropic, the process needs almost no human reviewers. The researchers call it "fully autonomous" proof generation, though the tools and formal foundations were built by humans at Theorem.

Claude catches bugs that years of testing missed

While generating proofs, Claude ran into hundreds of bugs and was allowed to fix them itself. Many would have slipped past conventional testing because they only show up under very specific conditions, like unusually large input files or a particular sequence of accesses, the researchers say.

During an effort to verify a widely used PDF reader, for example, the team found as many security bugs in one week as are typically reported for that software in an entire year. In another application, Claude caught a logical error that had gone undetected for over a decade. Even when a complete proof ultimately fails, Anthropic says, the attempt still surfaces real bugs.

What formal verification can and can't do

Anthropic acknowledges that "formally verified" doesn't mean "error-free." The proofs only hold under strict conditions: a specific processor architecture, single-threaded programs, and inputs under 64 MB. In practice, these libraries run on different hardware and in different configurations.

The compute cost is steep, with individual proofs running up hundreds of millions of tokens. Anthropic doesn't report total project costs. But if AI can verify its own code, developers can trust AI-generated software more and spend less time reviewing it. That saves costs not just on verification but on the entire coding process. A smaller test run also showed that proofs are reusable, and newer models are getting more efficient: Opus 5.5 solves half the proofs with about 40 percent fewer tokens than Opus 5.

The project strengthens the case for software automation. If AI can write code and guarantee its correctness under defined conditions, the question shifts from "Can AI program?" to "Can AI prove that the code it writes is safe?" If the answer is yes, the consequences could go well beyond today's coding tools.

Case in point: Anthropic expects formal verification with AI will soon become as practical as standard testing, and Theorem's roadmap already targets critical infrastructure like glibc, OpenSSL, and cURL.

AI News Without the Hype – Curated by Humans

Subscribe to THE DECODER for ad-free reading, a weekly AI newsletter, our exclusive "AI Radar" frontier report six times a year, full archive access, and access to our comment section.