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), strings ("hello"), and sets ({1,2,3}).

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-depth N | Maximum trace depth (default: 100) | | -q | Quick exploration (limit: 10,000 states) | | --export-dot FILE | Export state graph to DOT format | | --dot-mode MODE | DOT mode: full, trace, clean (default), choices | | --allow-deadlock | Allow states with no successors | | --check-liveness | Check liveness and fairness properties | | --continue | Continue past invariant violations | | --count-satisfying NAME | Count states satisfying a definition (repeatable) | | --sweep NAME=V1;V2;... | Sweep a constant across values, compare results | | --scenario TEXT | Explore a specific scenario (or @file) | | -i | Interactive TUI exploration mode | | --present FILE | Run a demo manifest (.json/.toml); TUI walkthrough, or --validate for a pass/fail report | | --export-md FILE | With --present: write a Markdown walkthrough | | --export-html FILE | With --present: write a self-contained HTML walkthrough | | --explorable | With --export-html: embed the wasm engine for in-browser state exploration | | --json | JSON output | | -v | Verbose output (depth breakdowns, etc.) |

Documentation

| Guide | Contents | |-------|----------| | CLI Guide | Configuration files, scenarios, demo walkthroughs (incl. the --explorable browser explorer), interactive mode, analytics, output, and state-graph visualization | | TLA+ Support | Supported operator subset, module instances, spec structure, and limitations | | WebAssembly | Browser-embeddable WASM API, including the live stepping bindings | | MCP Server | tla-mcp install, client registration, and tool reference | | Syntax Status | Operator-by-operator coverage table | | Architecture | Internal design | | Practical TLA+ Guide | Worked guidance for writing checkable specs |

License

MIT