用数学证明聊天软件安全：Signal的疯狂实验

想象一下，你发送的每条消息都被数学定理担保过——不是"我们相信它安全"，而是"这台机器已经验证过，这段代码不可能泄露你的密钥"。Signal正在做这件事，而且用的是一套连微软内部都在跟进的工具链。

这不是学术练习，是拿真实代码开刀

这个项目叫Signal Shot，目标是用Lean证明工具验证Signal协议及其Rust代码实现。不是纸上的数学推导，是跑在服务器上的真实代码。

三方联手推进：Signal工程师Rolfe Schmidt、Beneficial AI Foundation的Max Tegmark，以及Lean FRO开发团队。BAIF的启动声明已公开发布。

参照标杆是四年前的"液态张量实验"（LTE）。Johan Commelin团队用Lean形式化了Clausen和Scholze的液态向量空间主定理。LTE证明了Lean能驾驭现代数学；Signal Shot则要验证Lean能否搞定已部署的软件系统。这一次，AI会参与辅助。

不久前这还不可能。现在所有条件都已齐备。

Aeneas：Son Ho开发的Rust到Lean函数式翻译器，源自他在INRIA的博士论文《通过函数式翻译对Rust程序进行形式化验证》（获2025年法国科学院Gilles Kahn博士论文奖）。Son现为微软剑桥研究院博士后，Aeneas已在微软内部用于SymCrypt项目。它把libsignal的真实Rust代码转成可证明的形式，无需Signal维护两套代码库。

Mathlib与CSLib：Mathlib提供数学基础——椭圆曲线、模格、密码学证明依赖的各种归约。CSLib想成为计算机科学领域的Mathlib，一个共享的Lean基础定义与定理库；Signal Shot所需的密码学原语和协议级定义都将存放于此。

grind与SymM：grind是受SMT启发的自动化策略，整合同余闭包、E-匹配、线性算术和理论求解器。SymM是全新的软件验证单子框架。没有它们，验证libsignal需要大量手工操作；有了它们，验证条件能被高效自动消解。

AI辅助：各团队已在Lean和Mathlib中借助AI进行严肃的数学形式化工作。Hariharan的项目就是一个典型案例——用AI辅助形式化素数定理证明，现已进入Mathlib主线。

Signal Shot的野心很明确：把端到端加密从"我们相信安全"变成"机器验证过安全"。如果成功，这套方法论将适用于任何关键软件系统。