Talos, an early stage open source project, writes a WebAssembly interpreter (the portable bytecode that runs in browsers and edge runtimes) as Lean 4 (an interactive theorem prover and functional programming language) code, collapsing the gap between running a program and…
A small team has staked a concrete bet on a stubborn problem in formal verification: the code that runs a program and the code that proves what it does should live in the same file.
Talos, an early-stage open-source project from Cajal Technologies, is an interpreter for WebAssembly, the portable bytecode that runs in browsers, servers, and edge runtimes. The interpreter itself is written in Lean 4, an interactive theorem prover and functional programming language. The pitch is unifying. The same Lean definitions that execute a WebAssembly module are the ones a developer proves theorems about, so the implementation cannot drift from the specification.
That is the design idea the project calls its north star, and it is the reason a 27-star GitHub repository with 112 commits is worth talking about. Formal verification has always carried a two-codebase problem. Tools such as Coq, F*, and Rust's Kani reason about a separate model of the language while the actual runtime lives in a different codebase written for speed, not proof. The two implementations drift. Bugs and proofs move out of sync. Talos collapses those two roles into a single Lean file. The project's repository frames this as "Wasm interpreter in lean, designed for reasoning," with a verifier/ directory sitting alongside interpreter/, programs/, and the test harness at the repo root.
The reason the design matters in practice is that spec/verifier drift is the failure mode that has stalled verified systems work for years. A team can spend months proving theorems about a language model that no longer matches the production interpreter. The cost of keeping those two codebases in sync is the reason most verified-software projects stay narrow. An interpreter written in a theorem prover, where the executable semantics and the proof obligations refer to the same definitions, removes that ongoing tax.
What Talos actually delivers today is more modest than the pitch. The repository describes itself as a "work in progress" and warns that "APIs and proof interfaces may change." The interpreter and the verifier scaffolding both exist, but the README is the only public source for the project's goals in the material provided. There is no third-party benchmark against Wasmtime, V8, or Wasmer, and no peer-reviewed proof of full WebAssembly spec coverage. The 27-star and 7-fork count is a fair signal of how small the user base is.
Performance is a separate, explicit choice. The project deprioritizes speed in favor of a design where a separately proven-equivalent implementation would later replace the slow version. That implementation does not exist yet. The trade is a slow interpreter you can reason about directly, with the hope of a fast one that is provably equivalent later. The trade is reasonable. It is also the project's own framing rather than a delivered result.
The toolchain details point in two directions at once. A pinned Lean toolchain, a justfile, a testsuite_report.txt, and a structured layout with interpreter/, verifier/, programs/, docbuild/, codelib/, scripts/, and vendor/ directories suggest a working build and a contributor workflow. AGENTS.md, CLAUDE.md, CONTRIBUTING.md, and a LICENSE file are present. The presence of .claude/ and .codex/ configuration directories, with a pinned toolchain, hints at agent-assisted development, though the repository does not state this directly in the material provided.
For a reader who cares about verified systems, the live question is whether a single-Lean-codebase interpreter can be both expressive enough to support real WebAssembly modules and tractable enough to prove things about. The Lean-based Wasm work also competes with adjacent ecosystems in Coq, F*, and Rust+kani, none of which has settled the question either. Talos is a small, organized attempt to put a real artifact on the table so the community has something concrete to argue with.
What to watch next: a populated verifier/ directory with formal proofs of interpreter correctness, a real benchmark against an established Wasm runtime, and an external maintainer or research group willing to put their name on the proof obligations. Without at least one of those, Talos remains a credible early artifact, not a result. With any of them, it becomes a data point the verified-computing community has not had in this form before.