We already have tools for proving applications and compilations correct. The problem is there's little to no optimization of those applications because optimizations can break correctness. One aspect of research like this is skirting that by throwing all kinds of optimizations at something combined with equivalence checks that ensure the new form is semantically equal to original form that we know was correct.

For example, CompCert compiler will produce correct assembly from a correct, C program. A set of optimizations might be available for the middle passes. Let's say C program gets taken to form I for intermediate. We know I is correct because that's what CompCert does. Applying J = optimize(I) might break it semantically in process of trying to speed it up. J might not equal I in some way. So, strategy is to develop an equivalence check as strong as CompCert to do J = Optimize(I), If Equals(I, J), Then Return J, Else Return I.

An example of a project doing this for real-world stuff is effort to formalize and equivalence-check LLVM's intermediate code:

https://www.cis.upenn.edu/~stevez/vellvm/