Anthropic 与形式化验证公司 Theorem 合作，利用 Claude 对 123 个真实开源软件库进行了 RISC-V 汇编代码级的安全性质证明，据称为首次大规模将 AI 形式化验证应用于生产级软件的机器码层面。团队将 Google OSS-Fuzz 的模糊测试自动转化为形式化规约，即证明该测试对任何小于 64MB 的输入都不会崩溃，再由 Claude 撰写证明，由 Rocq 证明检查器机械化核验。数周内，Claude 为 239 个测试入口完成了约 1.8 亿行 Rocq 证明，单个证明平均约 60 万行，覆盖中位长度 1.8 万条指令的二进制程序。在尝试证明的过程中，Claude 发现并修复了数百个漏洞，其中包括模糊测试几乎不可能触发的深层缺陷，如需约 20MB 特定构造输入才能引发的越界写入，并再次发现了 libexpat 中的 CVE-2026-56132。团队还验证了 Linux 内核中的 zlib 实现、用 Rust 编写的 Python 解释器等项目，并在一款广泛使用的 PDF 阅读器中，一周内发现了一整年数量的安全漏洞。研究同时指出局限：证明依赖对 CPU 与操作系统语义的建模假设，且规约范围有限，形式化验证并不等于零漏洞。
事件分析
技术看点：该方法直接在编译后的二进制层面验证，绕开了传统上用可验证语言重写代码库的路径，证明还可复用，共享工作区中的智能体团队比各自为战节省 17% 的 token 开销，证明成本随模型迭代持续下降。产业影响层面，前沿模型自主挖掘并串联漏洞的能力正在快速拉低攻击门槛，而形式化验证规模化给出了可证明的防御范式。开源依赖呈幂律分布，验证少量共享库即可覆盖大量软件，Theorem 已给出验证整个 Nix 生态的路线图。后续值得关注的方向包括 x86 指令集语义建模、多线程与动态链接场景扩展，以及证明结果在安全审计流程中的标准化接入。
核心观点：AI 既能在汇编层自主找漏洞，也能自主证明代码无漏洞，形式化验证正从二十年专家工程变成模型可量产的工业能力。
原文链接：Hacker News
