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 .…