Anthropic的Claude现在写代码并自动证明安全
关键点
- Anthropic和伙伴定理使用Claude在数学上验证了现有的软件代码，并生成其正确性的正式证明。
- 该模型在短短几周内为123个开源图书馆生产了大约1.8亿行的证明代码。 沿途，Claude捕捉到数百个常规测试缺失的虫子。
- 如果AI能写出代码并证明它是正确的，软件自动化可能会大跃进。 Anthropic希望与AI进行正式核查，成为标准测试一样的常规。
Anthropic用Claude来数学上证明现有的代码是正确的。 该方法处理AI生成的软件的一个核心问题，但有严格的实际限制。
证明软件在任何情况下运行无错误，总是令人望而却步。 一个专家团队需要20个人年的时间来正式验证小操作系统内核seL4，因此这种方法被保留给空中客车航空器软件等极端情况。
Anthropic的边疆红队与伙伴定理合作，让Claude代为接管证明工作。 该模型在短短几周内就产生了大约1.8亿行的数学验证代码，借鉴了Google的OSS-Fuzz安全项目中123个开源库的测试程序。
Claude与其写作新的代码，不如通过将崩溃测试转换成数学问题，分析编译的机器代码，产生广泛的证明来验证现有的软件。 一个名为Rocq的独立核查程序自动检查这些证明，根据Anthropic，这个程序几乎不需要人审查。 研究者称其为"完全自主"的证明生成，尽管这些工具和形式基础是人类在定理中建造的。
Claude 捕获多年测试缺失的臭虫
在生成证据的同时，Claude遇到了数百个bug，并被允许自行修复。 研究者们说，许多人会忽略传统的测试，因为他们只在非常具体的条件下出现，比如异常大的输入文件或特定的访问序列。
例如，在核查一个广泛使用的PDF阅读器的过程中，小组在一周内发现的安全漏洞与该软件在一年中的通常报告一样多。 在另一个应用中，Claude抓住了一个逻辑错误，这十几年来一直没有被发现。 即使一个完整的证明最终失败，Anthropic 称，尝试仍然浮出真正的bug.
正式核查能做什么和不能做什么
Anthropic承认，"正式核实"并不意味着"没有错误". 证明只保存在严格的条件下：特定的处理器架构，单行程序，以及64 MB下的投入。 实际上，这些库运行在不同的硬件和不同的配置上。
计算成本非常高个别证据高达数亿 Anthropic不报告项目总成本。 但是如果AI能够验证自己的代码，开发者可以更信任AI生成的软件，并少花时间审查。 这不仅节省了核查的费用，而且节省了整个编码过程的费用。 一次较小的测试运行也显示，证明是可重复使用的，较新的模型越来越有效率：Opus 5.5用比Opus 5少约40%的代币解决了一半的证明。
该项目加强了软件自动化工作。 如果AI能在规定的条件下写出代码并保证它的正确性，问题就从"AI程序可以吗？"转移到"AI能证明它写的代码是安全的吗？". 如果答案是肯定的，后果可能远远超出今天的编码工具。
例：Anthropic预计与AI的正式核实很快会变得和标准测试一样实用，定理的路线图已经针对了glibc,OpenSSL,cURL等关键基础设施。
AI News Without the Hype – 由人类治愈
订阅THE DECODER免费阅读，每周AI通讯，我们独家的"AI雷达"前沿报告每年6次，全面存档访问，访问我们的评论部分。
现在订阅
本文由 AI图鉴自动抓取并翻译，版权归原作者所有；如需查看原文请点下方链接。
Anthropic's Claude now writes code and proves it safe automatically
Key Points
- Anthropic and partner Theorem used Claude to mathematically verify existing software code and generate formal proofs of its correctness.
- The model produced roughly 180 million lines of proof code for 123 open-source libraries in just a few weeks. Along the way, Claude caught hundreds of bugs that conventional testing had missed.
- If AI can write code and prove it's correct, software automation might take a major leap. Anthropic wants formal verification with AI to become as routine as standard testing.
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.
Subscribe now
Auto-fetched and translated by AI Atlas. All rights belong to the original author.