Learn how to use TLA+ to study, design and specify your algorithms. This workshop is designed to teach you about TLA+ from the ground up. We will start with simple distributed algorithms and slowly move toward more complex ones. Knowledge you gain can be immediatly applied at work next day after the workshop
TLA+ is a formal specification language developed by Leslie Lamport, designed to specify, model, document, and verify concurrent systems. It empowers your ability to clearly specify your design choices in the form of a formal specification, but also (even more importantly) can formally verify that your design choice is correct—meaning that it is both safe (does not break any rules) and live (over time it converges toward the result).
This workshop is designed to teach you about TLA+ from the ground up. We will start with simple distributed algorithms and slowly move toward more complex ones. In each section, a bit of TLA+ notation will be introduced, followed by the description of the algorithm that we will specify. Lastly, we will run the model checker to look for potential errors in our design. Each section will end with an exercise. This will be an intensive six hours, but at the end of the day it will be hard not to notice that your core engineering skills got a lot better.
We will use well known distributed algorithms as examples (such as Two Phase Commit or Paxos), but the knowledge you gain can be applied to any of your daily routines. The objective of this workshop is to equip attendees with powerful tools that will allow them to better design their systems and have stronger guarantees it will be correct. Lastly, working with TLA+ will also allow you to think more abstractly about your system—and that is a value of its own.