My review and experience of using TLA+ in distributed systems class are in the below posts:
<a href="http://muratbuffalo.blogspot.com/2014/08/using-tla-for-teaching-distributed.html" rel="nofollow">http://muratbuffalo.blogspot.com/2014/08/using-tla-for-teach...</a> <a href="http://muratbuffalo.blogspot.com/2015/01/my-experience-with-using-tla-in.html" rel="nofollow">http://muratbuffalo.blogspot.com/2015/01/my-experience-with-...</a>
"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 <i>all engineers are familiar</i>."<p>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.