Google 用 Gemini 4 Carbon 对 Signal 协议代码完成数学化形式验证并开源结果

Sundar Pichai 宣布 Google 团队用 Gemini 4 Carbon 配合 AlphaProof Code，对 Signal 协议底层代码做数学化验证，验证一直覆盖到编译后的设备代码。Gemini 4 Carbon 生成了超过 6M 行经机器检查的 Lean 证明，把需数年的人工验证压缩到数周，约 1% 的代码库需人工复核，其余由 Lean 自动检查，结果将向安全社区开源。