tla-rs

A TLA+ model checker and interactive exploration tool written in Rust.

tla-rs verifies TLA+ specifications by exploring all reachable states, checking invariants, and reporting counterexamples. Beyond pass/fail checking it offers an interactive TUI for stepping through state spaces, scenario-driven exploration, property-satisfaction analytics, parameter sweeps, tested demo walkthroughs (with an optional in-browser explorer), and an MCP server for agentic clients. The core library compiles to WebAssembly for browser embedding. It's a lightweight alternative to the official TLC model checker for specs that fit its supported subset.

Installation

cargo build --release

The binary will be at target/release/tla. Prebuilt binaries and the tla-mcp server are available via Homebrew, an install script, or GitHub releases — see the MCP Server guide.

Quick Start

tla spec.tla
tla spec.tla -c 'N=5' -c 'Procs={"p1","p2","p3"}'
tla spec.tla -c 'Proc={a,b,c}' --symmetry Proc
tla spec.tla --config model.cfg
tla spec.tla --quick    # limit to 10,000 states
tla spec.tla -i         # interactive TUI

Constants accept integers (42), booleans (TRUE), quoted strings ("hello"), sets ({1,2,3}), tuples (<<1,2>>), records ([hp |-> 100]), and functions (a :> 1 @@ b :> 2).

A bare identifier is a model value — an uninterpreted, pairwise-distinct atom, matching TLC. n1 is not equal to the string "n1", so -c 'Proc={a,b,c}' yields three model values, not three strings. Symmetry reduction requires a set of model values (--symmetry rejects a set of quoted strings, as TLC does).

Options

Documentation

License

MIT