> 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!