This script takes IR before and after canonicalization, translates it into llvm IR and converts it to format suitable for Alive2 https://alive2.llvm.org/ce/ This is primarily for arith canonicalizations verification, but technically it can be adapted for any dialect translatable to llvm. Usage `python verify_canon.py canonicalize.mlir -f func1 func2 ...` Example output: https://alive2.llvm.org/ce/z/KhQs4J Initial discussion: https://github.com/llvm/llvm-project/pull/91646#pullrequestreview-2049342826