Anthropic表示，Claude在 123 开源库中证明了安全性

Anthropic表示，其Claude模型能够在123开源库中为编译代码中安全属性生成形式证明，公司称这是迈向使形式化软件验证在更大范围内实现的一步。在2026年10月22日发布的研究文章中，Anthropic表示这项工作还揭示了多年来未被注意的漏洞。

证据与背景

据Anthropic介绍，Claude证明了在项目建模条件下，跨123库的239入口点64在MB以下的任何输入都不会崩溃。公司表示，这些证明是在RISC-V二进制文件上的汇编代码层面应用的，并使用定理的形式语义处理RISC-V和Linux进程行为。Anthropic表示，该项目涵盖了现实世界的开源软件，包括谷歌OSS-Fuzz计划中的库，据其了解，这是首次大规模使用人工智能在汇编代码层面将形式验证应用于生产软件。

公司表示，这些证明是在数周内生成的，Claude 还修补了过程中遇到的漏洞。举例中包括由罕见的 20 MB 输入布局触发的越界写入、需要 64 MB 输入和超过 2 GB 内存的图像解码器读取越界、跨二文件句柄与特定调用序列相关的崩溃，以及 libexpat 中重新发现CVE-2026-56132。Anthropic 还表示，此次尝试发现了未导致软件崩溃的逻辑错误一包括文件访问限制功能并非总是被执行的情况。

公司表示，这些证明是有条件的，并不意味着软件是无bug的。其自身的限制部分表示，这些保证依赖于建模假设，包括在RISC-V Linux上运行的单线程静态二进制，且该工作并不涵盖所有入口点或软件在生产环境中的所有使用方式。Anthropic表示，剩余的不确定性集中在可信组件中：RISC-V和Linux语义、定理陈述以及Rocq证明检查器。

为什么重要

Anthropic将这项工作定位为大型语言模型能够降低形式验证成本的证据，而形式验证历来需要高度专业化的努力，且通常局限于关键任务系统。文章称，大型模型在某些验证任务中需要更少的令牌，而共享证明组件减少了相关项目间的重复。公司还表示计划发布部分证明，定理将为其他开源项目提供相同的流程。

研究与更广泛的行业研究一致，表明形式验证可以补充而非取代测试。但正如Anthropic本身指出的，证明的价值仍取决于规范和机器模型是否符合现实，许多部署假设仍超出验证声明的范围。