Google（谷歌） DeepMind（谷歌旗下人工智能研究机构）用AlphaProof Code智能体验证Signal协议实际代码
Google（谷歌） DeepMind（谷歌旗下人工智能研究机构）公布AlphaProof Code：一个由多个大语言模型智能体协作的形式化验证框架。
研究团队称，它把Signal加密协议的核心安全目标写成数学规范，由Gemini Carbon驱动的智能体生成超600万行Lean（一种用于机器检查数学证明的编程语言）证明，除约1%经人工复核外均由Lean自动检查，耗时约四周。
这是AI（人工智能）首次在实现层面对广泛部署加密协议做深度形式化验证，但结论仅针对研究者指定的安全属性，不等于协议全部行为已验证。
Google（谷歌） DeepMind研究团队（作者Swarat Chaudhuri、Pushmeet Kohli等）构建了新型智能体框架AlphaProof Code，将人类专业判断与AI（人工智能）智能体结合做深度形式化验证。 流程为：人类专家与研究团队用多种模型把Signal的安全目标翻译为形式化数学规范，每条均由人类专家复核；
随后由Gemini Carbon驱动的智能体生成超600万行Lean证明； 智能体再审计证明并标记出约1%需人工复核的代码，其余由Lean自动检查。 Google DeepMind称整个过程约四周，而历史上此类任务需专家团队数年。
为检验系统能否区分正确与有缺陷代码，研究者把两个此前已修复的真实漏洞重新植入隔离版Signal代码，两次系统均产出经机器检查的“该版本不安全”证明。 Google DeepMind表示将开源其形式化验证工件。
这条报道的价值在“闭环方式”而非单项模型能力：任务被拆成“人定规范—智能体搜索证明—Lean机器检查—人复核被标记部分”，结论由机器检查兜底，压缩了智能体自说自话的空间。 对Agent赛道而言，这是少见的证据：智能体在数学约束下做长链推理，产出可被外部验证器校验的成果，而非仅是生成文本。
边界需看清：验证对象是研究者为Signal核心加密代码设定的安全属性，而非协议或代码库的全部性质； 四周耗时来自Google（谷歌） DeepMind（谷歌旗下人工智能研究机构）口径，无独立复现或第三方计时； 植入两个已知漏洞只说明系统能识别这两类错误，不等于能发现所有缺陷。
后续观察信号
- 技术论文中目标安全属性的完整清单是什么
- Gemini Carbon在证明搜索中的具体分工与模型组合
- Signal官方对验证范围的独立说明