> If it compiles, it typechecks. If it typechecks, the proof is correct. This is a consequence of the Curry-Howard correspondence

I think this perhaps the most common misconception of how formal verification works. If the program typechecks, then you have a proof that the program (or often a model of the program) implements the specification. However, you still have to make sure that your _specification_ is correct! This is one of the hardest parts of formal verification!

Exactly. It does not mean your formal specification is correct (of the code and what it should do).