The current state of TLA⁺ development

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 comfortab ... Read full article.