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