The current state of TLA⁺ development
a year ago
- #Model Checking
- #TLA+
- #Software Development
- The 2025 TLA+ Community Event was held at McMaster University in Hamilton, Ontario, Canada.
- The event featured a talk titled 'It’s never been easier to write TLA+ tooling!' discussing the state of TLA+ development.
- Key topics included an overview of existing TLA+ language tooling, overcoming legacy code challenges, and future development ideas.
- Existing tools include parsers (SANY, TLAPM, tree-sitter-tlaplus), interpreters (TLC, Spectacle), and model checkers (TLC, Apalache, Spectacle).
- Other notable tools include TLAPM, Snowcat Type Checker, TLA+ formatters, LSP Server, TLAUC, and VS Code Extension.
- Challenges include maintaining legacy code like SANY and TLC, which are large, old Java codebases with limited living knowledge.
- Strategies to overcome challenges include developing comprehensive test suites, improving developer onboarding, and providing grants and stipends.
- Future ideas include generative testing for TLA+ tools, syntax simplifications, and improving the SANY API.
- The 'One Billion States Per Minute Initiative' aims to significantly increase TLC model checker throughput by developing a bytecode interpreter.
- The TLA+ Foundation supports tool development and is looking for more contributors.