我们的团队让 Gemini 4 Carbon 投入一项重大安全挑战：用数学方法证明 Signal 协议底层代码的正确性。
谷歌 DeepMind（Google DeepMind）的研究人员利用 AlphaProof Code，引导智能体将协议验证一路推进到编译后的设备代码，弥合了真实漏洞往往藏身其中的那道缺口。结果如下：
- Gemini 4 Carbon 生成了超过 600 万行经过机器校验的 Lean 证明
- 多年的专家人工验证被压缩到短短几周
- 约 1% 的代码库需要人工审查（其余部分由 Lean 自动检查）
这有助于为构建安全软件解锁可扩展的形式化验证，为从根本上将优势转向防御方奠定基础。我们正将研究成果开源，回馈安全社区。
