tlaplus-mcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| TLC_TIMEOUT | No | Max seconds per TLC run. Default: 300 | 300 |
| TLC_JAR_PATH | No | Path to tla2tools.jar. Auto-downloads to ~/.tlaplus-mcp/lib/ if not set. | |
| TLC_JAVA_OPTS | No | JVM options for TLC. Default: -Xmx4g -XX:+UseParallelGC | -Xmx4g -XX:+UseParallelGC |
| TLC_WORKSPACE | No | Base directory for specs. Default: current working directory |
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": true
} |
| resources | {
"listChanged": true
} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| tlc_checkB | 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. |
| tlc_simulateA | 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. |
| tla_parseA | Parse and syntax-check a TLA+ module using SANY (Syntactic Analyzer). Returns parse errors and the list of modules parsed. |
| tla_evaluateA | Evaluate a constant TLA+ expression using TLC. Creates a temporary spec that prints the result of the expression. |
| pcal_translateA | Translate 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. |
| tlc_generate_trace_specA | 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. |
| tlc_coverageA | 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. |
| tla_texA | Typeset a TLA+ specification into a PDF or DVI file using TLATeX. Requires a LaTeX installation (pdflatex or latex) to be available. |
| tla_state_graphB | 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. |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
| specs | List all .tla and .cfg files in the TLA+ workspace directory |
| latest-output | Read the most recent TLC output file from the workspace |
TDQS
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.