Please, step away from "formal verification" and come back to world the rest of us devs work in. I have never seen a formally verified piece of software even once.

I don't know if its too hard to do to real software or if C doesn't allow for it, or if it is just too expensive. The simple matter is that is not an option for the vast majority of projects. Unless you can make it practical, I assert it has no place in a practical discussion about preventing software issues.

Worse: "It's amazing how many bugs there can be in a formally verified piece of software." I forget who said it, but it's been a long time. (Maybe in connection with formal verification of an OS? Does anyone remember?)

Formal verification only works if the formal verification was mistake-free. (And how are you going to prove that? With a formal verification? It's turtles all the way down...) Also, it only works for the aspects that were formally verified. Heartbleed, for example, could be regarded as a flaw in the specification; formally verifying that the code matches the spec won't save you from that.