Talos: An Open-Source Wasm Interpreter for Formal Reasoning in Lean 4

Talos is an open-source WebAssembly (Wasm) interpreter written in Lean 4, designed specifically to bridge the gap between program execution and formal verification. By using the same codebase for both executing Wasm programs and reasoning about them, Talos eliminates the need to maintain a separate specification interpreter, ensuring that evaluation and proof remain perfectly in sync.

Unified Execution and Verification

Talos provides a feature-complete, executable semantics for WebAssembly that functions as a formal object. This architecture allows developers to perform two primary actions within a single environment:

  1. Concrete Execution: Run Wasm programs on specific inputs to observe behavior.
  2. Formal Proof: State and prove theorems regarding program behavior, such as correctness against a specification, equivalence between different programs, or properties that hold across all possible inputs.

To facilitate these goals, the interpreter is optimized for clarity of reasoning rather than raw execution speed. The project maintainers state that performance optimizations should be implemented in separate versions that are then proven equivalent to the core reasoning-focused implementation.

Reasoning Foundation: Weakest Precondition Calculus

Formal proofs in Talos are implemented using weakest precondition (WP) calculus, a form of predicate transformer semantics. This approach allows developers to reason backward from a desired postcondition to the preconditions required to guarantee that condition.

This methodology provides structured and compositional proofs for complex program structures, including:

  • Loops
  • Branches
  • Conditional logic
  • Function calls

By using WP calculus, Talos avoids the need to re-unfold the interpreter at every step of a proof, making the verification process more manageable.

Project Architecture and Tooling

Talos is organized as a monorepo containing three Lake packages with a strict dependency chain:

Package Path Purpose
Interpreter interpreter/ Contains the Wasm AST, core semantics, and the WP tactic layer.
CodeLib codelib/ Provides lifting lemmas and helpers for program reasoning.
Programs programs/ Contains concrete verification tasks for Rust-to-Wasm translations.

Quick Start and Dependencies

Users can run .wat modules using the runner executable. For example, executing a factorial function with an input of 5 results in 120. The system also supports a "fuel cap" (defaulting to 1,000,000 steps) to prevent infinite execution.

Key Dependencies:

  • Lean 4: The primary language and proof assistant.
  • wasm-tools: Required for decoding .wasm binaries and running the Wasm test suite.

Community Insights and Technical Considerations

Technical discussions surrounding the release highlight several critical considerations for formal Wasm verification:

Verification Targets

A member of the Cajal team noted that the core strategy is based on the premise that "Wasm is a good verification target" because it is close to compiled artifacts and is targeted by many high-level languages.

Challenges in Formalization

Community members have raised questions regarding several complex aspects of the Wasm specification that impact formal proofs:

  • Memory Management: Questions have been raised about how Talos handles dynamic allocation and overlapping addresses in larger programs.
  • Nondeterminism: The Wasm spec includes sources of nondeterminism, such as NaN representation, host calls, and stack exhaustion. Experts in other Wasm formalizations (like WasmCert-Isabelle) have questioned how Talos models these to ensure that a program proven correct in Talos behaves identically in a conforming production interpreter.
  • Non-terminating Programs: As a shallow embedding in Lean, the approach for verifying properties of programs that may not terminate is a point of technical interest.

"If the goal is to prove programs correct, one risk is that I prove my program correct against your Wasm interpreter (which maybe makes certain choices that aren't determined by the spec), and then I run it against another fully-conforming interpreter in the wild and it behaves incorrectly."

Comparison to Other Frameworks

The project is part of a broader ecosystem of Wasm verification tools, including WasmCert-Isabelle, WasmRef-Isabelle, and WasmCert-Coq. The primary distinction for Talos is its implementation in Lean 4, leveraging Lean's specific proof tooling and tactic layers.

Sources