Compilers are among our most trusted software, yet their passes are still written and reviewed by hand, making miscompilations a recurring reality. Formal tools like Alive help, but they're limited to peephole rewrites and individual compilation, so they can't reason about imperative passes that walk and mutate the IR. We present VeIR, an executable formal model of MLIR in the Lean theorem prover that reimplements MLIR's actual pointer-based data structures (the same Operation/Block/Region design, def-use chains, and matchAndRewrite-style API), letting us prove transformations correct once and for all, while still having similar performance as MLIR.