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.
- 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.