Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@tlaplus-mcp Check the file safety.tla for errors."
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
MCP server that exposes the TLA+ toolchain (TLC, SANY, PlusCal, TLATeX) as structured JSON tools over the Model Context Protocol.
Any MCP client tlaplus-mcp TLA+ toolchain
┌────────────┐ ┌──────────────────┐ ┌──────────────────┐
│ Claude Code│ │ tla_parse │ │ TLC (checker) │
│ Cursor │───MCP────▶│ tlc_check │───Java───▶│ SANY (parser) │
│ custom app │ (stdio) │ tlc_simulate │ │ PlusCal │
└────────────┘ │ tla_evaluate │ │ TLATeX │
│ pcal_translate │ └──────────────────┘
│ tlc_coverage │
│ tla_state_graph │
│ tlc_trace_spec │
│ tla_tex │
│ │
│ tla://specs │
│ tla://spec/{f} │
│ tla://output │
└──────────────────┘npx -y @richashworth/tlaplus-mcpAdd to your MCP server config (.claude/settings.json or per-project .mcp.json):
{
"mcpServers": {
"tlaplus": {
"command": "npx",
"args": ["-y", "@richashworth/tlaplus-mcp"]
}
}
}The server auto-downloads tla2tools.jar to ~/.tlaplus-mcp/lib/ on first use. Set TLC_JAR_PATH to override.
Related MCP server: vsc-mcp
Node.js 18+
Java 11+ on PATH (runs TLC and SANY)
LaTeX (optional, for tla_tex only)
Tool | Description |
| Syntax-check a TLA+ module with SANY |
| Run TLC model checker (exhaustive) |
| Run TLC in random simulation mode |
| Evaluate a constant TLA+ expression |
| Translate PlusCal to TLA+ |
| Generate a trace exploration spec from a counterexample |
| Run TLC with action coverage reporting |
| Typeset a spec as PDF via TLATeX |
| Parse a TLC DOT state graph into structured JSON |
All tools return structured JSON with a raw_output field for fallback. Errors are returned as isError responses so the LLM can adapt.
URI | Description |
| List |
| Read a specific spec file |
| Read the most recent TLC output log |
Environment variable | Description | Default |
| Path to | Auto-download to |
| JVM options |
|
| Max seconds per TLC run |
|
| Base directory for specs | Current working directory |
npm run dev # Watch mode (recompile on change)
npm test # Run all tests (unit + integration)
npm run build # Production build
npm run lint # Run ESLint
npm run format:check # Check Prettier formattingA pre-commit hook (husky + lint-staged) runs ESLint and Prettier on staged files automatically. CI also gates on both.
The project has two layers of tests:
Unit tests (src/**/*.test.ts alongside source files) — test individual parsers and tool handlers in isolation with mocked Java/filesystem calls.
Integration tests (src/integration.test.ts) — use the MCP SDK's Client + InMemoryTransport to exercise the full protocol round-trip (client → transport → server → tool handler → response) without needing Java installed. These verify tool registration, schema validation, and response shapes.
npm test # Run everything
npx vitest run src/integration.test.ts # Integration tests only
npx vitest run src/parsers/ # Parser unit tests only
npx vitest run src/tools/ # Tool handler unit tests onlyTranslate PlusCal algorithm embedded in a TLA+ file to TLA+. Modifies the .tla file in-place by inserting/updating the TLA+ translation between the * BEGIN TRANSLATION and * END TRANSLATION markers.
Inputs: tla_file (required), fairness, termination, no_cfg, +3 more.
Evaluate a constant TLA+ expression using TLC. Creates a temporary spec that prints the result of the expression.
Inputs: expression (required), imports, output_file.
Parse and syntax-check a TLA+ module using SANY (Syntactic Analyzer). Returns parse errors and the list of modules parsed.
Inputs: tla_file (required), output_file.
Load a TLC-generated DOT state graph file and return it in a structured format for exploration. Supports raw DOT, simplified adjacency list, or full JSON format with disambiguated actions, invariants, and violation traces.
Inputs: dot_file, cfg_file, tlc_output_file, tlc_output, +3 more.
Typeset a TLA+ specification into a PDF or DVI file using TLATeX. Requires a LaTeX installation (pdflatex or latex) to be available.
Inputs: tla_file (required), shade, number, no_pcal_shade, +2 more.
Run TLC model checker in exhaustive breadth-first mode to verify a TLA+ specification. Checks all reachable states against invariants, properties, and (optionally) deadlock freedom.
Inputs: tla_file (required), output_file (required), cfg_file, workers, +8 more.
Run TLC model checker with action coverage reporting. Shows how many times each action was taken and how many distinct states it produced, helping identify under-explored parts of the spec.
Inputs: tla_file (required), cfg_file, interval_minutes, workers, +1 more.
Run TLC model-checking on a TLA+ spec with -generateSpecTE to produce a Trace Explorer spec (SpecTE.tla / SpecTE.cfg). This is useful for debugging counter-examples: it generates a standalone spec that replays the error trace.
Inputs: tla_file (required), cfg_file, monolith, extra_args.
Run TLC in simulation mode to randomly explore execution traces. Faster than exhaustive checking but not complete — useful for large state spaces or quick smoke tests.
Inputs: tla_file (required), cfg_file, depth, num_traces, +6 more.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
Loading tool schema changelog…
Scored across 9 tools
Each tool has a distinct purpose covering different aspects of TLA+ workflow: parsing, model checking, simulation, coverage, trace generation, state graph analysis, evaluation, translation from PlusCal, and typesetting. No two tools overlap in functionality.
Names follow a consistent pattern with prefixes (tla_, tlc_, pcal_) indicating the tool, followed by a descriptive verb or noun. The only minor inconsistency is 'tla_state_graph' which deals with TLC-generated files, but overall the pattern is clear and predictable.
9 tools is appropriate for a TLA+ toolset, covering essential operations without being too many or too few. Each tool earns its place in the workflow.
The tool set covers the core TLA+ lifecycle: parsing, evaluation, model checking, simulation, coverage, trace generation, state graph analysis, PlusCal translation, and typesetting. Minor gaps exist (e.g., no explicit LTL property checking tool, but tlc_check handles properties; no distributed mode) but the surface is largely complete.
A comprehensive Model Context Protocol (MCP) server that enables AI assistants to interact with yo…
A Model Context Protocol server for Wix AI tools
Convert, lint and generate LLM tool schemas for OpenAI, Anthropic, Gemini and MCP
SysML v2 systems engineering: generate, verify, simulate and export system models from text.