Signal加密通过AI数学验证，形式化验证迎来拐点

在隐私通讯领域，Signal一直是端到端加密的代名词。近日，这家非营利组织完成了一项颇具象征意义的实验：其加密协议通过了一次由AI辅助的数学验证。据Ars Technica报道，这个历时四周的项目由安全研究者与AI工具协同完成，目标是用形式化方法检验Signal协议核心加密逻辑是否真正符合设计预期。消息本身不算轰动，但它释放的信号值得玩味——AI或许正在把形式化验证从学术象牙塔推向工程一线。

为什么加密需要一次“数学体检”

大多数软件测试依靠“输入—观察—判断”的经验路径：跑一批用例，看结果对不对。但密码学协议不能只靠抽样验证，因为攻击者恰恰会寻找那些测试没覆盖到的边界条件。形式化验证走的是另一条路：把协议的安全属性写成数学命题，再用定理证明器逐步推导，确认代码在逻辑上不存在违背命题的路径。简单说，它不是“试了很多次都没问题”，而是“从数学上证明不可能有问题”。

问题在于，这条路极其昂贵。写形式化规约、构造证明、维护证明脚本，往往需要受过专门训练的专家耗费数月甚至数年。正因如此，形式化验证长期局限于内核、飞控、密码库等少数高价值场景。普通开源项目即便知道它好，也往往用不起。

AI如何改变验证的游戏规则

这次Signal项目的关键看点，是AI在证明过程中扮演了实质性角色。按照报道的描述，AI工具帮助完成了部分证明构造与检查工作，把过去需要人工反复推导的环节压缩到四周之内。这背后对应着近年一个清晰的技术趋势：大语言模型与自动定理证明的结合正在加速。模型可以协助把自然语言描述的安全目标转写为形式化规约，可以搜索已有的引理和证明模式，也可以在证明卡住时给出候选策略。

“这个为期四周的项目暗示，AI可能让形式化验证变得实用得多。”

需要强调的是，这不意味着AI可以独立“证明安全”。形式化验证的难点往往不在最后那几步推导，而在于把模糊的安全直觉准确地形式化，以及在证明失败时判断究竟是协议有漏洞，还是规约写错了。AI目前更像是放大器：它让熟练的验证工程师效率更高，也让更多团队有机会迈过入门门槛。

为什么是Signal，这件事影响有多大

Signal协议并非只服务于自家应用。它的双棘轮机制和端到端加密设计，被WhatsApp、Google Messages等数十亿级用户规模的产品采用或借鉴。换句话说，对Signal加密逻辑的任何形式化检验，其辐射范围都远超一款通讯软件本身。如果这类验证能够常态化、低成本地开展，整个加密通讯生态的信任基础都会更加坚实。

更现实的启示在于流程层面。过去，形式化验证通常发生在协议设计定稿之后，作为一次性的“验收”。而AI辅助降低了单次验证的成本，使其有可能嵌入持续集成流程：每次代码变更都跑一遍轻量级证明检查，像单元测试一样成为日常。这种“验证左移”对密码学软件尤其有价值，因为加密实现中的细微改动都可能引入灾难性缺陷。

编者按：冷静看待“AI验证”的光环

当然，四周完成验证不等于一劳永逸。形式化验证只能证明“代码符合规约”，无法保证规约本身抓住了所有安全需求；AI生成的证明也需要人工审查，否则可能把模型的幻觉带进信任链。此外，这次项目披露的细节有限，AI具体承担了多少工作量、证明覆盖了协议的哪些部分，仍有待更完整的技术报告来回答。

但方向已经足够清晰。形式化验证长期被困在“高价值、高成本、少数专家”的三角里，而AI正在同时撬动成本和人力两个支点。Signal的这次尝试未必是终点，却很可能是一个被后来者反复引用的起点：当数学证明变得便宜，软件安全的默认标准也会随之抬高。

本文编译自Ars Technica