10 月 22 日，Anthropic 与 Theorem 公布了一项 AI 辅助形式化验证研究。据团队介绍，Claude 为 123 个开源库的 239 个测试入口生成了机器可检查的证明，目标是排除限定条件下的崩溃。流程从现有模糊测试出发，把程序编译成 RISC-V 二进制，再由 Claude 写证明、Rocq 检查。
适用范围需要看清：研究限定单线程、静态链接、固定内存预算等条件，输入大小也有上限。它没有证明整个库不存在任何错误，更不能直接替代 x86 或 ARM 上的实际验证。
截至 10 月 26 日，公开的 OSS Verify 证明仓库列出的是 25 个库、60 个入口，属于研究成果的子集。仓库同时写明：证明针对特定二进制和系统模型；检测工具发现不了的错误仍可能存在，当前公开证明也不排除程序无限运行。
简短点评
这条路线值得关注的地方，是把 AI 生成的结果交给独立检查器，而不是让模型自己打分。对工程团队来说，下一步更实际的问题是：哪些关键依赖值得先验证，升级后能复用多少证明，验证成本能否进入日常构建流程。模型能写出很长的证明固然有用，规格是否写对、运行环境是否一致，仍然需要认真审查。测试和代码评审也没有因此失去价值。
来源：Anthropic 研究说明（2026-10-22）；Theorem 公开证明与边界说明（2026-10-26 核对）。