Anthropic 用 Claude 对 100+ 开源库做汇编级形式化验证并挖出多年漏网 bug
xennygrimmato_ · x · 2026-10-24
Anthropic 与 Theorem 合作发表论文，展示 LLM 让形式化软件验证首次具备大规模可行性：用 Claude 在超过 100 个真实开源库上，于 RISC-V 汇编层证明安全属性，据称是首个在汇编级对生产软件做 AI 形式化验证的大规模尝试。写证明过程中 Claude 还发现了历经万亿次测试仍未被发现的 bug。
形式方法专家 Hillel Wayne 点评：
- 核心创新在验证更靠后的阶段：传统流程是把源码翻译成定理语言再证明，翻译出错就会证明错误的东西；Anthropic 的做法是把代码编译成汇编，再把汇编编译为定理语言（LPS），只要编译器忠实，即可跳过源码语义分歧问题。
- 仍需信任翻译过程、硬件、OS 与 OCaml 编译器等底层环节。
结论：随着模型能力提升，形式化验证有望成为安全软件开发的标准组成部分。
所属事件:Anthropic 用 Claude 数周为百余开源库完成汇编级形式化验证(23 条相关)→
「安全」频道最新
- 「黑色十月」安全警报：AI 让老漏洞攻击成本降至拿铁价 — LexSokolin · 2026-10-24
- Google 隐私政策修改:Gmail、相册数据或可用于定向广告 — The Verge AI · 2026-10-24
- IBM X-Force 分享 Vibe Fuzzing：用 LLM 引导图输入与程序状态驱动模糊测试 — dyn___ · 2026-10-24
- 希腊立法禁止15岁以下儿童使用社交媒体 — Polymarket · 2026-10-24
- AI 挖漏洞快过修复：2026 前 7 月已录 45207 个新漏洞 — rohanpaul_ai · 2026-10-24
- OpenAI 解雇两名安全研究员，外部监督与防泄露矛盾凸显 — kevinroose · 2026-10-24