If my understanding of model checking is correct (which I believe is the primary method of formal verification) I don't think this would help much in the case of Heartbleed. The Heartbleed error had to do with an expression being in the wrong scope if I recall correctly. (I think someone forgot to put brackets around an if statement that contained two expressions).

In this case the model would be correct, but the implementation would be wrong. So I don't think formal verification would be of much help. That said, I think there are a number of static analysis tools that would pick up on the error, so a combination of approaches would work.

And of course, it would be great if we could verify that our security critical code was sound in theory, even if we can't necessarily verify that our implementation is free of coding errors, so I agree with your main argument. Of course, whether we're at the point where doing this verification is feasible in practice is another matter unto itself.