March 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!

Let’s start with some organizational, conference, blog post, and user-side TLA⁺ happenings:

Now on to coding-related community developments:

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

  • I created a semantic error test corpus for TLA⁺, a large set of small TLA⁺ files that should each trigger a specific standardized parse error. This corpus was developed by finding all locations in the Java-based SANY TLA⁺ parser where a parse error is reported, then attempting to reverse-engineer a parse input triggering that error. This greatly improves SANY test coverage, and also serves as an implementation-independent behavior standard for other TLA⁺ parsers to adopt.
  • I supported Markus’s work on updating the monotonic systems examples by adding some features (1, 2) to the TLA⁺ examples automated validation tooling, and also expanded documentation to hopefully reduce the difficulty of contributing example specifications.

Newbie Corner

Here we highlight an issue that would be a good choice for new contributors! This one is substantial, similar in genre to last month: extending the Java-based TLA⁺ interpreter to handle a wider variety of expressions. Calvin Loncaric proposed allowing \subseteq/⊆ in TLA⁺ next-state relations; currently the interpreter only supports the logically-equivalent ∈ SUBSET operator. This work could also be easily extended to support the \subset/⊂ operator (without equality). Similar to last month, the high-level steps required to implement this feature are:

  1. Figure out where TLC implements the ∈ functionality for next-state relations, while disallowing operators like \subseteq/⊆.
  2. Modify the logic to translate ⊆ to an execution form equivalent to ∈ SUBSET.
  3. Write tests to validate these changes.

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