December 2024 Monthly Development Update

Hello! You’re reading the inaugural edition of the TLA⁺ Foundation monthly development update. Here I’ll summarize the past month of development for the benefit of Foundation patrons and interested members of the community. These posts are authored by Andrew Helwer and while I’ll focus a fair bit on my own work (as a way of providing a monthly status update to the Foundation, really), I will also provide a rundown of other happenings in the community! If I missed your contribution or there was some important part of it I didn’t capture in the summary, worry not! These newsletters will be published monthly so it’s easy to hop on the next train; try opening an issue here.

If you’re interested in getting involved in the TLA⁺ community:

  • Learn TLA⁺ starting here!
  • Read the mailing list here!
  • Join the monthly virtual community meetings here!
  • Start hacking on the tools themselves here!

Let’s start with some interesting non-coding-related developments & announcements:

  • Leslie Lamport published a new book, titled A Science of Concurrent Programs! It’s freely available for download but a physical edition is in the works. I’ve been reading & enjoying it and asking lots of questions on the mailing list. It’s very much focused on the “TLA” part of TLA⁺ (meaning the Temporal Logic of Actions) so it’s a good read if you want to go really in-depth on the logical theory underpinning the TLA⁺ language.
  • The TLA⁺ Community Event 2025 was announced, to be co-located with ETAPS 2025 in Hamilton, Ontario, Canada on May 4th, 2025. We hope to see you there! The talk proposal submission deadline is February 7th, 2025.
  • East of the Atlantic, 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. TLA⁺-related papers are welcome; the deadline for submitting abstracts is February 3rd, 2025.
  • Jack Vanlighty wrote a blog post on using TLA⁺ to obtain statistical properties of distributed system designs.
  • Lorin Hochstein has been on a TLA⁺ blogging tear, publishing three excellent blog posts in quick succession: Specifying serializability in TLA⁺, Multi-version concurrency control in TLA⁺, and Extending MVCC to be serializable, in TLA⁺. The first post is especially effective as an introduction to using refinement to express whole-system safety properties that just can’t be done with single-state formulas.
  • At the November virtual community meeting, Feng Wenhan presented his work using the TLC state graph export function to drive model-based testing; some shortfalls in the state graph export functionality led to the proposal of designing a robust state graph export format.
  • Also at the November virtual community meeting, Leslie Lamport announced his retirement at the end of the year at the age of 83. A well-earned rest, although his contributions will be missed!

Now on to coding-related community developments:

  • Federico Ponzi is prototyping a TLA⁺ Formatter, including hammering down the default settings. If you have opinions on how TLA⁺ should look, now is a great time to weigh in!
  • Julia Ferraioli updated the TLA⁺ Foundation website with blogging capabilities, facilitating the very post you are reading right now! She chose the Hugo static site generator, of which I am also a fan.
  • William Schultz released Scimitar, a tool for verifying the safety of distributed protocols based on the technique of inductive proof decomposition in TLA⁺.
  • Hillel Wayne has started contributing to the TLA⁺ VS Code plugin, adding some nice diagnostic messages for PlusCal.
  • Ioannis Filippidis landed some long-awaited changes adding support for bound tuple quantification to the TLA⁺ Proof Manager (TLAPM), reviewed by Damien Doligez. This enables TLAPM to parse quantification expressions that use tuple destructuring, like ∀ ⟨x, y⟩ ∈ ℕ × ℕ : x + y ∈ ℕ.
  • We welcomed Mathieu Borderé as a new contributor as he landed his first PR in the TLA⁺ tools, improving command line help output for the parser!
  • Longtime TLA⁺ Tools maintainer Markus Kuppe submitted many changes, focused on the TLA⁺ debugger (1, 2), miscellaneous bugfixes (1, 2, 3, 4, 5, 6, 7, 8), and some design-level work on shortening & choosing counterexample traces (1, 2).
  • Finn Hackett found an issue with TLC where reading non-ASCII strings from disk causes a crash; a fix is pending review.

Finally, things I worked on over the past month-and-a-half - all funded by the TLA⁺ Foundation:

  • I adapted the TLA⁺ syntax test corpus for use on TLAPM, which implements its own TLA⁺ parser in OCaml. These found a number of issues in the parser, and also resulted in me writing around fifty additional syntax tests which were backported to the TLA⁺ Java-based tools and the tree-sitter-tlaplus grammar.
  • I investigated transitioning TLAPM’s parser to use SANY, the Java-based TLA⁺ tools’ parser. SANY has an XML parse tree exporter which would avoid any FFI weirdness between OCaml and Java code. I submitted some fixes (1, 2, 3) to dust off the XML exporter and wrote a prototype consumer in OCaml for the XML output. After poking at the prospect of translating SANY’s parse tree output to TLAPM’s internal parse tree format for a couple of weeks, I’m thinking the project has a fairly high risk of dragging on without any intermediate milestones to lock in value. It remains to be seen whether the TLA⁺ Foundation will commit to it. I think there are some work possibilities that could smooth the way, for example by developing a large corpus of tests for SANY’s semantic- and level-checkers to build familiarity with their workings.
  • I played at stepping into the TLAPM maintainer role, just making changes to the development infrastructure like fixing a flaky CI build, adding developer documentation, hunting for ways to cut down the release size, and - most substantially - setting up rolling pre-releases for TLAPM! TLAPM hasn’t seen an official numbered release for a couple of years now, so most people seem to build it from source to get the latest changes; this work just makes the built artifacts from the head of the main branch easily available for download.
  • I submitted a few one-off bugfixes and enhancements for the Java-based TLA⁺ tools: some tests and fixes for the level-checker, and the removal of a now-unused error logging path in the parser.
  • I wrote up a proposal for additional TLA⁺ standardization that has been rolling around my head for a bit, on standardizing human-readable error codes similar to Rust and C# and many other languages. I think the benefits would be wonderful, especially with regard to stimulating test coverage off the happy path.

Newbie Corner

Quite a bit of stuff going on in TLA⁺ development! Don’t be intimidated though, there is plenty of room and desire for newcomers. Join the mailing list and monthly community meeting to introduce yourself if you’d like to join in!

Here I will highlight one issue each month that I think would be good for new contributors. This month it’s the inability of the TLA⁺ parser to handle backticks in strings. The primary reason this is a good first issue is that the required change seems very localized and tremendously unlikely to introduce any bugs; the second reason is that it’s in a very well-tested part of the codebase (the syntax parser), which has the standard TLA⁺ syntax test corpus levied against it - a corpus you will contribute to as part of the fix! I hope to see somebody pick this up in December!