August 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

Posts, Papers, and Specs

  • Lorin Hochstein wrote a post about how formal specifications differ from a traditional program: a program is a list of instructions, and a formal specification is a set of behaviors.
  • Igor Konnov wrote about proving completeness of an eventually perfect failure detector in Lean4, comparing & contrasting it to solving the same problem in TLA⁺.
  • Jarod Differdange contributed two TLA⁺ specifications from his master’s thesis to the TLA⁺ examples repo. The first spec is of a barrier for synchronizing threads, and the second uses auxiliary variables to achieve bidirectional refinement between Peterson’s algorithm and an abstract lock; the thesis itself can be read here.
  • AI startup Crackd has launched a new platform to incentivize development of TLA⁺ specifications for training LLMs. Contributors will write a formal TLA⁺ spec corresponding to an informal specification document, along with a programming language implementation of the same system; they are then compensated according to the complexity of the problem. Interested potential contributors can fill out the form at https://www.getcrackd.ai/.

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!

  • In the Java-based core TLA⁺ tools, I fixed a bug introduced by my recent SANY output control changes, which inadvertently silenced detailed parser error messages in some cases. I also extended my previous error code standardization work to encompass PlusCal translation-hash mismatch warnings. In service of recent user requests to support reading TLA⁺ specs from non-file sources, I proposed some refactorings to SANY’s core NamedInputStream class. Finally, I developed a set of tests for SANY’s tokenizer and the parser’s belchDEF method, a small but critical method that identifies the start of new operator definitions.
  • For my main task of transitioning TLAPM to use SANY as its parser, I continued 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 work seems approximately 75% complete, in terms of number of distinct TLA⁺ AST node types for which a translation funtion has been written. One parser bug has been identified through this work.
  • I did some work on the TLA⁺ Examples repo, simplifying the CI & spec contribution process (1, 2, 3, 4) and adding some additional example specs to CI validation (1, 2).

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 looking at adding a capability to TLC’s model file format: the EXPECT statement. Sometimes, users want a model-checker run to fail in an interesting way, for example if the spec has identified a particularly interesting bug. For this it would be useful to have an EXPECT construct so the user can define the expected result of running a model - be that success, invariant violation, or otherwise. If TLC finds an invariant violation, ordinarily it will exit with a nonzero exit code. However, if the model file contains an EXPECT statement that an invariant violation is expected, it should exit with a zero (success) error code instead.

The work required is roughly:

  1. Locate the TLC model file parsing code and add support for EXPECT syntax
  2. Propagate the EXPECT value back to the top level of TLC, modifying the command-line exit code logic to exit with a zero code if the result is as specified by EXPECT

Since this issue involves modifying TLC’s exit code logic, it’s similar to the issue highlighted in the June 2025 newsletter. If you fix one issue, it would probably be easy for you to fix the other!

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