The Decoder· Matthias Bastian·· 6 小时前精选AI 评分79
Anthropic 用 Claude 自动形式化验证现有代码并发现漏洞
Anthropic's Claude now writes code and proves it safe automatically
AI 导读
Anthropic 使用 Claude 为现有软件生成数学证明，并由 Rocq 自动检查，项目在数周内产出约 1.8 亿行证明代码。过程中 Claude 发现并修复数百个漏洞，但证明只适用于特定处理器架构、单线程程序和小于 64 MB 的输入，单项证明还可能消耗数亿个 tokens。
推荐理由
这项工作展示了 Claude 将崩溃测试转为形式化证明并发现旧漏洞的做法，同时明确列出处理器架构、线程和输入大小等适用限制。
来源：The Decoder · the-decoder.com