The problem with proofs is that you need to know what to prove, and that is hard. Even formalizing something as seemingly simple as sorting is tough for most programmers. If your formalization of whatever you wanted to implement is wrong, then your proof is worthless -- you have only proved that your program does something other than what it was supposed to do.
It's not that TDD is perfect, but it is a pragmatic approach to reducing bugs and it helps a lot in preventing regressions.
Why are imperfect programs and test suites useful, yet imperfect specifications are worthless?
It's not all black-and-white. Specifications, like test suites, contain many properties. The problems of specifying slightly-wrong behaviour on edge-cases might be more than offset by the security guarantees that are gained.
Also, note that many properties are built on each other and specifications will grow and change along with the software. Incorrect properties are often incompatible, but unlike tests which may never hit the incompatible cases, a verification tool will refuse to accept such incompatibilities.
The article was talking about security. Security errors in specifications can be edge-case-like stuff. Or...
Back in the day, Microsoft very deliberately designed Outlook so that it could execute a file by having the user click on it. That was in the spec. It was also an enormous security hole. It wasn't just an edge case - the security hole was the essence of what the spec required.
If you get a spec like that, formal verification can do to things. It can tell you that yes, your code does what the spec says, without introducing any (additional) security bugs. That's somewhat useful, but it won't save you if the spec itself is the security bug.
Or, formal verification might be able to tell you that the spec itself is a security problem. That might not be called "verification", though - it might be called "theorem proving" or some such. It's in the same neighborhood, though.
Writing a specification for sorting sounds a lot easier than actually writing a sorting algorithm. Though admittedly I have never used a programming language where I could try to encode this property in a type.
It's not that TDD is perfect, but it is a pragmatic approach to reducing bugs and it helps a lot in preventing regressions.