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

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/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo... [1] https://news.ycombinator.com/item?id=8096185 https://news.ycombinator.com/item?id=8096185