Show HN: Talos – Open-source WASM interpreter for Lean

The 5-second version

• Talos is a WebAssembly interpreter written in Lean 4 where the same executable semantics are used for both running programs and formal verification, eliminating the need to keep a separate spec in sync.
• It uses weakest precondition calculus for compositional reasoning about program behavior, enabling proofs of correctness, equivalence, and properties without re-unfolding the interpreter at each step.
• The project is structured as three Lake packages in dependency order: interpreter (core Wasm semantics and WP tactics), codelib (lifting lemmas and reasoning helpers), and programs (concrete verification tasks).
• You can run .wat modules directly with a fuel-capped interpreter or prove theorems about them using Lean's proof tooling, with the immediate focus on non-optimized higher-level source semantics over performance.
• The codebase is AGPL v3.0 licensed, actively developed with potentially changing APIs, and requires Lean 4 (via elan) and wasm-tools for building and running the Wasm testsuite.

Top voices

Verbatim comments from the thread's most notable / highest-karma participants.