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.

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"), sets ({1,2,3}), tuples (<<1,2>>), records ([hp |-> 100]), and functions (a :> 1 @@ b :> 2).

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