Anthropic 用 Claude 自动编写并证明代码安全性

Anthropic 联合 Theorem 让 Claude 自动生成数学证明以验证现有代码的安全性，在数周内产出了约 1.8 亿行数学证明代码并自主修复了数百个漏洞。这种方法能挖掘出传统测试难以发现的深度漏洞，但目前受限于特定的处理器架构、单线程程序和输入大小等严格条件且计算成本高昂。