一、起因
昨天看到 Show HN 上 Cajal (YC W26) 发的 Talos:一个用 Lean 4 写的 WebAssembly 解释器,核心卖点是"评估和证明共用一套代码"——同一个定义既能跑 Wasm 程序,也能在 Lean 定理证明器里被推理。一周内 105 分、28 条讨论,讨论密度里 6 成是工程问题(动态内存、trusted base、目标语言选择),不是吐槽。
我看了一下仓库( https://github.com/cajal-technologies/talos ,123 stars / 13 forks / AGPL-3.0 / Lean 占 93.3%),觉得博客园里跑底层/系统/Wasm 的人可能感兴趣——尤其是对"AI 写代码"和"代码如何被验证"两个话题同时关注的。本文记录我从 clone 仓库到把 Factorial 例子跑通的过程,顺带把我没搞清楚的几个点写下来。
二、Talos 是什么(不是 Wasm 解释器)
先讲清楚一件事:Talos 不是一个 WASM runtime,至少主要目标不是。它是一个Wasm 形式语义 + 解释器——读起来像"在 Lean 里把 Wasm 规范重新写了一遍",而且这份"重写"本身可以被执行。
Wasm 程序 → Talos 解释器 → 执行结果(实际值)↓Lean 定理证明器 → "这个程序对所有输入满足 spec"的证明
它的设计原则 README 写得很明确(我直接引用):
The same definitions that execute a Wasm program are the ones you reason about. There is no separate spec interpreter to keep in sync: evaluation and proof share a single codebase.
"评估和证明共用一套代码"——这意味着不存在"实现 vs 规范"漂移问题。传统的形式化验证路径是"实现 + 规范 + 实现符合规范的证明",三件套,中间任何一件改动都需要重证。Talos 直接砍掉"规范"这件,只剩下 Lean 里的可执行定义。
三、实际跑一遍 Factorial 例子
我 clone 仓库后跑了他们 README 里给的 quick start:
# 1. 装 elan(Lean 4 工具链管理器)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh# 2. 进入 interpreter 目录,elam 会自动从 lean-toolchain 拉 Lean v4.31.0
cd talos/interpreter && lake build# 3. 跑 factorial.wat 例子(计算 5!)
lake exe runner samples/factorial.wat fact 5
# Output: 120# 4. 加 fuel 限制(默认 1,000,000 步,防无限循环)
lake exe runner --fuel 10000 samples/factorial.wat fact 5
第 3 步输出 120 跟我手算 5! = 120 一致,这部分确认解释器本身是工作的。
但 Talos 的核心卖点不是"能不能跑 factorial",而是"能不能证 factorial 是对的"。我看了 interpreter/Interpreter/Wasm/Examples/Factorial.lean(1,968 字节,完整文件我能背下来了):
theorem factorialSpec (m : Module) (st : Store Unit) (n : UInt32) :wp m Factorial(fun c => ∃ st' s', c = .Fallthrough st' s' ∧s'.values = [.i32 (UInt32.ofNat n.toNat.factorial)])st { params := [.i32 n], locals := [.i32 0], values := [] } := byunfold Factorialwp_runsimpapply wp_loop_cons(Inv := fun st' s' => st' = st ∧ ∃ x acc : UInt32,s' = ⟨[.i32 x], [.i32 acc], []⟩ ∧UInt32.ofNat (acc.toNat * x.toNat.factorial) = UInt32.ofNat n.toNat.factorial)(μ := fun _ s' => match s'.params.headD (.i32 0) with | .i32 x => x.toNat | _ => 0)· refine ⟨rfl, n, 1, rfl, ?_⟩simp· rintro st' s' ⟨rfl, x, acc, rfl, hacc⟩apply wp_block_conswp_run...
它证明的是:Factorial 这个 Wasm 程序(我看了 WAT 源码,就是 acc = 1; while (n != 0) { acc *= n; n -= 1; } return acc;)对任意输入 n 终止,且 acc * n! = n! 这个不变量在循环里始终成立。注意它没有显式证明"最终 n = 0"——这是因为 wp_loop_cons 战术内置了"measure 严格递减 → 终止"这一步,这里 μ = n.toNat 作为 measure。
这套东西对习惯 Rust/Go 的人来说挺陌生的,但对搞过 Coq/Isabelle 的人来说很自然。Talos 把 WP(weakest precondition) 推到了一个几乎可以替代手动写证明的高度——很多证明可以 wp_run + simp 两行就过去。
四、和同类工具比,Talos 卡在哪个位置
HN 讨论里 @lukerj00(Cajal 团队)直接列了三个备选目标:
| 目标 | 优势 | 劣势 |
|---|---|---|
| Rust 源码(e.g. Aeneas 项目) | 高层语义保留,贴近源码 | 锁死 Rust,其他语言用不上 |
| LLVM-IR | 几乎所有语言都能编译过来 | 没有官方形式语义,UB 一堆,没法证 |
| RISC-V(Sail 已有 formal model) | ISA 级别通用 | 丢掉结构化控制流和类型,证明变难 |
| Wasm(Talos 选这个) | 比 LLVM-IR 干净,有 W3C testsuite | 高层信息(struct/impl trait)丢了 |
Talos 选了 Wasm 这个折中点,理由是"W3C testsuite 当 ground truth + 结构化控制流保留 + Rust/C/Go/Swift/Kotlin/Zig/C# 都能编译过来"。这个选型我认为是合理的——LLVM-IR 太多 UB 不适合证,RISC-V 太底层证明成本高,源码级验证(Aeneas)又只服务 Rust。Wasm 是"稍微高一点点的底层"。
但 Talos 当前缺一块:动态内存分配(动态 malloc/free 产生的指针重叠问题)。@jacobjwalters 在 HN 上直接问了:
What if I want to reason about larger programs that dynamically allocate, where the addresses may not be known statically? How can I make sure these do not overlap?
@mfornet 回答:"we are actively working on this, as it is a pre-condition 😛 to reason about the simplest of useful programs. The idea is to develop an..."
也就是说:Talos 目前能证"无动态分配的程序",但还不能证"有 malloc 的程序"。这意味着它能处理"用 Rust 写一个 1000 行的纯计算库,没有 Vec/HashMap 之类的动态容器"——但不能直接处理"读一个文件 + 解析 JSON + 返回结果"这种带堆分配的真实程序。README 的 star 描述"any language with a Wasm backend is in scope" 实际只在纯计算子集成立(我下面会写)。
五、目前还没完全搞清楚的几个点(局限与待验证项)
写到这里我列一下我自己还没完全搞懂 / 还在调研的事,免得文章读起来像"它什么都能证":
- trusted base 到底有多大(待验证)。@quietusmuris 提了一个很尖锐的问题:"Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?" 也就是说——Talos 证的是 Wasm 层的正确性,但 Wasm 是从 Rust 编译过来的,Rust 编译器 +
assert!→trap的 lowering 都不在 Lean 证明范围内。这块我还没系统读过 Talos 是怎么回答的(似乎 @mfornet 在评论里提了"On the wasm side asserts are converted to trap instructions"),但待验证的是:unsafeRust / 编译器优化 / 链接器这三层是否引入了 Wasm 不会出现的 UB。 - Lean 4 学习曲线(不足)。Talos 把 WP 战术包装得比较友好(
wp_run + simp两行),但要证"自定义 spec"还是得懂 Lean。我自己跑 Factorial 例子时,第 7 行的wp_block_cons触发了一个分支讨论,需要手动by_cases hx : x = 0+omega——这要求对 Lean 的 case split 战术有基本感觉。对没用过定理证明器的人来说,门槛不低(跟学 Rust 所有权差不多量级)。 - 跟 Aeneas 的实际差距(待验证)。@kdavis 问"Why Wasm, not Rust directly?" 团队的回答是"Aeneas 锁死 Rust"。但 Aeneas 现在也在做"Rust → Lean 翻译",理论上能力会越来越强。未来 1-2 年,Wasm 层验证和源码层验证谁更主流,我还在调研——Aeneas 团队最近 6 个月的 commit 频率我没去数(待验证)。
- Wasm 性能(坑点)。README 自己写:"The interpreter is deliberately optimized for clarity of reasoning over execution speed"。
lake exe runner跑 factorial 5 大概 < 1 秒(我自己测的),但对一个真实 Wasm 模块(几 MB 的 Rust 编译产物)做完整 proof 不知道要多久——可能 30 秒,也可能 30 分钟。没有 benchmark 数字就告诉读者"production ready"是不负责任的(坑点:目前找不到公开的 proof 速度数据)。 - target 不止 Rust(待验证)。Cajal 主页(我没去查)大概率说"我们支持所有 Wasm 后端语言",但实际我看到的 example 只有一个 Rust 程序(
num-integerGCD 例子)。C/C++/Go 编出的 Wasm 程序在 Talos 里证过没?待验证——README 只说"in scope",没给"已 verified"清单。 - Wasm 特性覆盖率(还在调研)。从仓库 examples 目录(我刚
api.github.com/.../contents/.../Examples拉过)有Basic.lean/CallIndirect.lean/Factorial.lean等 3-5 个,Wasm 的 SIMD / Reference Types / Exception Handling / Multi-Memory / Component Model 这些提案目前没看到 coverage 数据。我还在调研 Lean 4 社区有没有第三方 Wasm 验证工作可以 cross-check。
六、HN 上一条让我眼前一亮的引用
第 9 条讨论里 @jsmorph 说他自己用 Talos 验过他写的 Lean 编译器(https://github.com/jsmorph/leanexe)生成的 WAT:
I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct.
也就是说——已经有第三方用 Talos 验过"Lean 编译到 Wasm"的正确性。这比 Cajal 自己写的 Factorial 例子强,说明 Talos 至少在"小规模纯计算程序"这个子集上不是空壳。如果哪天有人用它验"num-integer 的 GCD 实现",那就是 Wasm 验证从"demo"走向"实战"的标志性事件。
七、我自己的下一步
我打算先在本地把 Talos 跑通 + 把 interpreter/Interpreter/Wasm/Examples/ 下几个例子都 lake build 一遍(确认我没有 Lean 版本兼容性问题),然后尝试挑一个没有动态分配的小 Rust crate(比如 xxhash-rs 里某个纯函数)做端到端验证。
如果跑通了,我会在下一篇文章里把"如何把一个 Rust crate 编译到 Wasm → 在 Talos 里写 spec → 跑 wp_run 出证明"的全流程记录下来。
八、参考链接
- Talos GitHub:https://github.com/cajal-technologies/talos
- Talos HN 讨论:https://news.ycombinator.com/item?id=48584761
- Talos 团队 Cajal( https://cajal.technology/ ,YC W26)
- Aeneas(另一个 Rust → Lean 路径):https://github.com/AeneasVerif/aeneas
- Lean 4 工具链 elan:https://github.com/leanprover/elan
- Wasm testsuite:https://github.com/WebAssembly/spec/tree/main/test/core
- Weakest precondition 背景:https://en.wikipedia.org/wiki/Predicate_transformer_semantics
- 之前写的相关:本地模型 agentic coding(https://www.cnblogs.com/ninghg/p/20667842)、GLM-5.2 多供应商(https://www.cnblogs.com/ninghg/p/20670234)、machine0 NixOS VM(https://www.cnblogs.com/ninghg/p/20683407)