如何审查 AI 形式化验证的可信边界

AI 生成了几百万行证明，代码就能放心上线吗？这篇文章借 AlphaProof Code 验证 Signal 密码学核心的案例，给出的答案是：先看证明覆盖哪里、依赖什么假设，再看结果能否复查，以及错误输入能否被识别。

按原文描述，AI 承担了大量证明编写工作，Lean 内核负责检查，但人仍要决定究竟证明什么。对程序员最有用的，是这套判断「AI 已验证」是否可信的检查方法。

证明通过了，到底能保证什么

原文称，Google DeepMind 于 2026 年 11 月 10 日公布 AlphaProof Code，用四周完成了对 libsignal v0.105.4 密码学核心的形式化验证，验证对象深入到编译后的 AArch64 机器码。

形式化验证，可以理解为：把安全要求写成精确的数学命题，再检查代码是否满足这些命题。它的保证始终受命题和模型约束。

这次证明包含十个符号定理，涉及前向保密、失陷后安全、发起方与响应方保密、认证，以及 PQXDH 的 Theorem 1 的五个推论。范围限定为一对一会话、PQXDH 握手、Triple Ratchet 和 AArch64。

群聊、关联设备状态、操作系统、手机本身，以及密码学原语，都没有被一并证明。密码学原语被当作模型假设。原文还明确提到：SPQR 的恢复能力没有建立后量子保证。

证明的可信度，必须连同它的适用边界一起阅读。

因此，引用「Signal 已获验证」之前，应先能写清楚：哪个版本、哪种架构、哪些协议流程，以及哪些条件被直接假定成立。

怎样判断这份证明值得信任

作者提出了两个实用检查：证明产物能否复查，系统能否识别已知错误。

按原文，公开仓库为 google-deepmind/code-verification，对应提交 808b4b7，使用 Apache 2.0 许可证。Gemini 4 Carbon 驱动的智能体生成了超过 650 万行 Lean 证明，每份证明都经过 Lean 内核检查。

原文引用的独立复查者在次日统计出：11,323 个文件，共 7,528,293 行，并称主要证明中没有 sorry。这里的 sorry 可以理解为暂时跳过证明义务的占位入口，主要证明里没有它，是必要的检查项。

复查者还用 wc -l 统计 .lean 文件，并搜索 sorry、native_decide 和额外公理。不过，搜索只是初筛：找到这些内容后，仍要判断它们是否进入关键证明的依赖链。

原文称，基础检查十分钟可做；重新运行内核需要数小时、15–34 GiB 峰值内存，并固定 Lean 4 v4.34.0 和 Rust 1.98.1。读仓库与完整重建，是两种不同成本的检查。

另一个证据更容易理解：DeepMind 把两个真实存在、此前已修复的漏洞重新放进隔离副本，系统给出了经过机器检查的违规发现。

这是有价值的反例测试。不过，识别两个植入漏洞，不能推导出它能发现所有漏洞。作者建议向「AI 验证」供应商索要已知错误输入及对应结果，这条建议很值得保留。

四周完成验证，成本到底去了哪里

四周这个数字容易吸引注意力，但作者认为，预算更应该看证明规模和人工职责。

按作者基于 DeepMind 数据所做的计算，650 万行证明对应约 140,000 条机器指令，平均每条指令约 46 行证明，或每 KB 源码约 11,600 行证明。560 KB 代码对应 529 MB 证明产物，体积接近千倍。

这些比例是本案例的结果，不能直接当成其他项目的报价公式。它们至少提醒团队：证明产物的存储、检查和维护，也要计入成本。

650 万行分摊到 28 天，约为每天 232,000 行。原文描述的执行方式是：在单机上运行 40–80 个智能体，每个运行 24–72 小时。这里依靠的是持续生成与确定性检查组成的流水线。

人工工作也没有消失。原文给出的可信基础约为 26,000 行，包括约 18,000 行规格，以及约 8,000 行 AArch64 语义；规格连同文档则为 28,000 行。人类审查了全部规格，作者团队成员没有编写证明代码。

原文据此称，人工审查量约占产物的 0.4%，其余 99.6% 由 Lean 内核检查。但这些比例不能解释成安全责任也只剩 0.4%。规格决定系统究竟承诺什么，写漏一条要求，证明再严密也补不回来。

我的判断

我认同作者把注意力放到规格、公开产物和反例测试上。这比单看模型成绩表，更接近工程团队真正需要的证据。

但原文提供的是案例转述和作者的检查建议，没有给出与传统形式化验证、模糊测试或人工审计的同条件成本对照。四周是否具有普遍参考价值、智能体消耗了多少计算资源、代码升级后需要重做多少证明，文中都没说清楚。

「人不能让机器代写规格」也说得过满。机器可以辅助起草，关键在于最终语义需要人负责确认；原文真正支撑的是人类审查了全部规格。

形式化验证适合对明确性质给出强保证，fuzzing 擅长探索异常输入，渗透测试和运行监控覆盖实际环境。它们各自覆盖的边界不同。这次验证不能成为撤掉现有安全措施的理由。

能拿来做什么

• 在 Node 服务或日常 AI 编程任务中，先把关键约束写清楚，例如哪些状态迁移必须被拒绝，再让 AI 实现，并围绕这些约束检查结果。
• 遇到「AI 已验证」的工具或依赖时，要求提供版本、验证范围、假设、公开产物和复现步骤，区分代码检查、测试通过与形式化证明。
• 为自己的检查流程准备已知错误样本，确认它能拒绝违反要求的实现，并保留 fuzzing、依赖检查、渗透测试与运行监控。