June 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, 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

TLA⁺ Tooling Updates

TLA⁺ Foundation-Funded Updates

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

  • For the Create your own TLA⁺ tools how-to guide, I completed writing the chapter on functions, operators, and parameters. This included a very fun algorithm for enumerating through variable bindings in expressions like \E x, y \in Nat : P(x, y). I also finished writing, refining, & testing the code for the very involved chapter on finding next states, and wrote its first draft. TLA⁺ is quite a strange language to interpret!
  • Transitioning TLAPM to use SANY as its parser has moved to the implementation phase. To prepare, I spent a week working through the book Real World OCaml to understand the more advanced parts of the language. I also experimented with using GraalVM Native Images to expose a C API from SANY Java code, as a potential alternative to deserializing the syntax tree from SANY’s XML output. I am currently familiarizing myself with TLAPM parser internals by extending previous work subjecting it to a corpus of standardized syntax tests - previously only in a pass/fail manner - to also check the equivalence of the expected parse tree.
  • In the Java-based core TLA⁺ tools, I fixed some longstanding warnings in the JavaCC parser generation process, then made some changes to support greater control over SANY’s output by merging the abort & error classes and appending the error causing an abort to the thrown exception.

The TLA⁺ Foundation also funded a new research-oriented grant to Ian Dardik, a Software Engineering PhD student at Carnegie Mellon University. In his own words, here is the problem the grant is funding him to solve:

Showing that a TLA+ specification is safe (e.g., satisfies an invariant) is usually done through model checking. However, for specifications that are infinite-state or parameterized, one must find an inductive invariant to prove safety. Inductive invariant inference — the task of automatically finding an inductive invariant — is an important, tough, and consequently a well-studied research area. Past research papers propose techniques that can find more complex inductive invariants for more complex specifications. In this grant, however, we propose a new compositional technique for finding inductive invariants, in which we aim to find multiple smaller local inductive invariants. At a high level, we perform four steps: (1) decompose a specification into components, (2) write an assume-guarantee contract for each component, (3) infer a local inductive invariant for each contract, and then finally (4) stitch the local inductive invariants together to create a global one. A key part of this process is finding an assume-guarantee contract for each component in step (2); we also are building tooling for this step as part of this grant.

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, it’s about emitting a different exit code when the TLC model checker finds a liveness property counter-example that ends in stuttering, versus when the counter-example ends in a multi-state infinite loop. This would be helpful for the growing number of programs which iteratively run TLC & consume its output. You can find & begin discussing the feature proposal here.

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

New contributor Max Moiseev took a crack at the issue highlighted in the December 2024 newsletter on adding parser support for backticks in strings. It turned out to be much more complicated than expected! SANY does already support backticks in strings, but they have to be balanced by apostrophes; these are translated into UK English-style inverted commas by the tla2tex tool. Astonishingly this also uncovered that SANY (probably unintentionally) supports multi-line strings! So what was thought to be a simple beginner issue ended up being brought before the TLA⁺ Specification Language Committee to decide what TLA⁺ should actually do here. I try to find easy issues but you just never know in software development!