Anthropic 利用 Claude 自动证明代码安全性

Anthropic 团队与 Theorem 合作，利用 Claude 对现有代码进行形式化验证以证明其安全性。Claude 生成约1.8亿行证明代码，在验证PDF读取器时一周内发现的安全漏洞数量相当于平时一年报告的水平，还修复了数百个潜在Bug。该过程依赖 Rocq 自动检查证明，目前受限于单线程程序、特定处理器架构和小于64MB的输入，单次证明消耗数百万至上百万个token。