Skip to main content
Glama
richashworth

tlaplus-mcp

by richashworth
OverviewSchemaRelated ServersScoreDiscussions
TypeScript
Local

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.

Related MCP server: Agent Construct

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
Install Server
A
license - permissive license
A
quality
D
maintenance

How are these scores calculated?

Maintenance

–Maintainers
1hResponse time
–Release cycle
–Releases (12mo)
Commit activity

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Tools

View all tools

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/richashworth/tlaplus-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server