Amazon AWS（亚马逊云服务平台）自2011年以来就一直在使用TLA+做系统设计的形式验证。2015年4月，亚马逊六位工程师发表了一篇文章，描述了如何将其引入AWS，以及如何在AWS中使用。他们在文章中指出：“形式化方法在系统设计中发现了我们所知道的任何其他技术都找不到的缺陷。形式化方法对于主流的软件开发来说是出人意料的可行的，并且能带来良好的投资回报。在亚马逊，形式化方法通常被应用于复杂的现实软件的设计，包括公共云服务。”

早在2015年时，亚马逊在10个大型系统和7个team使用TLA+验证，包括senior manager和技术leader，包括S3云存储系统、NoSQL云数据库、EBS弹性块存储

分布式锁管理系统等。AWS security team 2017年形式验证投入增加76%，上线前发现security问题增加45%