<<There is no reason why correctly written code should run slower than buggy code>>
You miss the fact that there is no way to tell apart "correct" from "buggy" code, much less automatically. The best you can hope is to avoid operations that could make bugs become attack vectors.
And yes, as Linus said, every bug is at least a denial of service vulnerability, but let's not dive into that.
PS: please, the "but there's this and that code that has been verified" people save themselves from commenting, as there is no one able to asses that the verification is correct, see Turing, Godel, etc...