My review and experience of using TLA+ in distributed systems class are in the below posts: http://muratbuffalo.blogspot.com/2014/08/using-tla-for-teach... http://muratbuffalo.blogspot.com/2015/01/my-experience-with-...

"We found what we were looking for in TLA+,11 a formal specification language based on simple discrete math, or basic set theory and predicates, with which all engineers are familiar."

Somehow I get the sense that this is an extremely optimistic view of our profession. Even when you look at only those engineers hired by Amazon.