This article inspired me to try TLA+ and adopt it for use in my distributed systems class.
Here are two posts I discussed this process:
The non-mobile link was much more useful for me: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext
Leslie Lamport’s “Who Builds a House without Drawing Blueprints?” http://cacm.acm.org/magazines/2015/4/184705-who-builds-a-house-without-drawing-blueprints/fulltext is something of a companion to this. I don’t like Lamport’s chosen analogy, but agree with his overall point.
One interesting thing about Lamport’s approach (and the TLA+ approach) is the simple mathematical basis. By choosing set theory and predicate logic, I think he’s made a tool that’s easier to approach theoretically than those based on other formalisms (like Pi calculus and type theory). That’s both a strength and weakness, so it will be interesting to see how this evolves in the future.