In this talk, we introduce the `smt` dialect, a dialect to represent semantics in MLIR using SMT. We provide formal semantics to dialects such as `arith`, `index`, `comb`, or `scf`, directly as a lowering to the `smt` dialect. Additionally, we present multiple tools using the SMT dialect that can be extended with custom dialects and semantics. In particular, we present a translation-validation tool for MLIR, to check the correctness of the compilation of a given program. We also present a tool that automatically checks the correctness of a PDL program (extended to work with analysis passes), by lowering a PDL program to the `smt` dialect. Finally, we provide extra support for handling analysis passes with the use of an `analysis` dialect. This dialect allows users to write dataflow analysis passes as MLIR programs, and then verify both the correctness and the optimality of the analysis using the `smt` dialect, as well as generating the C++ code that can be used by the dataflow analysis framework.