AMO-Lean: Towards Formally Verified Optimization via Equality Saturation in Lean 4 (opens in new tab)

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 ability to