摘要 Google DeepMind公布AlphaProof Code，在指定执行环境和密码学假设下，验证了libsignal一对一会话实现的多项安全性质。关键进展是把协议层的数学保证接到编译后的机器码；人负责审定要证明什么，AI生成证明，Lean检查推理。结果覆盖PQXDH握手和Triple Ratchet相关代码，不等于整个Signal App已被证明安全。
给朋友发出一条加密消息，对方还没上线，服务器先替他存着；过了一会儿，他回复了，双方继续聊天。这里至少有两件事要做对：第一次怎样建立共享秘密，之后怎样不断换密钥。如果设计写得正确，程序却在保存旧会话时多留了一把秘密钥匙，安全保证仍可能落空。
聊天为何要不断换密钥
2026年11月10日，Google DeepMind发布AlphaProof Code。它验证的是libsignal——Signal协议的Rust参考实现。研究团队用标准编译器，把未修改的库接入一个小型命令行程序，编译成AArch64（ARM 64位）机器码，也就是处理器执行的指令，再对这个特定程序做数学证明。
回到那条发给离线朋友的消息：PQXDH是建立共享秘密的握手协议，它把传统密钥协商与后量子机制结合起来；对方预先留在服务器上的公钥，让发信者不用等他上线就能开始。之后由Triple Ratchet（三棘轮）持续派生新的消息密钥，其中结合了传统双棘轮和稀疏后量子棘轮SPQR。
不断换密钥，目的是限制一次泄露的影响。前向保密关注的是：当前密钥泄露后，过去已删除密钥的消息还能否保密；攻破后恢复安全关注的是：攻击者失去设备控制后，双方能否通过后续的新鲜密钥交换，重新让消息对他保密。恢复有条件，并非手机仍被控制时也能藏住屏幕上的明文。身份认证和握手保密，则分别关乎消息对方的身份与初始共享秘密是否得到保护。
把设计上的保证，接到编译后的代码
形式化验证，是先把程序应该满足的性质写成精确的数学规范，再证明程序符合它。普通测试可以检查选中的输入；证明则要覆盖所定义模型和前提内的所有情形。这个区别有用，但前提不能省：如果规范只要求一件很弱的事，证明通过也不会自动得到更强的保障。
Signal此前已有大量验证。Cryspen、Inria和Signal做过PQXDH协议设计的机器检查证明；Cryspen还验证过后量子升级所用ML-KEM实现，以及SPQR核心代码的无崩溃和部分正确性。论文也明确沿用并扩展了Bhargavan等人、Cheval等人的研究。
这次DeepMind所称的“首次”，限定在把协议层安全保证连接到广泛部署协议的未修改实现代码。库里还要处理乱序消息、旧会话、编码格式与状态保存，这些细节都可能让实现偏离设计。直接对编译结果证明，连编译器造成的相关错误也不能靠“源码看起来正确”蒙混过关；代价是需要推理大量寄存器、内存和指令细节。
人决定证明什么，AI交出可检查的证明
AlphaProof Code先让规范撰写智能体参考已有研究，把安全目标写成Lean规范，再由其他智能体挑错、人工修订和批准。Lean是一套能机械检查数学证明的语言与工具；它能查出推理不成立，却不能替人判断“这个目标是否正是我们想要的安全”。
目标获批后，证明团队分工处理各部分。论文称，规范阶段使用了Gemini 4 Carbon和Claude Opus 5.5，证明代码全部由Gemini 4 Carbon智能体团队生成，作者没有手写证明代码。一个关键检查是把提交结果与隔离保存的获批规范比较：不仅定理文字要相同，它依赖的定义也要相同，不能偷偷把条件改弱来过关。
论文报告，五人团队用了四周，生成约650万行Lean证明；被验证的libsignal代码约14万条AArch64指令。这些数字描述的是这次工作的规模。约2.6万行规范与机器语义仍需审视，其中约1.8万行是规范相关定义、约8000行是AArch64语义；Lean内核与底层例程约定等也在信任前提之内。不能把“AI写了650万行”理解成“人从此不用审”。
把旧漏洞放回去，检验规范能否挡住它
一个漂亮的证明也可能证明错了问题。团队做了一次有针对性的检查：把两个已修复的libsignal旧漏洞分别放回隔离版本，重新编译，看看同样的安全要求还能不能成立。
其中一个与旧会话有关：消息在新会话中解密失败，却能在旧会话中解密成功，存在漏洞的程序仍保存了新会话里未经确认的状态，包括不该留下的秘密。另一个涉及握手公钥的检查，可能让不同编码的输入建立共享秘密相同的会话。两种情况下，团队都在Lean中证明了有漏洞的编译版本违反符号安全定理。
这是对规范有效性的回归检查，没有发现新的Signal漏洞；两个反例也不能证明规范已覆盖所有可能问题。它至少要求这套规范能拒绝已知的错误程序，而不是任何版本都可以“证明成功”。
这份证明保护到哪里
这次对象是libsignal v0.105.4及SPQR v1.6.0组成的一对一会话程序，覆盖握手初始化、发送和接收。密钥生成没有被验证，参与方的密钥作为初始条件给定；群聊、完整App、服务器软件和用户设备本身的安全都不在这份结果内。手机App即使用同一套Rust库，迁移结论仍需额外相信编译、链接和系统接口的差异不改变协议行为。
证明还依赖Lean内核及机器、进程模型正确，底层密码算法本身安全。论文的符号模型把密码运算理想化；计算模型则把攻击成功概率联系到底层密码学难题。部分被调用的底层例程用contract（约定输入输出行为）代替，未逐一证明其实际实现。某些输入、会话规模与攻击方式也有限定，例如计算模型不允许向某类后续转为聊天会话的握手注入攻击者自制的首条消息。
后量子范围尤其要分开看：符号证明包含在特定前提下，未来破解传统密钥协商后握手秘密仍受保护的性质；计算证明只覆盖经典攻击者。SPQR旨在提供的攻破后恢复抗量子安全，本次两类棘轮证明都尚未覆盖，不能把“代码包含后量子组件”写成“所有后量子保障都已证明”。
对私密聊天，这项工作增加了核心实现符合特定安全目标的证据。对软件开发，它把一个问题推得更靠前：当AI能写出很长的证明，人必须先讲清楚哪些攻击要被排除、哪些假设能够接受。证明做到了机器码，目标与边界仍要由人认真审定。