No, that does not follow, it is actually a common logical flaw. What you can prove with formal verification is that the code conforms to the sacro-saint spec.

No, that does not follow, it is actually a common logical flaw. What you can prove with formal verification is that the code conforms to the sacro-saint spec. But who says the spec is bug-free?