Get the latest tech news
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:
Modulo some weirdness around conversions between functions and sequences, many industry-produced TLA⁺ specs have variables spanning a small set of values and would benefit from catching type errors at parse time. So, we have a large quarter-century-old Java codebase that is difficult to unit test due to prolific global static state, where all the original authors have long since left the project, and where the three regular core contributors lack knowledge of its many parts. along with a semantic-level test suite with lots of in-language assertions about levels and references (thanks to lobste.rs users for some great suggestions on its design) and - my favorite - a set of 150ish TLA⁺ parse inputs that should each trigger a specific standardized error code in any conformant parser.
Or read this on Hacker News
