May 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 2025 TLA⁺ Community Event was held alongside ETAPS 2025 in Hamilton, Ontario, Canada on May 4th, 2025. We had a good slate of talks, and the recordings have now been posted. Thanks to the organizers Igor Konnov, Markus Kuppe, Murat Demirbas, and Stephan Merz for putting on a great conference!
  • The TLA⁺ Foundation, in collaboration with NVIDIA, is holding a GenAI-Accelerated TLA⁺ Challenge! This is an open call for submissions exploring the intersection of TLA⁺ and generative AI. Entries must be submitted by July 3rd, 2025 and will be judged by the TLA⁺ Specification Language Committee. First place wins a NVIDIA RTX 5090 GPU!
  • 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!

Posts & Papers

Community TLA⁺ Tooling Updates

Work done by community members on non-TLA⁺ Foundation-managed projects:

Core TLA⁺ Tooling Updates

Work done by community members on TLA⁺ Foundation-managed projects:

TLA⁺ Foundation-Funded Updates

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

  • I spent a lot of time expanding the Create your own TLA⁺ tools tutorial series, trying to encode as much knowledge about parsing TLA⁺ as possible. As a highlight, the tutorial now has a module on parsing vertically-aligned conjunction & disjunction lists. The tutorial as a whole is nearly complete; I’ve finished writing the code for two of the final three modules (operator parameters, actions, then safety checking) and now need to write them up.
  • I created & delivered a talk at the TLA⁺ Community Event summarizing the current state of TLA⁺ development, what the TLA⁺ Foundation has been funding to improve it, and what I want to see in the near future. I also summarized the talk in a blog post.

In the next month I am hoping to focus on becoming more familiar with the TLAPM parser interface before transitioning it to use SANY.

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 is probably one of the most advanced issues yet profiled in this series, but it’s very interesting. William Schultz reported a bug where TLA⁺ cannot handle constraints like <<y>>' = <<y>>, which should be a synonym for UNCHANGED y and y' = y.

Why is this bug interesting? When evaluating an action, TLC has to do a weird double-duty where it both evaluates the action as a simple logical predicate over variables - evaluating to true or false - while also extracting hints about the possible values of those same variables! Consider what happens when TLC sees an action like:

Action ==
  /\ x = 0
  /\ x' = x + 1

When it evaluates the expression x' = x + 1, it doesn’t yet know the value of x'! It has to slyly recognize that the as-yet-undefined value of x' is on the left hand side of an equals operator, so can be assigned/constrained to the value x + 1; then, having defined the value of x', it evaluates x' = x + 1 as an ordinary expression which will of course be true.

Wrapping your head around this weird double-duty of TLC’s interpreter will bring you great understanding of TLA⁺ tool internals. In TLA⁺, it isn’t only variables that can be primed - entire expressions can be primed. When that happens, it is the same as individually priming all the variables within that expression. So, <<y>>' is the same as <<y'>>.

There are two plausible approaches to fixing this issue. First, you could look at how TLC evaluates the equals operator at runtime when both parameters are tuples, and more specifically when the left-hand-side is primed. Second, you could consider the approach of statically de-sugaring expressions like <<x, y, z>>' = <<e1, e2, e3>> into x' = e1 /\ y' = e2 /\ z' = e3 in the parser, so the transformation cost is only paid once instead of every time the expression is evaluated.

It will be a challenge to fix this issue, but you will come out the other side with a very solid grasp of the tools and what sort of TLA⁺ specs are possible to model check.

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