【CNMO 科技消息】谷歌 DeepMind 的研究团队完成了对 Signal 消息安全性的形式化验证，并称这是首次由 AI 协助构造出证明，把协议层面的安全保证与一款被广泛使用的密码学实现对应起来。

AI 示意图

这项工作依托 AlphaProof Code 完成，这是一个用于软件形式化规约与验证的多智能体框架。流程上，先由人工引导的智能体编写 Lean 规约、评估机器码语义，再由智能体生成证明，交由 Lean 内核对照规约逐项检查。被验证的对象是 Signal 的后量子 PQXDH 握手和 Triple Ratchet，由此确认了 libsignal 在前向保密、身份认证、密钥泄露后的恢复能力以及握手保密性方面的设计。

这距离有益人工智能基金会今年 4 月提出的构想近了一步：该基金会希望用 Lean 形式化验证 Signal 协议与应用。具体做法是先与多个模型协作，把 Signal 的安全目标转成经人工审阅的数学规约，再让 Gemini Carbon 智能体据此生成 Lean 代码，证明 libsignal 实现的正确性。智能体累计生成 650 万行代码，团队随后做了一轮审计，标出需要人工复核的部分。

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