封面为 AI 生成的概念插画，不是实际设备、系统架构或实验结果。
- 解读日期：2026-10-24
- 资料截止：2026-10-24 20:35:34（北京时间）
10 月 22 日，Anthropic 与 Theorem 公布了一项 AI 辅助软件形式验证研究：团队报告，Claude 为 123 个开源库中的 239 个测试入口生成了安全性质证明。值得关注的，是这些结果开始以可检查的证明文件交付。但“为软件写出证明”到底意味着什么，必须回到具体命题。本文解读的是两天前的公告，不是今天新发生的实验。研究公告
从试很多输入，到证明一个命题
模糊测试会不断生成输入，寻找程序崩溃的情况；形式验证则把要求写成数学命题，再检查推导是否成立。前者擅长找到反例，后者可以在明确前提下，对一个输入范围作整体论证。
这次工作把已有测试入口编译成 RISC-V 二进制，再借助机器与操作系统模型定义要证明的性质，由 Claude 构造证明、Rocq 检查。公告讨论的范围包括小于 64 MB 的输入，并带有单线程、静态程序和固定内存预算等条件。方法与范围
对科研读者而言，重要变化是评价对象变得具体：不只阅读模型写出的“这段代码应该安全”，还可以核对它交付的证明是否对应指定程序和指定要求。模型的语言说服力因此不再是最终裁判。不过，这种分工仍需要有人认真决定：究竟要证明什么？
公告规模与公开样本，必须分开看
本文核对的 OSS Verify 固定版本公开了 25 个库、60 个入口的证明。这是公告成果的子集，不能把较大的研究总数直接当作公众已经拿到的材料数量；更不能把“入口数”写成“完全验证的库数”。公开版本说明
还有一个容易遗漏的细节：该版本的证明比较普通构建与加入运行时错误检测的构建，说明它们在规定范围内不发生所定义的错误，并具有相同的可观察行为。README 明确指出，这批公开证明没有证明终止性，因此不排除程序一直运行而不结束。命题与未覆盖内容
这个区别并不削弱证明本身，却会改变新闻标题。“没有触发指定错误”“一定会结束”“计算结果符合使用者需求”，是不同的要求。若把它们合并成一句“软件不会出问题”，读者就无法知道证据实际支持哪一层结论。
检查器怎样避免证明了另一件事？
检查文档说明，流程会核对二进制文件的 SHA-256，编译证明，并用额外的包装定义要求证明具有目标命题的类型；随后审查所用假设，拒绝允许列表之外的假设。这些步骤分别约束“检查了哪个文件”“证明了哪个命题”和“额外相信了什么”。证明检查机制
这里最有研究价值的启发，是把生成与验收分开。假如模型可以同时修改题目、答案和评分方式，通过检查就未必意味着解决了原问题。固定对象与验收规则，能让失败留下可定位的原因，也让后来者知道应该从哪里重新检查。
同时，文档把额外的 rocqchk 检查列为可选步骤，并说明默认 CI 不执行它。看到“机器检查过”，仍应继续问检查的是哪条流程，不能自行补成“所有检查方式都已通过”。本文阅读了说明，没有实际运行这些检查。默认与可选检查
数学推导正确，现实映射仍要审查
可信基底，就是整套论证仍然依赖的基础组件与假设。项目列出的依赖不只有 Rocq 内核，还包括机器语义、文件转换工具、检查包装逻辑及命题文本。它明确不对二进制与源代码之间的关系作保证；证明指向的是哈希指定的字节。可信基底说明
这意味着，阅读者需要把逻辑是否成立与模型是否贴近真实机器分开。LPS 是对运行 RISC-V 程序的 Linux 进程所作的形式模型，作者明确标注它仍不完整，并记录了范围与假设。某个版本模型中的结论，不能自动转移到另一种运行环境。机器语义及限制
一个直观类比是：可以严格证明某张地图上的路线连通，但仍要检查地图是否遗漏了现实中的断桥。对于软件，版本、执行环境与使用方式共同决定这张“地图”的适用范围。指出边界不是否定形式证明，而是让它的保证能够被正确使用。
接下来，什么结果更有分量？
本文更期待看到三个后续信号：外部检查能否稳定重做，语义模型的假设能否持续接受审计，以及代码更新后维护证明需要多少投入。这些问题分别关系到可检查性、现实适用性和持续使用成本。
规模比较也需要完整分母。后续研究若能同时报告尝试了多少入口、哪些失败、哪些受模型范围限制，以及人工介入与总计算消耗，就更容易判断进步来自哪里。这是本文建议的评价方式，不是声称团队已经完成了这样的对照实验。
当前材料支持一个审慎判断：AI 正在把构造软件证明变成值得系统研究的工作流程，但公开样本尚不足以替整个软件生态作安全保证。本次依据是研究公告和作者技术材料，不能视作多次独立复现，也不作已同行评审论文介绍。本文未重跑证明或审计实现；真正值得持续追踪的，是可核验的保证怎样扩展，同时仍保留清楚的边界。
参考资料与阅读范围
- Anthropic：LLMs are making formal software verification feasible at a much larger scale，2026-10-22。已读公告的方法、规模、限制与相关脚注；未审阅其链接的完整附录，不使用附录中的额外实验结论。公告未给出具体发布时区时间，实验仅描述为持续数周。
- Theorem：OSS Verify README（固定版本）。已核对公开数量、命题说明、未覆盖内容及版本信息；固定提交为
8f5f467，本轮未独立确认其提交时间。 - Theorem：How a proof is checked。已读检查步骤、假设审查、可选检查及 CI 说明，未执行命令。
- Theorem：What you have to trust。已读全文，用于界定可信基底与二进制对象。
- Theorem：LPS: the Linux process semantics。重点阅读状态、设计原则与版本范围；未独立验证形式模型。这些仓库材料与公告属于同一合作项目的证据。
作者作品推广
以下是作者自有产品推广。除了写技术博客，我也独立开发了两款帮助整理日常生活的 App，欢迎了解：
- 日常收支小记：记录日常收支，安排预算与储蓄目标，让每笔账目和计划更清楚。在 App Store 了解。
- 一事微光：根据当下的时间、精力选择小行动，记录完成后的感受，给日常复盘留下一点线索。在 App Store 了解。
更多技术文章与个人作品，欢迎访问我的网站：zffjzz.top。也欢迎分享使用感受，帮助这些小工具逐步改进。