Formal Verification: The Gap Between Perfect Code and Reality
This is an excellent blog post.<p>If you believe a proof of correctness produced by a formal verification tool, I have a bridge to sell you.<p>For a proof of correctness, you need to model the environment, and write a specification or a golden model. These are just as prone to bugs as the system you are trying to verify (even assuming the tools are correct).<p>That is not to say formal verification is useless. Developing a proof will force you to formalize your intuitive grasp of the system and its interfaces. Counterexamples produced by the tools will often help to find deep bugs that would be almost impossible to find any other way. And after many iterations of debugging both the system and the proof, you might gain a lot of confidence in the proof and the system.<p>But even after all of that, trusting a formal proof as a guarantee of correctness is insane.