[agentultra]

If what you're saying is that TDD can guide you to a good design but it doesn't guarantee it then I think we're in agreement there.

When working on protocol specifications and proving the correctness of a certain invariant or property of the system I find TDD to be lacking and tend to turn to formal methods for results.

However at the module/interface level of an individual software library or component TDD is a very good tool that helps guide me towards a good design. As do other tools like a sound type system. When they work in concert the system almost writes itself -- I just have to come up with the queries, invariants, and assertions.