Keep in mind, these things are only proven to work as specified. There is no guarantee that the specification itself is secure. Or that there is no side channel attack possible. Or other stuff.
Correct. But what it achieves is a massive compression in the size of the attack surface. In as much as you trust the proof system, you know that the code matches the specification, so the only bugs which can exist are those in the specification itself.
Keep in mind, these things are only proven to work as specified. There is no guarantee that the specification itself is secure. Or that there is no side channel attack possible. Or other stuff.
Correct. But what it achieves is a massive compression in the size of the attack surface. In as much as you trust the proof system, you know that the code matches the specification, so the only bugs which can exist are those in the specification itself.