Anthropic 让 Claude 自动验证代码安全性并生成数学证明

Anthropic 联合 Theorem 利用 Claude 实现了软件形式化验证的自动化生成，在数周内针对 123 个开源软件库生成约 1.8 亿行数学证明代码。证明由独立程序 Rocq 自动校验且近乎无需人工干预，并在排查过程中发现了大量传统测试遗漏的隐蔽漏洞并完成修复。该技术目前受限于单线程与特定架构环境，算力消耗极高，团队计划未来将其拓展至 OpenSSL 和 glibc 等基础库。