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…