爆料称 DeepMind 用 AI 形式化验证 Signal 代码，仅花四周

IgorCarron · x · 2026-11-11

X 用户 Igor Carron 转引一则爆料：称 Google DeepMind 的 agent（文中称 Gemini Carbon 驱动、基于 AlphaProof Code）对 Signal 这一广泛部署的加密协议的实际机器代码完成了数学化安全验证，属首次在如此深度上验证主流密码协议。据称整个过程仅用四周，而传统上需要专家团队数年；生成了超过 600 万行 Lean 证明代码，仅将代码库约 1% 标记为需人工复核，并数学证明了两个此前已修复的 bug 确实导致代码不安全。注意：该说法来自第三方转述，尚无 DeepMind 或 Signal 官方确认。