July 2025 Monthly Development Update

This is the TLA⁺ Foundation monthly development update (subscribe via RSS). Here we summarize the past month of development for the benefit of Foundation patrons and interested members of the community. We will also highlight a good bug or small feature for prospective new contributors to look at! If your TLA⁺ contribution was missed, worry not - we publish monthly, so it’s easy to hop on the next train; open an issue here.

If you’re interested in getting involved in the TLA⁺ community:

  • Learn TLA⁺ starting here!
  • Join the monthly virtual community meetings here!
  • Read the mailing list here!
  • Start hacking on the tools themselves here!

Organizational Updates

  • The TLA⁺ Foundation grant program is continuing on a rolling basis; please submit a proposal if you have ideas to improve TLA⁺ so the Foundation can support you financially as you work on them. You can find some desired projects listed here. If you’re trying to figure out the next stage of your career and like the sound of being paid a stipend to work on free & open source software in the formal methods space, this is a great opportunity!
  • The GenAI-Accelerated TLA⁺ Challenge submission date was on July 3rd. Four submissions were received, and the winners will be announced at the start of August!

Posts & Papers

TLA⁺ Docs & Tooling Updates

TLA⁺ Foundation-Funded Updates

Here are things Andrew Helwer (author of this post) worked on - all funded by the TLA⁺ Foundation!

  • For my main task of transitioning TLAPM to use SANY as its parser, I have been translating the TLAPM syntax tree into a standardized S-expression format for comparison with an expected S-expression parse tree across a standardized set of TLA⁺ parse inputs. This builds familiarity with the TLAPM AST format and ensures thorough test coverage during the transition to using SANY.
  • For the Create your own TLA⁺ tools how-to guide, I completed the crucial chapter on variables, states, and actions. Here learners encounter the strange dual nature of interpreting TLA⁺, where statements both evaluate to values and reveal possible next states of the system. Only two chapters remain: one on how to model-check TLA⁺ (largely trivial once a next-state interpreter has been written) and a final one on the surprisingly subtle method of evaluating operator arguments lazily so that TLA⁺ operators can work like macros expanding into parameter-free expressions.
  • In the Java-based core TLA⁺ tools, I worked to support greater control over output and error reporting in the SANY parser. I also did some refactoring, replacing a custom internal stack class with the Deque class from Java’s standard library.
  • I supported Stephan’s TLAPM upgrade & proof fixing efforts by adding some proof checks to the TLAPM CI and fixing a bug in state count recording logic in the TLA⁺ examples repo.

This past month also saw longtime TLAPM contributor Karolis Petrauskas receive a TLA⁺ Foundation grant to work on decomposing TLA⁺ proofs in the VS Code extension, by implementing a new LSP code action.

Newbie Corner

Here we highlight an issue that would be a good choice for new contributors! Before starting work, be sure to read the contribution guidelines and discuss your planned approach with maintainers.

This month we’re back down in the depths of the parser. The Java-based SANY parser allows the @ symbol in places it shouldn’t, such as constant or operator definitions. The @ symbol is ordinarily used in statements like [f EXCEPT ![x] = @ + 1] to refer to the un-modified function value.

There are a few different ways to fix this. One possibility: at the lexer level, separate @ from the general identifier regular expression, then selectively allow @ in various places (for example, as an atom in ordinary expressions) at the syntax parser level. Existing resolution machinery would then catch @ being used outside of EXCEPT expressions.

Issues highlighted in past months have also yet to be claimed!