alt Hacker NewsNo? That's the whole point of formal verification?
You can even kind of retrofit this to C. The classic example is "sel4". You just need a set of proofs that the code doesn't trigger UB. This ends up being much larger and more complicated than the C itself.
You can fail to verify something which you actually wanted to verify (i.e you made a proof of something else instead of the thing that mattered). See WPA2 KRACK as an example.