AlphaProof Code 验证 Signal：让 AI 写证明，再由机器检查证明

软件通过了测试，仍可能藏着测试没有碰到的漏洞。对加密通信来说，这个缝隙尤其危险：协议在论文里成立，不代表它经过编译、运行在设备上以后，每一步都兑现了原来的安全承诺。

2026年11月10日，Google DeepMind 发布 AlphaProof Code，将 AI 智能体用于 Signal 协议实现的形式化验证。它要做的事情很具体：先明确需要保证的安全性质，再为代码满足这些性质写出数学证明，最后交给验证器检查。DeepMind 的介绍将这项工作定位为深入实际实现层的软件安全研究。

验证到了哪一层？

这次研究针对 libsignal，也就是 Signal 协议的参考实现。团队将 Rust 代码编译为 AArch64 机器码，在 Lean 中描述处理器指令的行为，连接协议层的安全目标与特定构建的执行行为。论文涉及 PQXDH 握手与 Triple Ratchet，讨论前向保密、身份认证、失陷后安全和握手保密等性质。约650万行 Lean 证明代码，是这项工程的一个规模指标。具体定义和适用条件见技术论文。

可以把这里的难点理解为“设计图”和“施工结果”的关系。设计图画出了门锁如何工作，但实际装配可能接错线路。验证协议设计，只回答图纸上的逻辑是否可靠；继续走到实现层，才有机会检查程序有没有在翻译、状态更新或异常处理时偏离图纸。

AI 负责找证明，谁来决定证明对不对？

AlphaProof Code 的工作顺序是：人与智能体共同编写形式化规范，由专家审核；证明智能体尝试建立推导；Lean 检查提交的证明。团队还设置了核对机制，检查证明对应的是否正是获准的规范。这个区分十分关键，避免系统悄悄把难以完成的目标换成更容易成立的目标。

从工程角度看，AI 在这里承担搜索和组织推导的工作。它可以提出错误路径，也可能反复失败；只有通过检查的结果才被接受。与让模型读一段代码后给出“应该安全”的判断相比，这种流程留下了可复核的对象。不过，人仍然需要判断规范有没有遗漏真正关心的问题。

DeepMind 表示，这轮验证过程用了四周。团队还在隔离版本中重新引入两个已修复的历史缺陷，检查系统能否证明有缺陷版本不安全。这是一种有价值的反向测试：验证流程如果只会给出“通过”，就难以让人信服。时间与实验结果属于研究团队披露，不能直接推算成所有项目都能获得同样的效率。

“证明成立”有清楚的边界

最容易误读的地方，是把成果扩展成“Signal 整个应用已经被证明绝对安全”。论文明确限定了构建、运行环境和攻击场景。部分结论依赖底层密码原语与环境行为的假设；侧信道不在相关证明范围内，计算安全部分也不提供对量子攻击者的保证。多设备状态等实际应用情况并未完整纳入。

因此，手机被恶意软件控制、用户遭遇钓鱼、操作系统泄露数据等风险，不能靠这项结果一并消除。形式化验证能给出的保证，与它检查的对象和写下的条件一样具体。读者判断这类研究时，应该同时看“证明了什么”和“把什么当作前提”。

下一步值得看的是维护成本

这项工作的长期价值，可能体现在软件更新之后。今天验证通过的构建，明天改动了依赖、编译器或协议实现，就需要确认旧证明还能覆盖哪些内容。能否持续重跑、发现失效的假设，并把人工审查集中在真正变化的部分，将影响这条路线是否适合日常开发。

对工程团队，一个务实的起点是先选择边界清楚、错误代价高的模块，写明输入、状态变化和安全目标，再讨论验证工具。对于连需求都含糊的系统，增加证明算力并不能自动补上需求。AlphaProof Code 提供的启发在于：当 AI 承担越来越多代码工作时，也可以要求它交出比文字解释更严格的证据。