DeepMind 用 AI 智能体形式化验证 Signal 加密协议核心代码

据谷歌 DeepMind 周二（10 日）发布的博客，其研究团队用名为 AlphaProof Code 的多模型智能体框架，对 Signal 协议实际运行代码的关键安全属性完成数学证明，属首次以 AI 对广泛部署的加密协议做如此深度的形式化验证，也是该协议实现首次被任何方法形式化验证。研究人员与多款模型协作，将 Signal 的安全目标转写为形式化数学规范，每条规范均经人类专家审核；随后由 Gemini Carbon 驱动的智能体生成逾 600 万行 Lean 证明代码，并自动审计，仅约 1% 代码需人工复核。验证耗时四周，此类工作过去通常需专家团队数年。该框架证明编译后代码满足消息在设备临时失陷前后均受保护等安全属性。对普通人而言，这意味着日常使用的加密通讯软件底层安全性首次获得机器可检验的数学保证。