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: Agent Construct
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.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla file containing PlusCal code | |
| fairness | No | Fairness condition: wf (weak), sf (strong), wfNext (weak on Next), nof (none) | nof |
| termination | No | Add termination detection to the spec | |
| no_cfg | No | Do not generate a .cfg file | |
| label | No | Add missing labels automatically | |
| line_width | No | Line width for the translation output | |
| output_file | No | Optional. If provided, raw pcal.trans output is written to this file and the response contains output_file instead of raw_output. (Note: this is the raw TRANSLATOR output — the translated TLA+ spec is always written in-place to tla_file, reported as translated_file.) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided, so the description carries full burden. It discloses that the file is modified in-place and that translation is placed between specific markers. However, it does not cover prerequisites, error conditions, or what happens if markers are missing, leaving some gaps.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is two sentences: the first defines the main action, the second adds key details about in-place modification. No redundant or extraneous information.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the complexity (7 parameters, no output schema), the description covers the essential purpose and main behavior. It could be improved by mentioning prerequisites or error handling, but it is largely complete for typical use.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
All 7 parameters have descriptions in the schema (100% coverage). The description adds no extra parameter information beyond the schema, so baseline score of 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description explicitly states the verb 'Translate' and the resource 'PlusCal algorithm embedded in a TLA+ file'. It distinguishes this tool from siblings like tla_evaluate or tla_parse by specifying it handles PlusCal translation and modifies the file in-place.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Indicates that the tool modifies the .tla file in-place, which implies when it should be used (translation step). It does not explicitly state when not to use or provide alternatives, but the context and sibling names suggest clear use cases.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Evaluate a constant TLA+ expression using TLC. Creates a temporary spec that prints the result of the expression.
| Name | Required | Description | Default |
|---|---|---|---|
| expression | Yes | TLA+ expression to evaluate (e.g., '1 + 2', '{1,2,3} \\union {4,5}') | |
| imports | No | Modules to EXTEND (e.g., ['Integers', 'Sequences']). Defaults to ['Integers', 'Sequences', 'FiniteSets', 'TLC'] | |
| output_file | No | Optional. If provided, raw TLC output is written to this file and the response contains output_file instead of raw_output. |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It discloses that a temporary spec is created and the result is printed, but lacks details on error handling, side effects, or response format.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Two sentences, no wasted words, highly concise and immediately readable.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description covers the core mechanism and purpose, but lacks details on the return format and how output_file works, given no output schema and no annotations.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100% with detailed parameter descriptions. The description adds minimal additional meaning beyond the schema, so a baseline score of 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb 'evaluate' and the resource 'constant TLA+ expression', and distinguishes from sibling tools like tlc_check by focusing on a single expression evaluation rather than model checking.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies use for constant expressions (no temporal logic, no state search) but does not explicitly state when to use or avoid it compared to siblings.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Parse and syntax-check a TLA+ module using SANY (Syntactic Analyzer). Returns parse errors and the list of modules parsed.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla file to parse | |
| output_file | No | Optional. If provided, raw SANY output is written to this file and the response contains output_file instead of raw_output. |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description must convey behavioral traits. It explains the tool uses SANY, returns errors and module list, and optionally writes raw output to a file. This is adequate but does not detail error format or side effects (none expected for a parse tool).
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is two sentences, no fluff, with all information front-loaded. Every sentence earns its place: first states action and tool, second specifies return value.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a parse tool with no output schema, the description sufficiently explains what the tool does and returns. However, it could be more complete by mentioning error format or that the tool may be used before other TLA+ operations.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so baseline is 3. The description adds value by explaining that output_file causes raw SANY output to be written and the response to include output_file instead of raw_output, beyond what the schema alone provides.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's action ('Parse and syntax-check a TLA+ module using SANY') and its output ('Returns parse errors and the list of modules parsed'). This distinguishes it from sibling tools like tlc_check (model checking) or pcal_translate (translation).
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage for syntax checking, but does not explicitly contrast with siblings or state when not to use. However, the context of sibling tool names (e.g., tlc_check, tla_evaluate) makes the purpose clear enough for an agent to select appropriately.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| dot_file | No | Absolute path to the .dot state graph file generated by TLC (not needed in traces_only mode) | |
| cfg_file | No | Absolute path to the .cfg file (for invariant/property names) | |
| tlc_output_file | No | Absolute path to the TLC output file (for violation traces) | |
| tlc_output | No | Raw TLC output string (for violation traces). If both tlc_output and tlc_output_file are provided, tlc_output takes precedence. | |
| format | No | Output format: 'dot' (raw), 'structured' (adjacency list), or 'json' (full structured output with states, transitions, violations, happy paths) | json |
| traces_only | No | When true, build a minimal graph from TLC output traces alone (no DOT file needed). Returns partial: true. | |
| output_file | No | Write JSON to this file (REQUIRED for json format) instead of returning it inline. Response will contain a compact summary. Must be omitted for dot/structured formats. |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description must fully convey behavioral traits. It states it loads a DOT file and returns structured data, but omits details like error handling, file size limits, or performance implications. Minimal behavioral context beyond the basic operation.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Two concise sentences covering action and format options. No wasted words; front-loaded with the core purpose.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With 7 parameters, no output schema, and no annotations, the description is sparse. It does not explain the structure of returned data (e.g., what 'structured format' entails) or how modes like 'traces_only' and 'output_file' affect the response. Incomplete for a tool with this complexity.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so baseline is 3. The description adds no extra semantics beyond the schema's parameter descriptions; it lists formats but does not elaborate on parameter interactions or constraints.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('load a TLC-generated DOT state graph file and return it in a structured format') and distinguishes the tool from siblings like tlc_check or tlc_simulate by focusing on state graph exploration. It specifies supported formats (dot, structured, json) and mentions disambiguated actions, invariants, and violation traces.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No explicit guidance on when to use this tool versus alternatives (e.g., tlc_coverage or tlc_simulate). The description implies usage for state graph exploration, but does not provide when-not-to-use or contrast with sibling tools.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Typeset a TLA+ specification into a PDF or DVI file using TLATeX. Requires a LaTeX installation (pdflatex or latex) to be available.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla file to typeset | |
| shade | No | Add shading to comments | |
| number | No | Add line numbers | |
| no_pcal_shade | No | Do not shade PlusCal code | |
| gray_level | No | Gray level for shading (0 = black, 1 = white) | |
| output_format | No | Output format |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It discloses the external dependency on LaTeX, but does not explain behavior on failure (e.g., missing LaTeX, invalid file) or whether files are modified. It adds some value beyond purpose but lacks depth.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is concise at two sentences, no wasted words, and front-loads the core purpose. It is efficient and easy to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description is largely complete given the high schema coverage and straightforward tool purpose. However, it lacks information about output behavior (e.g., file location, success indication) since no output schema is provided. Minor gap for a fully complete definition.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The input schema has 100% description coverage, so the schema already documents all parameters. The description does not add any additional meaning or context beyond what is in the schema, maintaining the baseline score.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Typeset a TLA+ specification into a PDF or DVI file using TLATeX.' The verb 'Typeset' and the specific output formats distinguish it clearly from siblings like tlc_check or pcal_translate.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description explicitly states when to use the tool (to typeset a spec) and a key prerequisite (LaTeX installation). However, it does not provide contraindications or explicit comparisons to sibling tools, though the sibling names offer implicit differentiation.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla specification file | |
| cfg_file | No | Path to .cfg file (defaults to same basename as tla_file with .cfg extension) | |
| workers | No | Number of worker threads, or 'auto' for all cores | |
| deadlock | No | Check for deadlock (default true). Set false to disable deadlock checking. | |
| continue | No | Continue model checking after finding a violation | |
| dfid | No | Use depth-first iterative deepening with given depth | |
| diff_trace | No | Show only changed variables between trace states | |
| max_set_size | No | Override TLC's max set size (default 1000000) | |
| generate_states | No | Dump state graph in DOT format | |
| dump_path | No | Override directory path for DOT state graph dump (default: <cwd>/states). Parent directories are created if needed. | |
| extra_args | No | Additional raw arguments to pass to TLC | |
| output_file | Yes | Required absolute path. Raw TLC output is written here so it doesn't flood the agent context. Response contains the output_file path; callers Read the file when they need the raw text. |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden for transparency. It describes what the tool checks but does not disclose side effects (e.g., file outputs, resource usage), performance characteristics (long runs), or error handling. The output file behavior is only noted in the parameter schema, not the main description.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is two sentences with no superfluous words. The first sentence encapsulates purpose and mode; the second adds detail on what is checked. It is front-loaded and every sentence adds value.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool complexity (12 parameters, no output schema), the description is insufficient. It does not explain the return behavior (output file path), performance warnings, result interpretation, or actions on violation. The output_file parameter is required but its role is not highlighted in the main description.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so baseline is 3. The main description adds minimal value beyond the schema, only mentioning 'optionally deadlock freedom' which is already clear from the deadlock parameter default. No additional parameter semantics are provided.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Run TLC model checker in exhaustive breadth-first mode') and the resource ('TLA+ specification'), specifying what is verified ('all reachable states against invariants, properties, and deadlock freedom'). It distinguishes well from siblings like tlc_simulate which runs in simulation mode.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage for exhaustive verification but does not explicitly state when to use this tool versus alternatives (e.g., tlc_simulate for quick checks, tlc_generate_trace_spec for trace generation). No 'when not to use' guidance is provided.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla specification file | |
| cfg_file | No | Path to .cfg file (defaults to same basename as tla_file with .cfg extension) | |
| interval_minutes | No | Coverage reporting interval in minutes (default 1) | |
| workers | No | Number of worker threads, or 'auto' for all cores | |
| extra_args | No | Additional raw arguments to pass to TLC |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided, so description must fully disclose behavior. It mentions output type (action counts, states) but omits side effects, resource usage, output format, or how results are returned (stdout/file), falling short for a computational tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Two concise sentences. First states the action, second explains the benefit. Every word earns its place.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given no output schema and 5 parameters, description covers main purpose but lacks details on output format, return behavior, or how parameters like extra_args or interval_minutes affect results.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so description adds no extra parameter meaning beyond what the schema already provides. Baseline score applies.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
Description uses specific verb 'run' and resource 'TLC model checker' with mode 'action coverage reporting', clearly distinguishing from siblings like tlc_check (invariant checking) and tlc_simulate (simulation).
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Description implies usage for identifying under-explored spec parts but provides no explicit when-to-use or when-not-to-use guidance, nor comparisons to sibling tools.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla file | |
| cfg_file | No | Path to the .cfg configuration file. Defaults to <tla_file>.cfg | |
| monolith | No | Generate a monolithic SpecTE (single file). Set false for multi-file output. | |
| extra_args | No | Additional TLC arguments |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It discloses the key behavior (runs TLC with -generateSpecTE, produces files), but does not explain side effects, error handling, or requirements (e.g., TLC installation, output overwrite behavior). This is adequate but not thorough.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is two sentences, front-loaded with the action, and then the purpose. Every sentence contributes value with no wasted words. Highly concise and well-structured.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given no output schema and no annotations, the description should cover return values and prerequisites. It mentions output files but not their content or structure. It does not explain failure modes or dependencies (e.g., TLC path). Sufficient for basic understanding but lacks completeness.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so the baseline is 3. The description does not add extra meaning beyond the schema's parameter descriptions; it only restates the purpose of the tool. No additional value for parameter understanding.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool runs TLC with -generateSpecTE to produce a Trace Explorer spec (SpecTE.tla/cfg). It identifies the specific verb and resource, and hints at debugging counter-examples, but does not explicitly differentiate from sibling tools like tlc_check or tlc_simulate.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description mentions it is useful for debugging counter-examples, providing context for when to use it. However, it lacks explicit guidance on when not to use it or suggestions of alternative tools (e.g., tlc_check for general model-checking, tlc_simulate for simulation).
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla specification file | |
| cfg_file | No | Path to .cfg file (defaults to same basename as tla_file with .cfg extension) | |
| depth | No | Maximum depth of each simulation trace (default 100) | |
| num_traces | No | Number of traces to generate | |
| seed | No | Random seed for reproducibility | |
| aril | No | Aril (adjusts the random seed) | |
| workers | No | Number of worker threads, or 'auto' for all cores | |
| deadlock | No | Check for deadlock (default true). Set false to disable deadlock checking. | |
| diff_trace | No | Show only changed variables between trace states | |
| extra_args | No | Additional raw arguments to pass to TLC |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, and the description only mentions that simulation is faster but incomplete. It does not disclose potential side effects, authorization needs, or limitations beyond incompleteness.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Two sentences succinctly convey the purpose, advantage, and typical use cases without any fluff or repetition.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description provides essential information but lacks details on output format or behavior of specific parameters, which is somewhat acceptable given the high schema coverage and the tool's exploratory nature.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
All 10 parameters have descriptions in the schema (100% coverage), so the description adds no extra meaning beyond what is already in the input schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool runs TLC in simulation mode to randomly explore execution traces, distinguishing it from exhaustive checking. It highlights specific use cases: large state spaces or quick smoke tests.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage for large state spaces or smoke tests when exhaustive checking is too slow, but does not explicitly state when not to use it or mention alternative tools like tlc_check for exhaustive verification.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v0.2.1pcal_translatetla_evaluatetla_parsetla_state_graphtla_textlc_checktlc_coveragetlc_generate_trace_spectlc_simulateScored 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
Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.
Official DevSpeak MCP server — translate technical text into formal specs from any AI IDE or agent
