tla-mcp

A TLA+ model checker as a Model Context Protocol server.

Plug a working model checker into Claude Code, Cursor, or any MCP-aware client. Validate specs, replay counterexamples, and catch invariant violations without leaving the conversation.

What is this?

TLA+ is a specification language for designing and verifying concurrent and distributed systems. You describe what your protocol should do; a model checker tries every reachable state and tells you when something goes wrong.

The Model Context Protocol (MCP) is how agentic clients like Claude Code call external tools.

tla-mcp bridges the two. It's a stdio MCP server built on top of tla-rs, a fast TLA+ model checker written in Rust. Once registered, your client can parse a spec, list its invariants, run a full check with a budgeted time limit, and replay specific scenarios — all from inside the chat.

Install

Pick whichever fits your toolchain. All paths install the same v0.4.3 binary.

Homebrew (macOS, Linuxbrew)

brew install fabracht/tla/tla-mcp

Installs both tla (model checker CLI) and tla-mcp (MCP server).

Install script (Linux, macOS)

curl -fsSL https://raw.githubusercontent.com/fabracht/tla-rs/main/scripts/install.sh | bash

SHA256-verified binary download. Pass --bin tla-mcp to install just the server.

Cargo (any platform with a Rust toolchain)

cargo install tla-checker --bin tla-mcp

Pre-built release binaries

Linux x86_64, macOS x86_64, macOS arm64, Windows x86_64 are attached to every GitHub release as tla-<platform> and tla-mcp-<platform>, alongside a SHA256SUMS file.

Register with your client

Add to your MCP client config (Claude Code example, ~/.claude/mcp.json):

{
  "mcpServers": {
    "tla": {
      "command": "tla-mcp"
    }
  }
}

Restart the client. The four tools become available immediately.

What the agent gets

Four tools, versioned JSON schemas (schema_version: "1"):

`tool`	purpose
`validate_spec`	Parse a `.tla` file. Returns vars, constants with resolved values, detected invariants, `has_init` / `has_next`, plus structured parse errors with source spans.
`list_invariants`	Return invariant names matching `Inv`, `TypeOK`, `NotSolved*`, plus anything declared via cfg `INVARIANT` directive.
`check_spec`	Full model checking with required `max_states` / `max_depth` / `max_seconds` budgets. Returns `ok`, `invariant_violation` (with trace + actions), `deadlock`, `liveness_violation` (prefix + cycle), `limit_reached`, or structured `error`.
`replay_scenario`	Step through a spec along a guided path (`step: <TLA+ expr>` lines). Returns per-step state snapshots + variable changes, or a failure with `available_actions` on a mismatch.

Why TLA+ for an agent?

Most "is this code correct?" questions an agent answers are really questions about reachable behavior — a race condition that fires in one specific interleaving, a queue that grows unboundedly under a corner-case workload, a consensus rule that lets two leaders coexist for one tick. Reasoning about all these by reading code is hard. Asking a model checker is straightforward, when the model checker is one tool call away.

tla-mcp is opinionated about how an agent should use it. Tool descriptions explicitly tell the agent: budget all three limits upfront; inspect constants before running; treat limit_reached as inconclusive, not as a pass; bugs are usually in the last transition of the trace. These are not soft hints — they're encoded in the tool metadata so they survive context truncation.