As much as that helps, it doesn't yield software, or systems, without faults. The AWS wikipedia page lists a few major outages of AWS[1]. My recollection is that they are generally caused by cascading failures and complex service interrelationships, which are likely much harder to formally prove, if possible.

1: http://en.wikipedia.org/wiki/Amazon_Web_Services#History

that Amazon paper is talking about design/algorithm verification using formal methods. This does NOT verify that the design or algorithm in question is actually implemented correctly and matches the design perfectly.

And as I recall, TLA+ doesn't tie into code generation which doesn't help with the verification process.