Claude 在超 100 个开源库上完成汇编级形式验证

这对软件安全的意义在于，传统防御已不足以应对 AI 能轻易发现并利用的漏洞。形式验证通过将代码转化为数学模型，证明其符合安全规则，但过去成本极高：seL4 内核开发花了 2 人年，验证却花了 20 人年，因此只适用于航空电子等少数关键领域。

Claude 的验证覆盖了 123 个开源库，证明其可执行文件在特定条件下（输入小于 64 MB、单线程静态二进制、固定内存预算、RISC-V 1 CPU 和 Linux 系统）不会崩溃或触发内存安全错误。这些条件有限，但比以往更接近实际可行。

• 验证对象是汇编代码级（RISC-V），而非高级语言，这更接近运行时的真实状态
• 所有证明基于现有编译测试套件自动生成的规格，避免了人工编写规格的高昂成本
• 部分证明已公开，任何人都能验证和复用；Theorem 也发布了 Claude 技能帮助开发者上手

此外，Anthropic 还探索了其他验证方法，包括评估 zlib 压缩算法安全性、证明 Rust 编写的 Python 解释器的行为等价性等。随着模型能力增强，写证明的成本持续下降，验证结果在不同代码库间复用的潜力也会进一步降低总成本。