Anthropic 的 Claude 现在可以自动编写代码并通过数学方法证明其安全性

Anthropic 联合合作伙伴 Theorem 让 Claude 通过将崩溃测试转化为数学问题并分析机器代码，在几周内自动生成了约 1.8 亿行数学证明代码，用于验证现有软件的正确性。该方法由独立的 Rocq 程序自动检查，并在验证过程中发现了多年传统测试未曾察觉的大量漏洞。不过，这种形式化验证目前仍有严格的使用条件和高昂的计算成本限制。