Google DeepMind 完成 Signal 协议的形式化验证，首次由 AI 协助构建安全证明

Google DeepMind 的研究团队完成了对 Signal 消息安全性的形式化验证，并称这首次由人工智能协助构造出证明，将协议层面的安全保证与一款被广泛使用的密码学实现相对应。

这项工作依托 AlphaProof Code 完成，这是一个用于软件形式化规约与验证的多智能体框架。流程上，先由人工引导的智能体编写 Lean 规约、评估机器码语义，再由智能体生成证明，交由 Lean 内核对照规约逐项检查。

被验证的对象是 Signal 的后量子 PQXDH 握手和 Triple Ratchet，从而确认了 libsignal 在前向保密、身份认证、密钥泄露后的恢复能力以及握手保密性方面的设计。这距离有益人工智能基金会今年 4 月提出的构想又近了一步：该基金会希望用 Lean 形式化验证 Signal 协议与应用。

具体做法是先与多个模型协作，将 Signal 的安全目标转成经人工审阅的数学规约，再让 Gemini Carbon 智能体据此生成 Lean 代码，证明 libsignal 实现的正确性。智能体累计生成 650 万行代码，团队随后进行了一轮审计，标出需要人工复核的部分。

Google DeepMind 成功验证 Signal 消息安全性

“这是一套从根本上为人和人工智能协作而构建的系统，” Google DeepMind 研究科学家、德克萨斯大学奥斯汀分校教授 Swarat Chaudhuri 说。他表示，传统做法是数学家将定义清晰的问题交给人工智能去证明，而这次首先要弄清楚该证明什么。