SYSTEMS CORRECTNESS PRACTICES AT AMAZON WEB SERVICES

Summary from the TLDR newsletter

AWS strives to deliver reliable services that customers can trust completely, which requires maintaining the highest standards of security durability, integrity, and availability. Systems correctness serves as the cornerstone for achieving these priorities. This article looks at the formal methods used across AWS to deliver complex services with high confidence in correctness. It covers more traditional formal approaches such as theorem proving, deductive verification, and model checking, as well as more lightweight semi-formal approaches such as property-based testing, fuzzing, and runtime monitoring.