2026 年 11 月 10 日，Google DeepMind 发布名为 AlphaProof Code 的 AI 软件形式化验证工具，宣布对 Signal 协议的关键密码学安全保证完成了深度数学验证。在外界把这事传成 AI 已经能证明软件绝对没有漏洞之前，有两条冷事实得先按住。截至发布当日，DeepMind 官网还查不到一手的技术报告与公开证明代码库，且这次验证明确排除了整个 Signal 移动应用程序。
真正值得盯住的变化不在宣传口号里。DeepMind 把过去三年攒下的两条技术线拧在了一起：一条是 2023 年 12 月发布的 AlphaCode 2，在 Codeforces 竞技编程中 10 次尝试内解决 43% 的问题、达到第 85 百分位；另一条是 2024 年 7 月拿过国际数学奥林匹克（IMO）银牌级成绩、并于 2025 年 11 月登上《Nature》的 AlphaProof。现在，AI 搜索数学证明的能力从奥数题跨进了工业级安全协议，但当 AI 替人类解决了最苦的怎么证，软件安全真正的死穴反而彻底暴露在证什么之上。
找证明的 AI 与查证明的铁律
很多人看到 AI 形式化验证，第一反应是让大模型看一遍代码然后拍胸脯说没问题。如果真这么干，那叫算命，不叫形式化验证。
工业界做形式化验证，底层工具分两大流派。一派是以 Lean 为代表的交互式定理证明器，靠极小的可信内核去逐行检查显式证明项；另一派是以 Dafny 和 Verus 为代表的求解器驱动工具，Dafny 经由 Boogie 生成验证条件并调用 Z3 等 SMT 求解器，Verus 则针对 Rust 子集结合所有权系统做自动求解。不管哪一派，过去之所以在工业界推不动，是因为哪怕有自动求解器，人类专家依然得手动写出极其繁琐的形式化契约、循环不变量和辅助引理。一行核心代码背后，往往要配十行甚至几十行证明代码。
AlphaProof Code 切入的正是这块最消耗人力的苦力活。它不去替代 Lean、Dafny 或 Verus 的底层检查器，而是充当上游的证明发现者。
这种找证明归 AI、查证明归确定性内核的分工非常聪明。哪怕大模型在搜索策略时产生幻觉，只要交到底层验证器手里通不过检查，就会被直接打回。这也是为什么 DeepMind 能把强化学习用在这里：验证器报错就是最干净的奖励信号。
满分通过的测试与不安全的协议
既然底层验证器不会撒谎，为什么不能说经过 AlphaProof Code 验证的软件就高枕无忧了？问题出在验证器检查的参照系上。
验证器只能证明代码严格符合人类写下的形式化规范（Specification）。韩非子讲过郑人买履的典故，宁信度，无自信也；在形式化验证里，那张写着数学契约的规范就是度，如果尺子本身量错了地方，证明过程哪怕拿到一百分，做出来的依然是一双穿不上的废鞋。
这不是理论上的抬杠，密码学和软件工程界已经踩过一模一样的坑：
- 2026 年 10 月发表的论文《Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation》构造过一个极端案例：一份形式化规范在正负后置条件测试中拿到了满分，但实际上它把前置条件卡得死死的，拒绝了所有必需的有效输入。只看证明成不成功，根本发现不了这份规范是个摆设。
- MIT CSAIL 针对 Signal 双棘轮（Double Ratchet）算法的研究《A More Complete Analysis of the Signal Double Ratchet Algorithm》更是直接戳破过安全定义的幻觉：研究人员找出了 6 个修改版的双棘轮协议，它们在旧的安全定义下全部能被严格证明为安全，但换到更强的真实安全定义下，这 6 个变体实际上全是不安全的。
证明通过只代表代码符合契约，不代表契约挡得住攻击。
再退一步看，哪怕对 Signal 协议选定密码学属性的规范写得滴水不漏，抽象协议模型与用户手机里跑的完整 Signal 客户端之间，还隔着一道实现对应（Implementation Correspondence）的鸿沟。协议本身在数学上不可攻破，不等于客户端的 UI 渲染、网络栈解析、内存管理或操作系统交互没有漏洞。以前几次高危即时通讯软件被攻破，黑客压根没去硬撞双棘轮密码学算法，而是直接打穿了图片解码库或缓存处理。
- 风险.把局部的抽象协议验证当成整个生产级软件的免死金牌，反而容易让工程团队在规范审查与外围代码审计上放松警惕。
接下来怎么验这颗成色
到目前为止，关于 AlphaProof Code 的细节还停留在媒体报道与那页只有全局导航栏的博客空壳上。对于密码学工程团队、操作系统内核开发者以及安全审计机构来说，与其跟着大新闻兴奋，不如拿五把尺子等着 DeepMind 交出一手底牌：
我更在意的是第四层和第五层。在形式化证明代码里，只要偷偷塞进一行未经证明的假设（比如直接假设某个随机数生成或外部接口绝对可靠），后面几千行推导就会瞬间变成空中楼阁。
AlphaProof Code 确实把形式化验证从少数数学家和验证专家的手工作坊里拽了出来。但工具越快，留给人类工程师的问题就越尖锐：以前写不出证明，大家可以赖工具太难用；以后 AI 把证明全包了，万一系统还是被攻破，背锅的就只能是那个连什么叫安全都没定义清楚的写规范的人。接下来最该盯紧的，就是 DeepMind 何时把对 Signal 协议的证明工件开源出来，让外部同行看看它到底用了哪套底层验证器、又在规范里埋了多少前提假设。