Tla Rs

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](MCP.md#install).

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

Option	Description
-c NAME=VALUE	Set a constant value
-s CONST	Enable symmetry reduction for a constant
--config PATH	Load TLC-style cfg file (auto-discovers Spec.cfg next to Spec.tla)
--max-states N	Maximum states to explore (default: 1000000)
`--max-dep