Systems Correctness Practices at Amazon Web Services. - Brooker, Marc; Desai, Ankush (Communications of the ACM, 2025)
This article provides an overview of the current practices, both formal and semi-formal, employed at Amazon Web Services (AWS) for ensuring system correctness. Topics include the use of the formal specification language TLA+ as well as the incorporation of another language, P, a state-machine-based language at AWS, as well as methods including property-based testing, fault-injection testing and event-based simulation.