DeepMind 用 AI 验证 Signal 核心密码代码

Google DeepMind 在 11 月 10 日介绍 AlphaProof Code，相关研究于 11 日获多家媒体报道。研究人员结合人类审查与 AI 智能体，验证 Signal 协议部分核心实现的安全性质。

团队先把安全目标写成形式规范，再让智能体构造由 Lean 检查的证明，并将核对延伸到实际执行的机器代码。官方表示，项目历时四周，产生超过 600 万行 Lean 证明代码。

团队也把两个已经修复的历史缺陷重新加入隔离版本，检查系统能否识别不安全实现。工作验证的是明确规定的性质与代码范围，不意味着已经证明整个 Signal 应用绝无漏洞。

来源：Google DeepMind 原文；Google DeepMind 研究公告。

图片来源：Google DeepMind。