DeepMind 用 AI 形式化验证 Signal 协议
先了解这件事
Google DeepMind 研究人员用智能体 AI 对 Signal 协议实际代码的多项关键密码学保证完成形式化验证，并以概念验证形式在四周内完成。DeepMind 称，这是 AI 首次在如此深度上形式化验证广泛部署的密码协议，也是此类协议实现首次被任何方法（无论是否用 AI）形式化验证；相关规范与证明已开源。 验证范围限于 Signal 协议本身，并非对 Signal 整个应用做全面安全审查；Ars Technica 称该分析未发现新漏洞。研究人员还用该方法测试含已知漏洞的旧版实现，AI 识别出问题并判定其未通过验证。 该工作依托新框架 AlphaProof Code。IT之家称，目前尚无法确定这项技术在更大范围推广的实际可行性，此次成果只是研究进程中的一个里程碑。
AI 根据报道生成 · 更新于 3 天前
事件进展
2 个进展
- 11月10日 21:35 · 1 篇报道AI 完成 Signal 协议形式化验证IT之家 · AI：谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性
- 11月10日 20:02 · 3 篇报道AlphaProof Code: a breakthrough in verifying complex softwarThe Decoder：Google DeepMind 推出 AlphaProof Code，四周验证 Signal 加密核心
报道时间线
沿着报道，了解事件的不同侧面。
- The Decoder精选Google DeepMind 推出 AlphaProof Code，四周验证 Signal 加密核心
谷歌 DeepMind 发布 AlphaProof Code，一款符合安全规范的 AI 数学证明软件，并在四周内完成了通常需要数年才能在 Signal 加密协议上完成的验证工作。
- Ars Technica · AI精选Google DeepMind 用 AI 对 Signal 协议关键部分完成数学验证
Google DeepMind 研究人员使用智能体 AI 对 Signal 协议的多项关键密码学保证完成了形式化验证，该项目以概念验证的形式在四周内完成。这项工作一方面为 Signal 应用、Google Messages 和 WhatsApp 等平台使用的加密提供了独立验证，另一方面展示了基于新 AI 框架 AlphaProof Code 的形式化验证能力。
- IT之家 · AI谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性
谷歌 DeepMind 利用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性。分析过程耗时约四周，但未公布具体计算资源规模，目前还无法确定技术在更大范围内推广应用的实际可行性。
- Google DeepMindAlphaProof Code：Google DeepMind 开源多 LLM 智能体框架实现复杂软件深层形式化验证
Google DeepMind 开源 AlphaProof Code 框架，用多 LLM 智能体首次实现广泛部署的 Signal 协议代码深层形式化验证，生成超 600 万行 Lean 证明，仅 1% 代码需人工复核，将专家团队数年工作压缩至四周，并成功识别出两处已知漏洞。
本事件热度走势
- 可比范围当前
- 3
- 可比范围峰值
- 2711月12日 03:00
- 近 24 小时变化
- -74%
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。