I'm reasonably sure that for all things where a proof would be helpful, that is properties that the programmer has a nontrivial chance of getting the implementation wrong and not catching the mistake with a test, a correctness proof is a lot harder than writing a correct implementation. I've dabbled a bit with Coq and Isabelle and certainly found this to be the case.

Stronger type systems help a lot with common security problems. Memory safety and a system to express taint of inputs eliminate a huge class of potential problems. They are still very, very far from correctness proofs that could catch actual logic bugs.