[djb_hackernews]

You may be interested in this[0] paper outlining AWS use of TLA+ to formally prove its systems. Also previous discussion here[1].

[0] http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

[1] https://news.ycombinator.com/item?id=8096185