Workshop: TLA+ in action

The goal of this workshop is to show developers of concurrent and distributed systems how to model algorithms with TLA+. Inspired by Safra's EWD998, we will design and verify a termination detection algorithm. The focus is on applying TLA+ rather than the TLA+ language itself. In other words, the workshop will follow Lamport's video course style and introduce TLA+ as we go. At the end of the workshop, attendees will have written a specification of EWD998, checked safety and liveness properties, stated fairness constraints, and encountered refinement.

This is a hands-on, interactive workshop for programmers who want to get familiar with TLA+. The format of the workshop will be similar to the talk "Weeks of Debugging Can Save You Hours of TLA+", enriched with hands-on exercises. The material is available in advance at https://github.com/lemmy/ewd998 (please consider starring the repository). Familiarity with logic is not a prerequisite (if you've been using Coq, Isabelle, Lean, ..., this workshop is likely not for you).

For the workshop to run smoothly, we are going to use a browser-based TLA+ IDE. Before starting on Wednesday, please open the GitHub link above and go through the Gitpod login process with your Github account (Gitlab and Bitbucket won't work). Afterward, you will be greeted by the TLA+ IDE with the workshop material open.