Revitalizing TLA⁺: A Call to Arms for Tool Development

The 2025 TLA⁺ Community Event highlighted the current state and future direction of TLA⁺ tooling. The author argues that ease of development within the TLA⁺ ecosystem is paramount. Existing parsers, interpreters, and model checkers are reviewed, alongside challenges such as legacy code and documentation gaps. Strategies to overcome these hurdles include test-driven development, developer onboarding, and grants. Future directions include generative testing and syntax simplification, culminating in an ambitious goal: boosting TLC's throughput to 1 billion states per minute.