tlaplus-mcp

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    │
                         └──────────────────┘

Installation

npx -y @richashworth/tlaplus-mcp

Configure in Claude Code

Add 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.

Prerequisites

• Node.js 18+
• Java 11+ on PATH (runs TLC and SANY)
• LaTeX (optional, for tla_tex only)

Tools

Tool	Description
tla_parse	Syntax-check a TLA+ module with SANY
tlc_check	Run TLC model checker (exhaustive)
tlc_simulate	Run TLC in random simulation mode
tla_evaluate	Evaluate a constant TLA+ expression
pcal_translate	Translate PlusCal to TLA+
tlc_generate_trace_spec	Generate a trace exploration spec from a counterexample
tlc_coverage	Run TLC with action coverage reporting
tla_tex	Typeset a spec as PDF via TLATeX
tla_state_graph	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.

Resources

URI	Description
tla://specs	List .tla and .cfg files in the workspace
tla://spec/{filename}	Read a specific spec file
tla://output/latest	Read the most recent TLC output log

Configuration

Environment variable	Description	Default
TLC_JAR_PATH	Path to tla2tools.jar	Auto-download to ~/.tlaplus-mcp/lib/
TLC_JAVA_OPTS	JVM options	-Xmx4g -XX:+UseParallelGC
TLC_TIMEOUT	Max seconds per TLC run	300
TLC_WORKSPACE	Base directory for specs	Current working directory

Development

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 formatting

A pre-commit hook (husky + lint-staged) runs ESLint and Prettier on staged files automatically. CI also gates on both.

Testing

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 only