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.