TLA+ Conf 2022
Thursday, September 22, 2022
St. Louis, MO, USA

A decade of TLA+ at AWS

Marc Brooker


Service teams at AWS have been using TLA+ for over a decade. In 2015, we wrote in Communications of the ACM about our experiences with TLA+ on S3, DynamoDB, and others. Since then, our use of formal methods has expanded substantially, with TLA+ playing a large, but increasingly niche, role. In this talk I’ll cover how we’re using TLA+ today, some of the ways our use of formal methods has evolved, and what we see as the challenges for the future. I’ll end with a call to action, describing the tools I think distributed systems designers need, but don’t yet have.