The current state of TLA⁺ development

Summary

The 2025 TLA⁺ Community Event was held last week on May 4th at McMaster University in Hamilton, Ontario, Canada. It was a satellite event to ETAPS 2025, which I also attended, and plan to write about in the near future. I gave a talk somewhat-hucksterishly titled It’s never been easier to write TLA⁺ tooling! which I will spin into a general account of the state of TLA⁺ development here. The conference talks were all recorded, so if you’d like this blog post in video form you can watch it below: Outline The thesis of this post is that almost all the dreams & desires we have for TLA⁺ are downstream of making it easy to develop in or on TLA⁺ language tooling. We break this down into three parts: Overview of existing TLA⁺ language tooling Overcoming the legacy code challenge Some TLA⁺ development ideas for the near and middle future I’m very optimistic about the future of TLA⁺, despite the challenges. We now have the TLA⁺ Foundation, which has very generously been paying me a comfortable living wage to work on the tools for the past six months. I will talk about some of the things I’ve accomplished. Being paid to work on FOSS is a blessed existence; if that sounds appealing to you as well, the TLA⁺ Foundation is looking to fund more contributors! This is a summary of what TLA⁺ language tooling exists, to stoke the imagination for what tools you could contribute to or build upon. Parsers Parsers are of course the foundation of any language tooling, because your tools need to know what some source code actually says. We have a decent stable of them: SANY (Syntactic ANalYzer) - our flagship parser, a Java-based recursive descent parser generated by JavaCC. This is the only parser that really handles all the syntax and does a lot of semantic checks (including level-checking, which is the closest thing TLA⁺ has to type checking) that other parsers don’t. The TLAPM parser - a parser-combinator-based OCaml parser, this is used by the TLA⁺ Proof System. It handles almost all TL...