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

Organization & user updates

• The program for the TLA⁺ Community Event 2025 has now been announced! It will be co-located with ETAPS 2025 in Hamilton, Ontario, Canada on May 4th, 2025. Hope to see 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.
• TLA⁺ Foundation patron Amazon has appointed a new representative to the TLA⁺ Foundation board! Ankush Desai is a Principal Applied Scientist at AWS and one of the original developers of the P formal specification language. He recently co-authored a paper on formal methods use in AWS and delivered a talk on the same topic. TLA⁺ is sure to benefit from his advice and experience!

Community TLA⁺ tooling updates

Work done by community members on non-TLA⁺ Foundation-managed projects:

• Dom Dwyer worked extensively on his new Rust-based TLA⁺ formatter tool.
• William Schultz worked on his web-based spectacle TLA⁺ interpreter, adding an animated Raft example and making many tweaks to the UI.
• Ioannis Filippidis released a new TLA⁺ syntax parser, written in Python. The source code can be obtained by downloading & extracting the package file.
• Hillel Wayne began development of a set of exercises to help people learn TLA⁺. The exercises are all designed with the aim of automatically verifying attempted solutions.

Core TLA⁺ tooling updates

Work done by community members on TLA⁺ Foundation-managed projects:

• Karolis Petrauskas added another feature to the TLAPM-based TLA⁺ language server, supporting renaming proof steps.
• First-time contributor Krishna Padmasola added validation for the -labelRoot PlusCal command-line parameter, fixing a bug featured in the January 2025 edition of this newsletter.
• Another first-time contributor Bruno Felipe Francisco fixed a longstanding bug in the TLA⁺ VS Code extension, adding support for identifying parameterized constants as possible symbols for autocompletion and other operations.
• Federico Ponzi worked on the TLA⁺ VS Code extension, linking directly to error locations in the code when possible and tweaking the counterexample UI (1, 2).

TLA⁺ Foundation-funded updates

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

• After spending the past few months doing a lot of testing & exploration of the various TLA⁺ parsers, I am writing a guide to distill this knowledge for others. The tutorial series Create your own TLA⁺ tools will teach you how to write TLA⁺ language tooling for a minimal vertical slice of the language (just enough to handle the generalized Die Hard spec, with some inconvenience). The purpose of the guide is to prepare contributors to make serious contributions to the existing TLA⁺ language tools, by writing their own simple prototype and then contrasting it with the existing implementations.
• I attempted (unsuccessfully) to get the Eclipse-based TLA⁺ Toolbox GUI to build using the TLA⁺ tools Maven package, so we can split the Toolbox out into its own repository. If you’re reading this and know anything about the OSGi build process, your help would be greatly appreciated!
• I combined some repos and collected TLA⁺ standards documents into the RFCs repo, to be used as a one-stop shop for the TLA⁺ language standard, conformance test suites, and RFC status tracking.

Newbie Corner

Here we highlight an issue that would be a good choice for new contributors! This time we’re looking at PlusCal, a language which transpiles into TLA⁺. The transpilation process includes logic to insert linebreaks so the output TLA⁺ is readable. Unfortunately, in one case this logic has gone awry and results in invalid TLA⁺ output on long procedure names!

There is an old PR (not merged for some reason or another) which might contain the simple fix necessary. So, the work required is to evaluate the PR change to see whether it indeed fixes the issue, then find a way to write an automated test for it. Try various modifications of the reported failing test case to ensure that close input variants don’t elude your fix. Resubmit the combined changes in your own PR with credit to the original, using the Co-authored-by: git commit message trailer.

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

• March 2025: interpret expressions of the form x' ⊆ S
• February 2025: interpret expressions of the form CHOOSE x : x ∈ S
• December 2024: add parser support for backticks in strings

The following past highlighted issues have now been fixed:

• Highlighted January 2025, fixed April 2025: Krishna Padmasola completed fix the PlusCal CLI -labelRoot option