I mean ... The thing about formal verification is that you can write the extremely slow but correct version of your code and then have an optimizer write a much more efficient version with a proof of correctness.

For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.

If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.

Most software is ultimately like this