I was interested in a first project for getting familiar with TLA+, “a high-level language for modelling programs and systems.” TLA+ has been used to find errors in the design of real-world distributed