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

Category: library

Tags: webassembly, formal-verification, lean

Score: 6.3/10 (Innovation: 7, Technical: 6, Documentation: 7, Utility: 5)

Talos is a WebAssembly interpreter written in Lean 4 that doubles as a formal verification tool, allowing users to both run Wasm programs and prove theorems about their behavior using a weakest precondition calculus. Its unique integration of execution and proof in a single codebase makes it interesting for research and verification of Wasm programs in safety-critical contexts.

Target audience: researchers, verification engineers, systems programmers

Repository: https://github.com/cajal-technologies/talos · Lean · AGPL-3.0 · 23 stars

View on Hacker News