想象一下：你用的加密聊天软件，它的安全性不是靠"我们相信工程师"，而是像数学定理一样被严格证明。Signal正在干这件事——不是证明纸上的协议设计，是证明实际跑的Rust代码。

这个项目叫Signal Shot。合作方包括Signal的Rolfe Schmidt、有益人工智能基金会（Max Tegmark）和Lean FRO。目标是用Lean形式化验证工具，给Signal协议和它的Rust实现一个数学级别的安全背书。

参考点是四年前的"液态张量实验"（LTE）。Johan Commelin团队用Lean形式化了Clausen和Scholze的液态向量空间主定理，证明Lean能搞定现代数学。Signal Shot则要测试：Lean现在能不能搞定已部署的软件？这次AI会帮忙。

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

核心工具叫Aeneas——Son Ho的Rust到Lean函数式翻译器，源自他在INRIA的博士论文《通过函数式翻译对Rust程序进行形式化验证》。Son现在是微软剑桥研究院博士后，Aeneas已在微软SymCrypt项目内部使用。它能把libsignal的实际Rust代码变成可证明的对象，无需Signal维护第二套代码库。

数学基础靠Mathlib，涵盖椭圆曲线、模格等密码证明所需的数学工具。CSLib则想成为计算机科学界的Mathlib，Signal Shot需要的密码学原语和协议级定义都会放在这里。

验证效率靠grind和SymM。grind是SMT风格的自动化策略，SymM是新的软件验证单态框架。没有它们，验证libsignal又慢又痛苦；有了它们，验证条件能被高效消解。

AI也在深度参与。已有团队借助AI在Lean和Mathlib中完成严肃的数学形式化工作。