Signal Shot：使用 Lean 验证 Signal 协议及其 Rust 实现的项目

# 平台已就绪 —— Leonardo de Moura Source: https://leodemoura.github.io/blog/2026-4-20-signal-shot-the-platform-is-ready/ ## Signal Shot：平台已就绪 2026-04-20 Signal Shot 是一项公开的登月计划，旨在使用 Lean（https://lean-lang.org/）验证 Signal 协议及其 Rust 实现。不是纸上的数学，而是实际的代码。 这是 Signal（Rolfe Schmidt）、Beneficial AI Foundation（https://www.beneficialaifoundation.org/）（Max Tegmark）和 Lean FRO（https://lean-fro.org/）的联合项目。BAIF 的启动文章在此：https://www.beneficialaifoundation.org/blog/signal-shot。 参照点是液态张量实验（Liquid Tensor Experiment，https://leanprover-community.github.io/blog/posts/lte-final/）。大约四年前，Johan Commelin 的团队在 Lean 中形式化了 Clausen 和 Scholze 的液态向量空间主定理。LTE 证明了 Lean 可以扩展用于现代数学。Signal Shot 则是检验 Lean 现在能否扩展用于已部署的软件。这一次，AI 提供了帮助。 ## 为什么现在可以做成 不久前这还不可能。今天，所有拼图都已摆在同一张桌上。 **Aeneas。**Son Ho（https://www.sonho.fr/）开发的 Rust 到 Lean 的函数式翻译器，最初源自他在 INRIA 的博士论文《通过函数式翻译对 Rust 程序进行形式化验证》（2025 年法国科学院 Gilles Kahn 博士论文奖 accessit）。Son 现就职于 Azure Research Cambridge 担任博士后，Aeneas 已在微软内部用于 SymCrypt。它将 `libsignal` 的真实 Rust 代码转化为我们可以证明其性质的对象，无需让 Signal 维护第二套代码库。 **Mathlib 和 CSLib。**Mathlib（https://github.com/leanprover-community/mathlib4）奠定了数学基础：椭圆曲线、模格、密码学证明所依赖的归约。CSLib（https://www.cslib.io/）旨在成为计算机科学领域的 Mathlib，一个共享的 Lean 基础定义与定理库，Signal Shot 所需的密码学原语和协议级定义将存放于此。 **grind 和 SymM。**`grind`（https://lean-lang.org/doc/reference/latest/The--grind--tactic/#grind-tactic）是我们受 SMT 启发的 tactic：同余闭包、E-匹配、线性算术、理论求解器。`SymM` 是我们为软件验证全新设计的单子（monadic）框架。下文我会详细介绍。没有它们，验证 `libsignal` 将是手动且痛苦的；有了它们，验证条件可以高效地自动消解。 **AI。**各团队已在 Lean 和 Mathlib 中借助大量 AI 辅助进行严肃的数学形式化。Math Inc.（https://www.math.inc/sphere-packing）便是一例：他们最近在数周内（而非数年）自动形式化了 Viazovska 的菲尔兹奖球堆积证明。其他团队也在做类似工作。我预计 Signal Shot 的面貌将与此相似：模型负责自动形式化和常规工作，人类负责选择抽象并发现细微缺陷。 单独任何一块都不够。但合在一起，也许可行。 ## Lean FRO 带来了什么 其他人赖以构建的工具，以及在工具无法扩展时愿意重写其部件的决心。 目前最清晰的例子就是 **SymM**，这是我在 2025 年 12 月 Lean@Google Hackathon（https://sites.google.com/view/lean-at-googl-2025/home）之后立即启动的一个全新单子框架。SymM 从零开始为软件验证而构建。它实现了极大共享项（maximally shared terms）、高效的元变量管理与化简器，以及验证条件生成器所需的若干定制高效 tactic。一个专用的规范化器（canonicalizer）缓存了验证策略在每次证明中重复数千次的工作。 在我们的软件验证基准测试中，SymM 比标准的 `MetaM` 基础设施快数个数量级。它将二次爆炸转化为线性遍历。在那些曾让旧系统陷入停滞的压力测试中，它已带来约 100 倍的加速。Signal Shot 将依赖 Aeneas 来生成 `libsignal` 的验证条件，而 Aeneas 目前正在向 SymM 迁移。 我将于 4 月 20 日在 Lean 巴黎黑客松上做相关演讲，题为 *Scalable Software Verification in Lean 4*（https://leodemoura.github.io/static/svil26/），活动为 SViL2026（https://beneficial-ai-foundation.github.io/SVIL2026/）。Signal Shot 的大部分合作者都会到场。可扩展性是这次登月计划中由我们负责的部分；当 Signal Shot 中的某个环节撞墙时，我们的职责就是移开那堵墙。 内核保持精简且可靠。arena.lean-lang.org（https://arena.lean-lang.org/）上存在多种独立的内核实现。Signal Shot 生成的证明可以被任何审查者独立检验，无需信任编写者。这正是整个登月计划赖以立足的属性。正如陶哲轩所说（https://www.youtube.com/watch?v=Q8Fkpi18QXU&t=3180s），强化学习会找出验证流程中的每一个后门，因此绝不能有任何后门。内核的可靠性就是 AI 安全的基础设施。 ## 我们需要什么 Signal Shot 是开放的。如果你从事软件验证、密码学、协议设计、Rust 或 Lean 本身，这里都有你的位置。 - **Mathlib 贡献者。**密码学原语需要你。 - **CSLib 贡献者。**协议规范需要你。 - **Lean 黑客。**Aeneas 需要帮助以扩展到 `libsignal`。围绕它的验证流水线需要基准测试、回归测试和粘合代码。 - **密码学家。**在任何人在证明之前，我们需要你审视这些定义。 LTE 证明了数学可以在 Lean 中扩展。Signal Shot 对已部署的软件提出的是同一个问题。 我将在 4 月 20 日的 Lean 巴黎黑客松上发布首次更新。