cajal-technologies/talos

Talos is a WebAssembly interpreter written in Lean 4, a programming language that doubles as a proof assistant. WebAssembly (often shortened to Wasm) is a binary format that compilers for languages like Rust and C can produce, and which can then run in browsers or other environments. An interpreter is the software that actually executes that binary. What makes Talos different from a conventional Wasm interpreter is its purpose. Most interpreters are built to run code quickly. Talos is built to let you reason about code formally: you can run a program on concrete inputs, but you can also state and mathematically prove claims about what the program will do for all possible inputs, or prove that two programs behave identically, or prove that a specific function always returns the correct result. The same code that executes a program is the code you write proofs against, so there is no risk of the proof applying to a different version of the semantics than the one actually running. Proofs in Talos use a technique called weakest precondition calculus. In practical terms, this means you describe what you want to be true after a function runs (the postcondition), and the proof system works backwards to figure out what must be true going in (the precondition). This approach handles loops, branches, and function calls in a structured way without having to unfold the entire interpreter definition every time. The repository is split into three packages. The core interpreter contains the WebAssembly semantics and the proof tooling layer. A second package adds helper lemmas and utilities for reasoning about programs. A third package holds worked verification examples for Rust-compiled Wasm programs. To use it you need Lean 4 (managed automatically by its version manager) and a tool called wasm-tools for handling binary Wasm files. The project is marked as a work in progress, meaning the API and proof interfaces may still change. It is released under the MIT license.