Our experiments with Lean and formal verification continue to bear fruit. To further our knowhow and experience, we set out to see if we could apply Lean's strengths to a more advanced topic: compiler optimizations. Traditional verified compilers focus on semantic preservation of already-written C code, limiting their