Talos provides a feature-complete, executable semantics for WebAssembly that doubles as a formal object for theorem proving. It uses weakest precondition (WP) calculus to allow developers to state and prove properties about Wasm program behavior directly within Lean's proof tooling, sharing a single codebase for both execution and reasoning.