Talos：Lean定理证明专用WASM解释器

Talos 是一个用 Lean 4 编写的 WebAssembly 解释器，得名于希腊神话中的青铜巨人——他曾守卫克里特岛，是一个机械守护者，被造来执行规则。

执行 Wasm 程序的定义和你用来推理的定义是同一套。没有单独的规范解释器需要保持同步：计算和证明共享一个代码库。

开发中。Talos 正在积极开发中。API 和证明接口可能会改变。

目标是实现功能完整的、可执行的 WebAssembly 语义，同时作为一个形式化对象。你可以：

• 在具体输入上运行程序。

• 用 Lean 的证明工具陈述并证明关于程序行为的定理——针对规范的正确性、程序间的等价性、对所有输入都成立的性质。

解释器刻意优化了推理的清晰性而非执行速度。Talos 致力于完整覆盖 Wasm，但当前重点是自然产生于非优化、高级源代码（Rust、C 等）的特性子集——当你想验证程序做什么而不是做得有多快时，这才是真正重要的语义。

证明是北极星。 性能工作应该在单独的、被证明等价的实现之后。

Talos 中的证明建立在最弱前条件（WP）演算之上——一种谓词变换语义，让你从后条件反向推理到保证它们的前条件。这为循环、分支和函数调用提供了结构化、可组合的证明，而无需在每一步都重新展开解释器。

运行示例

cd interpreter
lake exe runner samples/factorial.wat fact 5

使用燃料上限运行（默认 1,000,000 步）：

lake exe runner --fuel 10000 samples/factorial.wat fact 5

见 interpreter/samples/factorial.wat 获取一个最小示例模块。

证明示例

interpreter/Interpreter/Wasm/Examples/Factorial.lean 展示了通过组合指令粒度小步跟踪的完整正确性证明。

项目结构

单一仓库中的三个 Lake 包，形成严格的依赖链。

作为依赖使用

仅依赖解释器（Wasm 语义 + WP 演算）：

# lakefile.toml
[[require]]
name = "WasmInterpreterLean"
scope = "your-org"           # if published, or use path/git
path = "path/to/repo/interpreter"

依赖 CodeLib（在其之上添加提升引理和推理助手）：

[[require]]
name = "CodeLib"
path = "path/to/repo/codelib"

导入 CodeLib 的代码永远不需要直接导入解释器——CodeLib 重新导出下游证明所需的解释器部分。

构建

just build   # builds interpreter → codelib → programs in order

或构建单个包：

cd interpreter  && lake build
cd codelib      && lake build
cd programs/lean && lake build

依赖

Lean 4 ——工具链固定在 interpreter/lean-toolchain 中，由 elan 自动获取。

wasm-tools ——解码 .wasm 二进制文件和运行 Wasm 测试套件需要。brew install wasm-tools 或 cargo install wasm-tools。

运行 Wasm 测试套件

just testsuite

按名称过滤到特定文件：

just testsuite i32

许可证

GNU Affero General Public License v3.0 ——见 LICENSE。