Writing a formal specification using something like TLA+ is actually very much like writing unit tests. Therefore, many of the same problems apply. The main dif

Writing a formal specification using something like TLA+ is actually very much like writing unit tests. Therefore, many of the same problems apply. The main difference is that you are testing your design, not the implementation. You are trying to work at a much higher level than the actual code. That's why it is most useful for checking concurrency. It is hard for humans to mentally think about all possible interleavings of events, hard for fuzz testing to catch rare interleavings, but very easy for a computer to check all possibilities with breadth-first search. By no means are specifications a complete answer, even making sure your implementation implements the spec is hard. But it is another useful tool in the arsenal.