Google DeepMind公布AlphaProof Code研究框架，通过人类专家与AI智能体协作，为Signal特定构建的机器码建立可由Lean检查的协议级安全证明。研究缩小了协议设计与实际实现之间的验证缺口，但不代表整个Signal应用无漏洞，也未完整证明所有后量子安全承诺。
Google DeepMind于2026年11月10日公布AlphaProof Code研究框架，称通过人类专家与AI智能体协作，为Signal核心加密协议实现的特定机器码建立了可由Lean检查的安全证明。研究的关键进展不是再次论证协议设计，而是把规定的安全性质与实际编译产物连接起来。
根据DeepMind公告及其技术论文，五人团队用四周开展证明工作，生成约650万行Lean证明代码。但这不是整个Signal应用“没有漏洞”的保证：证明针对特定版本、构建和运行环境，依赖人工审核的规格、机器语义、外部例程契约及密码学假设。
这也不是一次Signal现有安全事故的披露。团队重新引入的是两个已经修复的历史漏洞，目的是检验自己的形式化规格能否识别错误实现。
从协议设计，走到编译后的程序
加密协议的设计正确，不代表实现它的软件必然正确。消息如何解析、会话状态如何保存、新旧会话如何切换，都可能在数学设计与实际程序之间引入偏差。
DeepMind此次验证的对象，是libsignal-protocol v0.105.4与spqr v1.6.0中的一对一会话代码。研究人员没有为了方便证明而重写这些库，而是将其接入一个小型命令行封装libsignal-cli，再用标准Rust编译器构建为AArch64 Linux可执行文件。证明覆盖会话建立、发送和接收操作，密钥生成不在验证范围内。
官方技术文档说明，研究把机器指令的执行行为形式化，再证明它与协议安全模型之间的关系。这样，保证不必以“编译器一定正确”为前提；如果编译错误破坏了被证明的性质，相应的机器码证明就无法成立。不过，机器模型能否准确描述现实硬件和Linux行为，仍属于必须信任和审查的基础。
研究方将这项工作定位为：首次为广泛使用、未经修改的加密协议实现建立连接到机器码的协议级安全证明。这一“首次”有明确范围，并不意味着此前没有Signal形式化研究。
AI负责写证明，人类仍须决定证明什么
AlphaProof Code把工作分成两类。首先，人类与智能体把安全要求写成Lean中的定义和定理，并审核其中的假设；随后，证明智能体围绕获批规格构造推导，最终交给Lean内核检查。
两类工作承担不同风险。智能体写出错误推导，检查器应当拒绝；但如果规格本身过弱，正确证明仍可能回答一个没有实际价值的问题。例如，限制攻击者能力过多，或漏写关键安全要求，都可能让程序轻易满足命题。检查推导正确，并不能自动证明问题问得正确。
为防止智能体通过修改定义来降低难度，团队保存一份独立的获批规格，并使用比较工具检查定理及其依赖定义是否一致。涉及规格的修订须经过相应审核，而不是让证明智能体自行改题。
论文披露，约650万行证明之外，读者仍需审查约2.6万行受信任规格及AArch64语义。这个数字也不是全部信任成本：Lean内核、被调用例程的契约、密码学假设，以及部分构建与符号提取工具，仍在保证链条中。证明行数衡量的是产物规模，不能直接换算为安全程度。
证明了哪些安全性质，又没有证明什么
此次工作涉及PQXDH会话握手和Triple Ratchet消息机制。前者用于建立会话秘密，后者让密钥随通信持续更新。
Signal对SPQR的官方解释区分了两个容易混淆的目标：前向保密保护过去的消息，避免后来泄露的密钥暴露此前通信；入侵后安全则要求在满足协议恢复条件后，后续消息能够重新得到保护。Signal将稀疏后量子棘轮SPQR与原有Double Ratchet结合，称为Triple Ratchet。这是此次研究的协议背景，而不是11月10日才推出的新功能。
DeepMind分别给出符号模型和计算模型下的证明。符号模型把密码学操作视为遵守规定规则的抽象对象；计算模型则把攻击成功的优势与底层密码学问题的困难程度联系起来。两者提供不同保证，不能简单合并为“抵御所有攻击”。
尤其需要保留量子安全的限制：计算模型证明只覆盖经典攻击者；符号模型涵盖部分握手秘密在未来量子攻击下的保护，但论文明确表示，其棘轮定理没有证明SPQR额外提供的后量子恢复能力。因此，不能把验证Triple Ratchet实现，改写成已经完整证明所有后量子安全承诺。
其他边界同样实质性。结果针对研究构建的命令行程序，不是Signal手机或桌面应用整体；侧信道攻击不在符号证明的覆盖范围内，计算模型也没有多设备状态，并对攻击者操作、会话和消息作出限制。底层密码学例程有部分通过契约建模，而不是逐一证明其全部实现。把结果迁移到其他平台或构建，还需要确认这些环境保持了受验证代码的行为。
重新放回旧漏洞，是为了检查规格是否有用
团队将两个已修复的libsignal漏洞分别重新引入隔离版本，再重新编译，得到带错误的二进制。一个涉及旧会话试解密与新会话状态保存之间的关系，另一个涉及PQXDH中对X25519密钥的检查。
据技术文档，两种情况下，研究人员都得到由Lean检查的证明，表明错误二进制不满足相应的符号安全定理。这比仅仅观察“某次测试失败”更具体：它为所写规格能够排除这些历史错误提供了证据。
但这仍不是规格完整性的证明。能排除两个已知错误，并不意味着所有潜在漏洞、所有应用行为或所有攻击类型都已被表达进定理。研究方也没有据此宣称当前Signal遭到攻击。
四周的研究，距离日常工程还有多远
五人、四周与数百万行证明，展示的是AI辅助形式化验证的一次研究结果，不是可直接套用到其他项目的工期承诺。论文称，大部分人类精力投入了规格编写与审核。证明生成成本下降后，瓶颈并未消失，而是更集中到如何准确表达安全要求。
这与本站此前报道的Anthropic与Theorem软件二进制验证研究形成呼应：两者都让AI生成证明，再由形式系统检查，但验证对象、机器平台和安全命题不同，不能用证明行数直接比较能力。
DeepMind已公开形式化验证材料，供外部审查。本文核对了公告、论文及技术文档，未重新运行整套证明，因此上述结果应归属于研究团队，而不是独立复现结论。公开研究材料也不等于完整智能体框架已作为通用产品上线。
这项工作的意义，是把“协议按设计应当安全”推进到“特定机器码在明确假设下满足指定性质”。它缩小了设计与实现之间的保证缺口，却没有取消对规格、依赖组件和真实部署环境的审查。对准备采用这类方法的团队，最重要的问题仍是：证明了哪个构建、哪条性质，以及哪些风险尚在证明之外。