DeepMind 用 AI 一个月形式化验证 Signal 协议生产代码
sebkrier · x · 2026-11-10
Google DeepMind 宣布用 AlphaProof Code——一个多 LLM agentic 形式化验证框架——数学证明了 Signal 协议底层生产代码的关键安全性质。这是首次有 AI 对广泛部署的密码协议做这种深度的形式化验证，也是该类协议首次被任何方法（无论是否用 AI）验证到这一深度。
工作方式：像研究团队一样分工——人类专家与 AI 协作决定证明什么，一组 AI agent 完成证明。流程为：将 Signal 的安全目标翻译成 Lean 形式化规约（专家逐条审核）；把 Signal 的 Rust 代码编译为机器码并在处理器 Lean 模型上运行；由 prover agent 团队生成证明、gatekeeper 过滤不可信输出。
意义：形式化验证是安全保证的最高标准，但通常被认为不切实际——类似工作量以往可能需要团队数十年，这次仅用约一个月完成，展示了前沿 AI 作为对抗现代网络威胁「力量倍增器」的潜力。
所属事件:DeepMind 发布 AlphaProof Code，首次机器码级验证 Signal 协议(5 条相关)→
「安全」频道最新
- Discord 将公开服务器消息接入 Google 搜索,用户需手动退出 — charis_ai · 2026-11-10
- 间谍丑闻后或掀新一轮出口管制,Nvidia 面临政策新压力 — pstAsiatech · 2026-11-10
- RIDArena 发布：首个评估AI内部背叛行为的测试环境 — jammastergirish · 2026-11-10
- Charlotte Stix 论文梳理「可信 AI」概念的演变史 — ArtificialOther · 2026-11-10
- ExploitGym 获开源 AI 大奖最佳评测项目，曾触发 OpenAI 事件 — dawnsongtweets · 2026-11-10
- 网友实测称 Anthropic 训练时刻意削弱模型 AI 研发能力 — burny_tech · 2026-11-10