Talos 是用 Lean 4 编写的 WebAssembly 解释器，得名于希腊神话中守卫克里特岛的青铜巨人 - 一个机械守护者，旨在执行规则。执行 Wasm 程序的相同定义也是你所推理的内容。没有单独的规范解释器需要保持同步：评估和证明共享一个代码库。正在进行中的工作。Talos 正在积极开发中。API 和证明接口可能会发生变化。这个目标是一个功能完整、可执行的 WebAssembly 语义，双重作为一个形式对象。你可以：在具体输入上运行程序。声明并证明有关其行为的定理 - 针对规范的正确性、程序之间的等价、对所有输入都成立的属性 - 使用 Lean 的证明工具。这个解释器特别优化了推理的清晰性，而不是执行速度。Talos 旨在实现全覆盖 Wasm，但当前重点是自然来源于非优化的高层源代码（如 Rust、C 等）的特性子集 - 当你想验证程序的功能时，确实重要的语义，而不是它的执行速度。证明是北极星。性能相关的工作应在单独经过证明等效实现的后面。推理基础 Talos 中的证明建立在最弱前置条件 (WP) 演算之上 - 一种谓词变换语义，允许你从后置条件向后推理到保证它们的前置条件。这为循环、分支和函数调用提供了结构化的、组合性的证明，而无需在每一步重新展开解释器。快速开始 运行 .wat 模块：cd interpreter lake exe runner samples/factorial.wat fact 5 输出：120 限制燃料上限（默认 1 000 000 步骤）：lake exe runner --fuel 10000 samples/factorial.wat 参见 interpreter/samples/factorial.wat 以获取一个最小示例模块。证明有关它的内容：interpreter/Interpreter/Wasm/Examples/Factorial.lean 显示了使用 WP 战术层的完整正确性证明。仓库布局 三个 Lake 包位于单一仓库中，形成严格的依赖链：包路径 目的 解释器 interpreter/ Wasm AST、语义、WP 战术层 CodeLib codelib/ 提升引理和程序推理辅助程序 程序 programs/ 具体 Rust-to-Wasm 验证任务 作为依赖使用 仅依赖解释器（Wasm 语义 + WP 演算）：# lakefile.toml [[require]] name = "WasmInterpreterLean" scope = "your-org" # 如果已发布，或使用路径/git path = "path/to/repo/interpreter" 依赖 CodeLib（在其上添加提升引理和推理辅助程序）：[[require]] name = "CodeLib" path = "path/to/repo/codelib" 引入 CodeLib 的代码无需直接导入解释器 - CodeLib 重新导出下游证明所需的解释器部分。构建 仅构建 # 按顺序构建解释器 → codelib → 程序 或单独构建一个包：cd interpreter && lake build cd codelib && lake build cd programs && lake build 依赖项：Lean 4 - 工具链在 interpreter/lean-toolchain 中固定，由 elan 自动获取。 wasm-tools - 需要解码 .wasm 二进制文件并运行 Wasm 测试集。brew install wasm-tools 或 cargo install wasm-tools 。 运行 Wasm 测试集只需 testsuite 按名称过滤特定文件： just testsuite i32 贡献 请参见 CONTRIBUTING.md 。 许可证 GNU Affero 通用公共许可证 v3.0 - 请参见 LICENSE 。