u/Anxious_Tool

Hi all,

Just shipped an MCP server some of you might find useful: **tla-mcp**.

TLA+ is a formal-spec language for designing concurrent and distributed
systems. You describe what your protocol should do and a model checker
tries every reachable state to catch invariant violations, deadlocks,
race conditions you didn't see coming. With tla-mcp registered, Claude
Code can call the checker as a first-class tool: validate a spec, run a
bounded check with a counterexample trace, replay specific scenarios, all from inside the chat.

Tool descriptions are deliberately opinionated about how the model
should use the checker (budget all limits upfront, treat `limit_reached`
as inconclusive, look at the last transition of a trace first) so the
guidance survives context truncation.

Install + client config snippet + tour of the four tools is on the
landing page: **https://fabracht.github.io/tla-rs/**

It's an experiment. Feedback and bug reports welcome.

Hello everyone,

It's been a while since I last posted about the tla crate in Rust (https://github.com/fabracht/tla-rs). We had many contributions over the months and interest seems to be steadily increasing. I would like to thank everyone for the support and interest.

I'm here today to announce a new experiment with tla-rs: the `tla-mcp server`. It exposes the model checker as a Model Context Protocol server so agentic clients can call it as a first-class tool to validate a spec, run a bounded check, inspect counterexamples, replay scenarios, all from inside the chat.

Install instructions, client config, and a quick tour of the four tools are on the landing page: **https://fabracht.github.io/tla-rs/\*\*

It's an experiment. I have started simple, so feedback, bug reports, and war stories welcome.

MCP server for the TLA+ model checker tla-rs

MCP server for the TLA+ model checker tla-rs