Formal correctness proofs – much like another of Dijkstra's bugaboos, static type systems – are a substantial amount of effort to use. Formal correctness proofs are so difficult to use that I'm not aware of any research project to validate their effectiveness, but static type systems are the closest thing we have in the field of software industry to provably worthless.
(To be fair, my favorite bugaboo, test-driven development, also has relatively weak empirical support for its benefits. But of course in the case of the thing that I like, the study was flawed and in the case of the thing that I don't like, one study is definitive.)