TLA+ Community Meeting 2023
Saturday, April 22, 2023
Paris, France


TLA+ at AWS: Past, Present, and Future


Since 2011, engineers at Amazon Web Services (AWS) have used TLA+ for formal specification and model checking to help solve difficult design problems in large complex real-world systems. That TLA+ enables description of both the desired correctness properties of the system (the ‘what’) and the design of the system (the ‘how’) has been advantageous and more than 100 TLA+ models have been created inside Amazon.

In this talk, we will explain how Amazon engineers have worked with TLA+ over the years and discuss the benefits and challenges they have experienced.