GoKawiilTalos
Talos is a WebAssembly interpreter written in Lean 4, named after the bronze giant of Greek mythology who guarded Crete — a mechanical guardian, built to enforce rules.
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.
Work in progress. Talos is under active development. APIs and proof interfaces may change.
What this is
The goal is a feature-complete, executable semantics for WebAssembly that doubles as a formal object. You can:
Run programs on concrete inputs.
State and prove theorems about their behavior — correctness against a spec, equivalence between programs, properties that hold for all inputs — using Lean's proof tooling.
The interpreter is deliberately optimized for clarity of reasoning over execution speed. Talos aims for full Wasm coverage, but the immediate focus is on the subset of features that arise naturally from non-optimized, higher-level source code (Rust, C, etc.) — the semantics that actually matter when you want to verify what a program does, not how fast it does it.
Proof is the north star. Performance work belongs behind a separately proven-equivalent implementation.
... continue reading