Anthropic与Theorem Labs用Claude完成1.8亿行形式化证明

Anthropic与Theorem Labs利用Claude对RISC-V汇编及生产级开源代码开展形式化验证，数周内覆盖123个代码库和239个测试入口，生成并核验约1.8亿行Rocq证明代码。项目报告称，该方法发现了传统模糊测试长期未覆盖的逻辑漏洞、部分高危缺陷，以及x86处理器层面的硬件问题和相关文档错误。Claude还可辅助生成补丁并继续验证。相关证明已部分公开，验证效率据称约每两个月提升一倍。按当前趋势，投入约1.34亿美元，预计到2027年底完成Nix生态95%机器码验证。