# Google DeepMind 公布 AlphaProof Code，完成 Signal 核心密码代码的形式化验证

> 原标题：Introducing AlphaProof Code: a breakthrough in verifying complex software at depth

- 来源：Google DeepMind
- 发布时间：2026-11-10T12:02:28.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/kapajigq1pfr5f26biqz3j802
- 原文：https://deepmind.google/blog/introducing-alphaproof-code/

## 摘要

Google DeepMind 公布 AlphaProof Code 多 LLM 智能体框架，在四周内完成 Signal 协议核心密码代码关键安全属性的形式化验证。

## 推荐理由

Google DeepMind 将 Signal 的形式化验证从协议设计推进到实际代码层面，覆盖设计与实现之间容易隐藏漏洞的落差。

## 锐评

人类专家只要看 1% 的代码，形式化验证这笔账才算能算通。以前给密码实现做数学验证动不动耗时好几年，人工太贵根本没法普及。

DeepMind 这套 agent 四周搞定 Signal 核心代码，生成的证明全交由 Lean 自动检查。大模型负责生成证明，数学工具兜底卡死错误，这个结合我信。基础软件的安全审计成本总算有希望被压下来了。