Workshop details

Building large, complex software systems is hard. While software engineering has made significant strides in 
the areas of programming and operating systems in production, the tools and techniques available for the 
design stage of development have yet to mature. Traditional methods, such as whiteboard sketches and 
design documents combined with manual reviews, usually fail to identify and prevent design errors, leading to 
hard-to-detect and costly to-correct bugs downstream during the implementation and operation phases.

The TLA+ specification language offers a solution to this problem by providing a rigorous and formal method 
for specifying and reasoning about the behavior of complex systems, such as concurrent and distributed 
ones, before their actual implementation. This allows for early identification and correction of errors, 
leading to a more efficient and effective development process. TLA+ is also an excellent prototyping tool, 
making developers more agile while producing a more robust final product.

TLA+ has been successfully applied in a wide range of companies, from industry leaders like Amazon and 
Microsoft to smaller organizations, and across various projects, including planetary-scale storage systems,
 state machine replication protocols, and hardware architecture. By utilizing TLA+ in the design phase,
 software teams greatly improve the quality and reliability of their software systems.

Designing Complex Systems with TLA+ is a two-day, instructor-led course focusing on the practical 
application of TLA+ in the design of concurrent and distributed systems. This workshop is designed for 
professional software engineer craftsmen working on concurrent and distributed systems who want to add the 
TLA+ specification language and rigorous formal methods to their software engineering toolbelt.

Throughout the course, participants will learn TLA+ and how to apply it to modeling non-trivial systems in a 
hands-on workshop emphasizing practical application rather than just learning the language with toy 
examples. By the end of the workshop, participants will have written a real-world specification and checked 
safety and liveness properties. In short, the course provides a comprehensive introduction to TLA+ and fast-
tracks participants on their path to TLA+ mastery.

### Prerequisites

The detailed agenda for the course can be found at  https://github.com/tlaplus-workshops/ewd998/issues/1. 
Additionally, all workshop materials are available at https://github.com/tlaplus-workshops/ewd998/. To 
prepare for the workshop, we recommend watching Lamport's introductory video 
(https://lamport.azurewebsites.net/tla/tla.html). For the workshop to run smoothly, we will use a browser-
based TLA+ IDE. Thus, Participants must have a GitHub account. Prior formal methods or TLA+ exposure 
obviously helps, but it is not a prerequisite.

### Endorsements

"TLA+ is an indispensable tool for any engineer designing a distributed system/cloud service. At 
Microsoft, we have used it extensively in building services like the Cosmos DB (a globally distributed 
database) and Singularity (a cloud-scale AI scheduling system) and have found it extremely useful to catch 
design bugs upfront. Markus Kuppe is great at explaining TLA+ and its applications in designing real-
world systems." Dharma Shukla (Technical Fellow)

"TLA+ is a language with a set of tools for modeling programs and systems. It can help simplify their design
 and can catch bugs before any code is written. TLA+ is especially useful for building concurrent and 
distributed systems. Markus Kuppe understands and is very good at explaining TLA+ and how it is used in 
industry." Leslie Lamport (Turing Award Winner & TLA+ creator)

### Testimonies

"No competition the best training I have taken since joining Microsoft!"
"I know a few other folks [that] are signed up for later sessions. They're in for a treat!"
"How you teach it is fantastic [...]! Love the [...] interactive teaching!"
"...I was amused that word of how good your workshop was already reached my friend doing formal verification
 at IST Austria..."

### Instructor

Markus Kuppe is a seasoned TLA+ expert and a member of the TLA+ project team for over a decade, during which 
he became the top contributor to the TLA+ tools. Markus has spent the last eight years as a Principal Software 
Engineer at Microsoft Research. He has extensive experience teaching TLA+, having taught more than two 
dozen TLA+ classes. Markus has also published papers on TLA+ and holds a master's degree in computer science 
from the University of Hamburg, which he completed with honors under the guidance of Leslie Lamport. Markus is 
among the world's best TLA+ experts and has given many talks on TLA+ both in academic settings and at industry 
venues worldwide. He is the perfect instructor for anyone looking to learn about TLA+ and its applications 
in concurrent and distributed systems.

### Links:

Use of Formal Methods at Amazon Web Services: https://lamport.azurewebsites.net/tla/formal-methods-
amazon.pdf
TLA+: Viewed from 40,000 Feet and Ground Level: 
https://www.youtube.com/watch?v=Ocxczi-CvRQ
Let's shift-shift left: How modeling can help software 
engineering: https://www.youtube.com/watch?v=yJdY-RNlpuE