I wouldn't say "a massive waste of time" - except if done at the wrong level. I like Chris Newcorde's view [1] that TLA+ is "a pseudocode for writing design doc

I wouldn't say "a massive waste of time" - except if done at the wrong level. I like Chris Newcorde's view [1] that TLA+ is "a pseudocode for writing design documentation". At that level, it's completely appropriate to use formal methods to check that you specified/investigated/considered all the edge cases. However, I find that using it to "prove program correctness" is indeed a waste of time, since what is most often wrong is your assumptions, not necessarily your implementation. [1]http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf