Google DeepMind研究人员构建了一种全新的智能体框架，成功对Signal加密协议的代码进行了形式化验证。这一长期被视为安全领域“宏大挑战”的任务，如今取得了里程碑式突破。
Signal协议是Signal应用及Google Messages等产品中数十亿私密对话的技术基石。此次突破得益于AlphaProof Code——一种结合人类专业知识与AI智能体的新型框架，旨在以前所未有的深度执行形式化验证。形式化验证通过数学方法证明代码无缺陷，代表了最高级别的安全保障标准，但传统上难度极大且劳动密集。
这是业界首次利用AI对广泛部署的加密协议进行如此深度的形式化验证，也是历史上首次通过任何方法对该类协议的实现层代码完成验证。
人机协作的验证范式
AlphaProof Code是一个多大型语言模型（LLM）智能体框架，其工作模式模拟了研究团队：人类专家与AI共同确定证明目标，AI智能体集群负责执行证明过程。
首先，研究人员与多种模型协作，将Signal的安全目标转化为正式的数学规范，并由人类专家逐一审核。随后，由Gemini Carbon驱动的智能体执行证明，生成了超过600万行Lean代码。Lean是一种用于从数学上证明代码准确性的计算机语言。
在后续阶段，智能体会审查证明过程，并标记出需要人类二次检查的区域。这部分代码仅占整个代码库的1%，极大地节省了时间。由于Lean会自动检查其余部分，专家得以将精力集中在最需要人类判断力的关键环节。
弥合设计与实现的鸿沟
加密协议支撑着从在线银行到网页浏览的数字通信，单个漏洞可能暴露数百万人的数据。尽管专家们几十年来一直对其进行形式化分析，但大多数验证仅停留在设计层面。
DeepMind的智能体更进一步，直接证明了编译后的代码确实满足关键安全属性——例如在设备暂时受威胁前后保护消息不泄露——直至设备运行的确切代码层。现实世界中的漏洞往往隐藏在设计与其实现之间的差距中，弥合这一差距使得证明极其复杂。
即便面对如此复杂性，整个验证过程仅耗时四周，而历史上专家团队完成此类任务通常需要数年。结果证实，Signal的核心加密代码确实提供了专家所指定的安全防护。
为验证AlphaProof Code区分正确代码与缺陷代码的能力，研究人员将两个真实存在且已修复的漏洞重新引入隔离版本的Signal代码中。在这两种情况下，系统均生成了经机器检查的证明，明确指出包含漏洞的版本是不安全的。