AI研究热点|Anthropic与Theorem公布开源库形式化验证研究

◆Claude生成证明，Rocq检查是否满足指定安全性质

10月22日，Anthropic与Theorem公布形式化软件验证研究。团队称，Claude在修复所发现问题后，为123个OSS-Fuzz开源库的239个入口，证明特定RISC-V编译产物在给定条件下不会触发所定义的崩溃。研究规模是团队披露，不等于每个库的全部功能均已被证明正确。

方法从现有模糊测试入口出发，把可执行程序、系统形式语义和安全条件组成待证明的命题，由Claude生成证明，再由Rocq内核检查。它尝试从反复寻找反例，转向证明输入范围内的性质，但依然依赖命题本身及可信组件是否正确。

公告所述条件包括输入小于64MB、单线程静态RISC-V二进制、Linux环境和固定内存预算。公开证明仓库当前列出25个库的60个入口，属于整项研究公开的部分；其一致性证明也不排除所有不终止执行，不能与“程序一定正常结束”混为一谈。

这些结论不直接覆盖其他架构或任意编译版本，也不能排除规范未描述、检查器未检测的逻辑错误和内存泄漏。形式化验证扩大了可机器检查的证据范围，仍需要保留具体二进制、证明条件及系统语义，才能判断某项安全结论适用在哪里。

◆参考来源

• Anthropic：LLMs are making formal software verification feasible at a much larger scale，2026年10月22日
• Theorem：OSS Verify公开证明、范围与限制
• Theorem：RISC-V与Linux进程形式语义仓库