How Amazon Web Services Uses Formal Methods

Engineers use TLA+ to prevent serious but subtle bugs from reaching production.