LLM 让形式化验证第一次能上规模：在 100+ 开源库的汇编层做证明
来源：anthropic.com — 2026-10-22
📋 概述
Anthropic 与 Theorem 合作，用 Claude 在 RISC-V 汇编层为 100 多个真实开源软件库证明了安全性质，这是首次把 AI 形式化验证大规模推到生产软件的汇编层。写证明的过程中，模型还发现了经过数万亿次测试都没暴露的 bug。背景是形式化验证过去贵到不可行：seL4 内核实现花两人年，验证花了二十人年；而现在 LLM 能把这项工作的边际成本压下来，使「证明这段代码没有某类 bug」进入常规开发流程。
🔑 核心要点
- 层级选择很关键：验证在汇编层做，绕过了编译器与语言语义的可信假设。
- 规模：100+ 个真实开源库，全部是生产代码而不是玩具例程。
- 副产品是找 bug：这些 bug 在数万亿次测试运行中都没被发现过。
- 动机是攻防不对称：当模型能轻易把无害 bug 串成关键利用，只有「证明没有 bug」才是终局防御。
💡 金句
While writing the proofs, Claude also discovered bugs that had eluded detection for years, despite trillions of test runs.
👍 0
👎 0
← 返回 Hacker News 首页