Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check.

Sure, extensive formal verification of all software would probably bring some benefit in terms of correctness and perhaps security. But you're not considering the cost involved.

So far, such verification has only proven to be possible in rather limited situations, namely where there are significant resources available, or in academic exercises. Maybe this will change in the future, but in the present it's generally far more cost-effective to use a statically-typed programming language along with some form of automated testing. That gives many of the benefits of more formal methods of verification, but while also avoiding many of the costs, even if the end result doesn't conform to some theoretical idea of "perfection".