Claude digs up bugs that survived trillions of tests across open-source software

Claude 形式化验证 123 个库，发现数百隐藏 bug

Anthropic 与 Theorem 用 Claude 对 123 个开源库的 RISC-V 汇编做形式化验证，目标是弥补模糊测试无法穷尽输入的短板。其做法是把已有模糊测试转成数学规范，再为 239 个程序入口点生成在定义条件下不会崩溃的证明；官方称该流程发现大量长期未被自动测试捕获的缺陷。Claude 共生成约 180 million 行证明代码，交由 Rocq 独立检查，无需人工逐行审阅，并可修补漏洞后为新代码重新证明。案例包括解压路径的计数器下溢触发越界写、图像解码器在极端输入下失败、文件句柄序列导致越界读、重新发现 libexpat 已知漏洞，以及绕过文件加载限制的逻辑缺陷。作者强调证明只覆盖单线程、静态链接的 RISC-V 程序和建模 Linux 环境，不能保证未描述属性，未来将通过模型改进与证明复用降低共享库验证成本。

1. 1239 个入口点获得无崩溃证明
2. 2生成约 180M 行证明代码
3. 3保证仅限单线程 RISC-V 程序

为什么重要　它把 LLM 用于编译级证明生成，为共享库安全保证提供可复用路径；但范围受限于 RISC-V 与既定规范。适合　做安全验证、AI 测试与基础库维护的工程师

来源

interestingengineering.com

发布

2026/10/23

作者

Aamir Khollam