February 2025 Monthly Development Update

You’re reading the TLA⁺ Foundation monthly development update. 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 or some important part of it that wasn’t captured in the summary, worry not - these newsletters will be published 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 interesting non-coding-related developments & announcements:

• The TLA⁺ Community Event 2025 will be co-located with ETAPS 2025 in Hamilton, Ontario, Canada on May 4th, 2025. The talk submission deadline is Friday, February 28th; hopefully we’ll have some great talks in store and we look forward to seeing you there!
• 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.
• In Europe, ABZ 2025 - the 11th International Conference on Rigorous State-Based Methods - will take place from June 10th to 13th of 2025 in Düsseldorf, Germany and will hopefully have some TLA⁺-related talks.
• Hillel Wayne wrote a post exploring the idea of “Rosetta problems” for formal specification - common simple problems for comparing different formal specification languages by looking at how each language solves each problem.

Now on to coding-related community developments:

• Calvin Loncaric ran some benchmarks on the SANY TLA⁺ parser and found latency could be greatly improved by using Graal native images. He contributed a fix to SANY’s dependency loading code so it works with TLA⁺ modules embedded within the images, also taking the opportunity to improve the code’s clarity (1, 2). Latency is important to consider as more applications move to consume SANY as a dependency.
• Stephan Merz explored using TLA⁺’s proof language to analyze monotonic systems. Distributed system designs commonly use monotonicity with elements like increment-only counters or append-only logs. Monotonic systems have an unbounded state space so are difficult to analyze with finite model-checking. Stephan proved convergence of a conflict-free replicated datatype and validated the proof using TLAPM.
• Federico Ponzi contributed a fix for erroneous syntax highlighting in the TLA⁺ VSCode extension, ensuring operator definitions are not highlighted inside comments. While a tree-sitter grammar for TLA⁺ does exist, VSCode does not support it and so it is necessary to maintain a regex-based TextMate grammar for syntax highlighting.
• William Schultz made a number of updates to spectacle, a JavaScript-based interpreter for TLA⁺ previously known as tla-web. In particular, support was added for calling operators in modules imported as instances.
• Karolis Petrauskas landed a fix for a race condition in the TLA⁺ language server when running multiple concurrent TLAPM backend provers. He also looked into strangely long processing times in the TLAPM parser (1, 2); the level-checker turned out to be the culprit, exhibiting exponential-time behavior on some inputs.
• Damien Doligez worked on speeding up the TLAPM level-checking process using memoization.
• Julia Ferraioli had previously submitted TLA⁺ for inclusion in the Amazon Web Services Open Source Credits Program. It was recently accepted, so Finn Hackett and Markus Kuppe worked to revive performance tests for the TLC model checker!
• Longtime TLA⁺ Tools maintainer Markus Kuppe continued investigation of fingerprint duplication issues arising during long-running model checking (1, 2), fixed a bug with TLC using the wrong value in parameterized spec instances, and investigated lasso-shaped liveness examples failing to reconstruct when a VIEW is defined.

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

• I worked with Calvin Loncaric to design a new API for the SANY TLA⁺ parser, supporting emerging use-cases and setting us up to easily expose more capabilities in the future.
• The bulk of my time went toward developing a semantic test corpus for TLA⁺: a large set of implementation-independent test files filled with assertions about semantic properties like identifier resolution and expression level (roughly analogous to type-checking) which various TLA⁺ tools can adopt to verify conformance with the language specification. This sort of work is dull, slow, and seemingly endless - but I know from experience how wonderful it is to have an existing test corpus to rely on & add to over time! At this point the tests cover most of the important parts of the language, although there are always more cases to consider.
• I did some testing & refactoring of SANY’s error reporting machinery to facilitate future implementation of standardized error codes in TLA⁺ parsing. In addition to the clear usability improvement of including such codes in user-visible error messages for reference, they would enable development of a negative counterpart to the semantic test corpus: a set of specifications which should each trigger a specific error code when parsed.
• I did some minor refactoring of existing SANY tests (1, 2) using JUnit’s class parameterization & assume functionality to control test execution.
• I wrote two RFCs proposing un-contentious changes to the TLA⁺ language standard (1, 2). While both RFCs address issues that ought to be definitively decided, I think they are primarily useful as exercises for figuring out what the full end-to-end language standard update process actually is. We can then apply that same process to more-exciting RFCs, like combining set map & filter into a single language construct!

Newbie Corner

Here we highlight an issue that would be a good choice for new contributors! This one is a bit more advanced than past months, but hopefully someone can rise to the challenge: we want TLC to interpret expressions of the form CHOOSE x : x ∈ S. Ordinarily this would be an unbounded choose error, but this specific form of the expression is obviously bounded (the bound is just given in the body!) and is much nicer to write than the clunky CHOOSE x ∈ S : TRUE.

To solve this issue you will need to:

1. Figure out where TLC raises the unbounded choose error
2. Modify the logic to first check whether the choose body is just the ∈ infix operator, defining an expression of the form x ∈ S
3. If so, evaluate the choose expression as though the bound is S instead of raising an error

As a bonus you can extend this work to support larger sets of reasonable expressions, like CHOOSE x : x ∈ S ∧ ….

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

• January 2025: fix the PlusCal CLI -labelRoot option
• December 2024: add parser support for backticks in strings