Tla Plus

How Amazon Web Services Uses Formal Methods

Newcombe et al. (CACM 2015) describe how Amazon Web Services engineers use TLA+ to specify and verify distributed systems protocols, finding real bugs in S3, DynamoDB, and EBS before deployment. One of the few industrial accounts of formal methods working in production at scale.