Talos – Open-source WASM interpreter for Lean
Summary
Talos is a WebAssembly interpreter written in Lean 4 that provides executable semantics suitable for proving properties about Wasm programs. The project emphasizes verification, using weakest precondition calculus, and positions itself as a runnable semantics plus formal reasoning tool, with a three-package monorepo and an AGPL license.