I learnt and used TLA+ while working at msft, and I'm still using it today:

- anytime I have some protocol or state machine whose behaviour isn't obvious, I write a TLA+ spec. - the process of writing it clarifies my understanding and leads to new insights. These insights directly inform the code and the tests. - the model checker makes it very easy to check sophisticated properties of the algorithm.

I don't use it all the time, but it's a tool I'm very happy I invested in.