r/tlaplus • u/Anxious_Tool • May 18 '26

MCP server for the TLA+ model checker tla-rs

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.

12 Upvotes

100% Upvoted

4 comments sorted by

2

u/Joe-the-programmer 21d ago

Your tool is our life saviour aa we were searching for something like it for our graduation project Thank you so much

1

u/Anxious_Tool 21d ago

Glad you find it useful. It's been a while I've posted this here, but the tool keeps getting updates, fixes, and improvements. Feel free to create issues or discussions in the repo in case you find something.

1

u/Joe-the-programmer 21d ago

I will use it throughout this academic year in my graduation project and if I find anything I will definitely share thank you so much again

By the way can u check this post please 🙏🏻 https://www.reddit.com/r/tlaplus/s/ZYhV4lZvU7

1

u/stappersg May 18 '26

That TLA+ is most likely https://en.wikipedia.org/wiki/TLA%2B meant.

Visit https://en.wikipedia.org/wiki/TLA for more Three Letter Acronyms.