Google DeepMind研究人员利用智能体AI（Agentic AI），仅耗时四周便完成了对Signal协议关键加密保证的数学证明，即“形式化验证”。这项概念验证工作被视为密码学与人工智能交叉领域的里程碑式进展。
该成果具有双重意义：一方面，它为保护Signal、Google Messages和WhatsApp等全球主流通信平台的底层密码学提供了独立的额外验证；另一方面，它展示了DeepMind新推出的AI框架AlphaProof Code在形式化验证方面的潜力。
AI加速验证，但仍需人机协作
形式化验证长期被视为软件安全的“圣杯”，通过数学手段确保代码按预期运行且无关键漏洞。在传统模式下，人类将软件特性转化为公式并开发证明的过程极其耗时。智能体AI显著压缩了这一周期，使得对Signal协议的快速评估成为可能。
不过，此次分析的覆盖范围有限，并未涵盖整个Signal移动应用。DeepMind研究科学家Swarat Chaudhuri指出，团队开发了一种“人机协作流程”，允许智能体在多数阶段自我纠正，同时在关键环节引入人类审查。“我们不想让AI自写题目、自证答案，”Chaudhuri表示，“我们需要找到中间地带。”
DeepMind的分析未在审查部分发现新漏洞。但在测试包含已知且已修复漏洞的旧版Signal时，AlphaProof Code成功识别了这些问题，并判定协议未通过验证。研究人员已公开相关规范和证明，以协助社区后续工作。
行业展望与商业化悬而未决
Signal首席技术官Ehren Kret评价称，相比以往针对小部分代码的验证，DeepMind的方法实现了显著扩展，增强了对其隐私保证的信心。Google Cloud首席科学家兼DeepMind研究副总裁Pushmeet Kohli则认为，若能验证关键服务实现的正确性，银行等高风险行业将能彻底消除对漏洞的担忧。
尽管项目效率引人注目，但AI形式化验证的可扩展性及成本效益仍是行业难题。DeepMind研究人员承认，此次快速进展部分得益于Signal基金会此前的验证基础。目前，Google拒绝透露分析成本，也未评论是否有计划推出商业化的形式化验证服务。