AI把代码证明做到汇编级

Anthropic 发文称，用 Claude 在 RISC-V 汇编层给 123 个真实开源库（239 个入口）做出了形式化安全证明，共约 1.8 亿行 Rocq 证明代码，还顺手挖出几个 fuzz 几乎不可能发现的 bug（比如要 20MB 特定布局输入才触发的越界写、libexpat 的 CVE-2026-56132）。结论：以前要专家干几年的活，LLM 现在能规模化做了。
来源：https://www.anthropic.com/research/formal-verification