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.