开发者用 Lean 4 形式化验证 Rust Web 应用正确性

形式化验证 Rust Web 开发 安全 用 Lean 4 证明 Rust Web 应用的正确性 Hideaki Takahashi 阅读时长 9 分钟· 2026 年 10 月 6 日

Claude Code、Codex 这类 AI 编码代理，让我们能在极短时间内构建出规模惊人的 Web 应用。

但随着写代码的速度越来越快，另一个问题也变得愈发重要：“我们怎么知道生成的代码确实按照我们的意图运行？”

当然，我们可以写单元测试。但测试通常只能告诉我们：“对于我们尝试过的这些输入，程序行为是正确的。”

然而有时候，我们想要强得多的保证，比如：

这些性质我们希望对所有可能的输入都成立，而不只是对有限的一组测试用例成立。

这正是形式化验证的用武之地。本文将展示如何用 Rust 编写 Web 应用的核心逻辑，自动把该逻辑翻译成 Lean 4，并针对实际程序证明相关性质。

我们将使用 h5i-app，这是一个作为 h5i Web 安全项目的一部分构建的 Rust 框架（仓库：https://github.com/h5i-dev/h5i）。

Lean 4 既是一门编程语言，也是一个交互式证明助手系统，我们可以在其中写下数学命题和机器可检查的证明。

假设我们在测试一个简单的函数。用普通测试，我们可能会检查这样一些例子：

1 + 1 = 2 100 + 1 = 101

Lean 则允许我们陈述强得多的命题：

对于每个自然数 n， n + 1 大于 n。

我们不再检查若干个具体值，而是陈述一个对所有可能取值进行量化的命题，然后由 Lean 验证该证明在逻辑上是否正确。

对于一个 Web 应用，我们可能想证明类似这样的命题：

对于任意一对用户 A 和 B， 由 A 执行的操作无法修改 B 的数据。

如果 Lean 的内核接受了该证明，那么在模型中所编码的假设之下，该性质就已经得到了机器验证。

然而，一个实际问题是：我们如何确保实际的 Rust 实现与 Lean 4 模型之间的等价性？为了缩小这一差距，h5i-app 使用了 Aeneas，它能把 Rust 程序翻译成 Lean。

因此，整个工作流是这样的：

用 Rust 编写应用逻辑 ↓ 自动将其翻译成 Lean 4 ↓ 把期望的性质陈述为定理 ↓ 在 Lean 中证明它们

关键在于，证明是与 Rust 实现本身相连的，而不是与一个单独维护的模型相连。

h5i-app 是 h5i 的一部分，后者是一个面向代理的原生 Web 安全工作区。h5i 从两个互补的方向处理 Web 安全：1）像专业红队一样发现 bug；2）通过形式化验证证明性质。

h5i-app 负责第二部分，它围绕 Axum 设计——Axum 是 Rust 中最流行的 Web 框架之一——让开发者能够把安全关键的应用逻辑隔离在 Rust 中，并在 Lean 4 中验证该逻辑。

目标并不是用 Lean 重写整个 Web 应用。你仍然照常使用 Rust 编写应用。相反，你要把正确性最关键的部分——授权、状态转换、业务规则和数据库写入——分离出来，并让这些部分适合验证。

从概念上讲，架构是这样的：

HTTP 请求 │ ▼ ┌──────────────┐ │ Axum / HTTP │ │ 传输层 │ └──────┬───────┘ │ ▼ ┌──────────────────────┐ │ Rust 内核 │ │ │ │ 授权 │ │ 业务逻辑 │ │ 状态转换 │ └──────┬───────────────┘ │ │ Aeneas ▼ ┌──────────────────────┐ │ Lean 4 │ │ │ │ 定理 / 证明 │ └──────────────────────┘ │ ▼ ┌──────────────────────┐ │ 存储 / PostgreSQL │ └──────────────────────┘

核心思想是那个内核，它接收：

当前状态 + 执行操作的用户 + 请求的操作

并决定：

允许 / 拒绝 + 新状态 + 响应

由于内核是用相对纯粹的 Rust 编写的，与 HTTP 和 SQL 分离，Aeneas 可以将其翻译成 Lean。

我们来构建一个小例子。我们将创建一个行为类似计算器记忆功能的极简应用。

h5i app new calculator cd calculator-01

生成的结构大致如下：

calculator/ ├── h5i-app.toml ├── kernel/ │ └── src/ │ └── lib.rs └── proofs/ ├── Theorems.lean └── generated/

重要的部分有：

kernel/src/lib.rs 用 Rust 编写的应用逻辑

proofs/Theorems.lean 我们想要证明的性质

proofs/generated/ 从 Rust 自动生成的 Lean 代码

h5i-app.toml 提取、验证和变异测试的配置

第 1 步：定义谁在执行操作

首先，修改 kernel/src/lib.rs，定义一个表示已认证用户的 Principal：

#[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct Principal { pub org: u64, pub user: u64,

这里我们可以理解为 org 是组织 ID，user 是该组织内的用户 ID。

接下来，我们定义应用存储的数据。h5i-app 提供了一个 schema! 宏，用一种在 Rust、Lean 和 PostgreSQL 之间共享的形式来描述 schema。

h5i_app_schema::schema! { mapping calc_tables for calculator_kernel, lean "../proofs/generated/Schema.lean"; #[derive(Clone, Debug, Default, PartialEq, Eq)] pub struct Snapshot { memories: Vec<Memory>, #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct Memory in "memories" { key { user: u64 } value: u64

你可以把 Snapshot 理解为当前相关的数据库状态。每个 Memory 表示一个用户的计算器数值。schema 定义还会用于生成诸如以下机制：

Rust 行操作 数据库转换 SQL 写入表示 Lean schema 定义

这很有用，因为否则我们就得为 Rust、SQL 和 Lean 分别维护各自的数据模型描述。

现在我们来编写核心应用逻辑。从概念上讲，内核暴露的函数类似：

fn transition( actor: &Principal, snap: &Snapshot, cmd: &Command,

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）