Claude 生成 1.8 亿行形式化证明，发现传统测试未能捕捉的软件漏洞
Anthropic 与 Theorem Labs 使用 Claude，对生产级开源代码进行 RISC-V 机器码层面的形式化验证。据报道，数周内系统检查了 123 个代码库和 239 个测试入口，生成 1.8 亿行经核验的 Rocq 证明代码。项目据称发现了大规模模糊测试仍未捕捉到的漏洞，以及与 x86 硬件和官方文档有关的问题。Claude 还能够提出补丁并继续验证。结果显示，AI 可能降低形式化验证的工作成本；关于未来成本和验证覆盖范围的预测则仍属估算。
本文来源：AIbase，仅供学习参考，版权归原作者所有。