DeepMind称AI验证Signal协议机器码

事件综述根据 3 篇报道整理，11月11日更新

Google DeepMind 团队宣布，用其智能体验证框架 AlphaProof Code 对 Signal 消息协议的生产代码完成形式化验证，证明该协议底层机器码的关键安全属性。该框架运行在包括 Gemini Carbon 在内的 LLM 上，验证对象是设备上实际运行的代码，而非模型或规范。DeepMind 称这是首次有广泛部署协议的真实生产代码被验证到这一深度，并表示将开源形式化规范与验证产物。 Google CEO 桑达尔·皮查伊称，Gemini 4 Carbon 生成超过 600 万行经机器校验的 Lean 证明，把原本需要数年的专家人工验证压缩到数周，约 1% 的代码库需要人工复核，其余由 Lean 自动检查。 据 IT之家报道，整个分析过程耗时约四周，验证针对的是 Signal 加密协议本身，而非对 Signal 应用的整体安全审查。团队还用该方法测试了含已知漏洞的旧版协议实现，AI 识别出问题并判定其未通过验证。谷歌表示，尚无法确定该技术在更大范围推广的实际可行性，也未公布所需算力规模。上述结论来自 DeepMind 和谷歌方面的声明，报道未提及独立第三方复核。

综述由模型根据报道生成，细节以各篇原文为准。