Wadler's Blog: How Amazon Web Services Uses Formal MethodsHow Amazon Web Services Uses Formal Methods by Newcombe et al, appeared in Communications of the ACM in April 2015. It describes the use of Leslie Lamport's TLA+ (Temporal Logic of Actions) to refine the design of web services such as Dynamo DB and S3. (S3 stored 2 billion objects and handled 1.1 million transaction per second back in 2013.) Thanks to Jessica Kerr for pointing me to this paper aft
