We aim to combine the convenience of automation with the versatility of ITPs for verifying peephole rewrites across domain-specific IRs. Our tool (lean-mlir) built in the Lean proof assistant provides: (a) a user-friendly frontend, (b) scaffolding for defining and verifying peephole rewrites, and (c) proof automation for semi-automatically verifying common compiler IR patterns. In this talk, we will showcase our work in bringing an Alive-style workflow for peephole optimizations over an LLVM style IR in Lean. We will sketch out our future vision, with the goal of making formal verification a core part of the day-to-day compiler development workflow. We hope to engage the community into providing formal semantics for many of the more complex IRs in the MLIR ecosystem.