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

Category: infrastructure

Tags: wasm, lean4, formal-verification, webassembly-interpreter, proof-assistant

Score: 7.5/10 (Innovation: 8, Technical: 9, Documentation: 7, Utility: 6)

Talos is a WebAssembly interpreter written in Lean 4 that doubles as a formal verification tool, allowing users to both execute Wasm programs and prove theorems about their behavior using a weakest-precondition calculus. Its unifying of execution and proof in a single codebase is a novel combination that enables verification without a separate spec interpreter. This project is particularly interesting for its potential to bring formal verification to practical Wasm workloads.

Target audience: backend devs, devops, data engineers

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

View on Hacker News