tlaplus-mcp
Exposes the TLA+ toolchain (TLC, SANY, PlusCal, TLATeX) as structured JSON tools via the Model Context Protocol, enabling AI assistants to parse, check, simulate, and typeset TLA+ specifications.
Caution. Specific findings reduced this grade. They are listed on the page. Grades reflect the full trust pyramid: code, verification depth, and reputation. New projects cap at C until adoption is earned.
How we verified
Verified is a snapshot. Live keeps it current, and builds your track record.
⚡ Connect GitHub → continuous verification on every pushwhy connect →Who stands behind it
richashworth
Source: Glama
Claim it to get a verified publisher badge, a free copy of our full audit findings, and direct contact for any high-priority issues we find. Or connect your repo for our deepest verification, Live Monitored: read-only, revoke anytime. What we access →
Install from
The grade above is for the source repository. Registries can serve a different version, so we mark the ones we were not able to read.
These names and descriptions are the publisher's own, read from the source code. We print them as written. Our assessment is the findings above, not this list.
pcal_translateTranslate 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.
tla_evaluateEvaluate a constant TLA+ expression using TLC. Creates a temporary spec that prints the result of the expression.
tla_parseParse and syntax-check a TLA+ module using SANY (Syntactic Analyzer). Returns parse errors and the list of modules parsed.
tla_state_graphLoad 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.
tla_texTypeset a TLA+ specification into a PDF or DVI file using TLATeX. Requires a LaTeX installation (pdflatex or latex) to be available.
tlc_checkRun 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_coverageRun 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.
tlc_generate_trace_specRun 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_simulateRun 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.
Disclosed vulnerabilities in this server's declared npm dependencies (via OSV). Whether each is reachable depends on the installed versions.
When Vitest UI server is listening, arbitrary file can be read and executed
TLC_JAR_PATHThe server auto-downloads tla2tools.jar to ~/.tlaplus-mcp/lib/ on first use. Set to override.TLC_JAVA_OPTS-Xmx4g -XX:+UseParallelGCTLC_TIMEOUT300TLC_WORKSPACECurrent working directoryTool annotations
No tools have read-only/destructive annotations
Add readOnlyHint or destructiveHint annotations to every tool so hosts can warn users before invoking.
All four hints declared on every tool
9/9 tools missing one or more hints — pcal_translate (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint); tla_evaluate (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint); tla_parse (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint), +6 more. OpenAI's directory rejects tools where any of the four hints are missing or non-boolean.
For every tool, set all four hints (readOnlyHint, destructiveHint, idempotentHint, openWorldHint) to explicit true/false values that match the handler’s actual behaviour.
Destructive tools are labelled
5 tools perform destructive updates without destructiveHint — tla_evaluate deletes at line 138 (unlinkSync(tlaPath)); tlc_check deletes at line 161 (rmSync(metaDir, { recursive: true, force: true })); tlc_coverage deletes at line 92 (rmSync(metaDir, { recursive: true, force: true }))
Add destructiveHint:true to any tool whose handler calls .delete(), .upsert(), .update(), unlink, rm, DELETE, DROP, REPLACE INTO, or any operation that overwrites existing data.
Descriptions match behaviour
2 tools describe read intent but their handlers mutate — tla_parse (line 54: parsingFileRe.exec(output)); tla_state_graph (line 290: fs.mkdirSync(dirname(outputFile), { recursive: true }))
Rename the tool, rewrite the description, or move the side-effect into a separate clearly-named tool.
Tool inputs are validated
Only 1/9 tool handlers declare input schemas (11%)
Declare an inputSchema with zod/joi/yup on every tool definition.
Dev dependencies
1 critical/high in dev-only deps (does not ship to users)
Upgrade dev dependencies when convenient.
Tool description accuracy
tla_parse: description implies read-only but handler writes/deletes/executes; tla_state_graph: description implies read-only but handler writes/deletes/executes
Update tool descriptions to accurately reflect all capabilities — especially write, delete, or execute operations.
Claim the listing to review these findings one by one and send us a correction where you disagree, straight to the team. Claiming also means we tell you when the grade moves, and reach you first if we find anything urgent.
[](https://m8ven.ai/mcp/richashworth/tlaplus-mcp)?variant=verified from the URL.Vetting this one by hand? Tool Check is an MCP that scores other MCPs. Add it once and ask Claude, ChatGPT, or any MCP client to grade a server, surface CVEs, check the publisher, and suggest safer alternatives — before you install.
https://m8ven.ai/api/mcp/tool-check