11 月 10 日，Google DeepMind 发布 AlphaProof Code，用多智能体框架对 Signal 协议的参考实现 libsignal 做了机器码级形式化验证，证明了前向安全、认证、妥协后恢复与握手保密等关键安全性质。DeepMind 称，这类验证此前多停留在设计层面，本次工作推进到实现代码这一层。
AlphaProof Code 把形式化验证拆成研究团队式的分工。人类专家与多个模型协作，把 Signal 的安全目标翻译成形式化数学规范，每条都经人工审查；随后 Gemini Carbon 智能体生成证明，产出约 650 万行机器可检查的 Lean 证明代码，依托 2.6 万行受信规范与 AArch64 语义。整项证明由 5 人团队 4 周完成，类似工作历史上常需专家团队数年。
与多数只分析协议设计的验证不同，DeepMind 把验证推进到编译后的实际机器码，证明设备指令满足既定安全模型。团队把两个已被修复的真实 libsignal 漏洞重新引入隔离版本，结果系统都生成了机器可检查的不安全证明。DeepMind 已开源验证产物供社区审查。
这一结果并非证明 Signal 整个应用无懈可击。群聊、密封发件人、侧信道与多设备状态等仍不在验证范围内，密钥生成也未覆盖。但它展示了一种新的分工，智能体承担证明构造，安全保证仍建立在人工审查的规范与假设之上。
从医疗设备固件到电网软件，这类方法有望把形式化验证带向更多真实系统。DeepMind 表示，要让该技术扩展到全世界软件仍有很长距离，下一步将加强定理、缩减受信基并扩大覆盖范围。