You don't need to prove the application correct, you just have to prove the optimisation correct, i.e. that the generated code has the same observable behaviour as the given code, except for its resource usage.

Superoptimisation is an implementation detail, in the same way that existing compiler optimisations, JIT compilers, CPU branch predictors, etc. are optimisation details. The machine will behave according to the code you wrote, whether that code is correct or not.