How Amazon Web Services Uses Formal Methods
https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/
Method
"Since 2011, engineers at Amazon Web Services (AWS) have used formal specification and model checking to help solve difficult design problems in critical systems."
Population
"At the time of this writing, Amazon engineers have used TLA+ on 10 large complex real-world systems."
What it does not show
No counterfactual: no comparison against similar AWS systems built without TLA+, so it cannot isolate incidents prevented — only bugs caught before shipping. Does not quantify the engineer-hours cost of writing and maintaining specifications, or any false-negative rate. Self-reported by the practitioners who built the tooling.
Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff
Model checking found subtle concurrency and fault-tolerance defects in production distributed systems that had already passed design review, code review and testing — including a DynamoDB data-loss bug whose shortest counterexample was 35 steps. Engineers were reported productive in TLA+ within two to three weeks.
Tier III: Single-org engineering report across named production systems with counted bugs found; no control group of comparable systems built without TLA+.