2011年からAmazon Web Service（AWS）の技術者は形式仕様記述とモデル検査を利用しています。AWSの1つであるクラウドストレージサービスAWS S3は2006年から提供されていますが、データを保護するために、複製、並列制御、オートスケール、ロードバランシング等、様々な分散アルゴリズムを採用しており、バグの存在しないシステム構築は困難でした。さらに、無停止で次々に拡張していく必要があり、安全な変更であることを検証することも難題でした。
この難題を克服するために、AWSの技術者は様々な技術を検討していました。その中でも形式手法の存在は知っていましたが、形式手法は導入コストがかかるため、医療システムや航空システムといった安全性が非常に重視されるシステムでなければ投資対効果が得られないと認識していました。しかし、形式手法の一つであるAlloyをChord（分散型データ共有システム）に適用して成功した事例を知り、形式手法の調査を開始しました。
Alloyの多くの特性は好意的に受け入れられるものでしたが、AWSのユースケースを表現するには不十分な点があったため、TLA+（及びその第二言語であるPlusCal）を採用し、はじめにDynamoDBへの適用を行いました。DynamoDBへのTLA+の適用が成功し、引き続いてAWS S3にも適用を行っています。AWS S3では1445行のPlusCalコードを記述し、3つのバグを発見し、多くの最適化を行うことが可能となりました。
TLA+は、簡単な離散数学、集合演算、述語論理に基づく形式仕様記述言語であり、これらは全ての開発者が知っている内容でした。そのため、開発者は2-3週間程度でTLA+を習得しており、TLA+の導入は費用対効果が非常に高い結果となっています。