The advantage of TDD lies largely in the practice of ensuring you have code coverage: that you are regularly exploring all the code paths you aim to deliver. It

The advantage of TDD lies largely in the practice of ensuring you have code coverage: that you are regularly exploring all the code paths you aim to deliver. It's not about modeling the states. A formal specification could do the same thing. In fact, the code is itself a formal specification of exactly that. If you start thinking of TDD as specifying what the code should do, then you probably should be writing tests for your tests to ensure they test what you mean for them to test. And if your code is compartmentalized into small enough components, it is just as easy to write a correct test as it is to write correct code. If you are doing that, then writing tests is clearly a waste of time. (And you should be doing as much of that as possible.)