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.