How Amazon web services uses formal methods
Newcombe, Chris, Rath, Tim, Zhang, Fan, Munteanu, Bogdan, Brooker, Marc, Deardeuff, Michael·2015·Communications of the ACM
DOI 10.1145/2699417
Abstract
Engineers use TLA+ to prevent serious but subtle bugs from reaching production.