This tutorial will introduce mechanical reasoning about optimizations on the LLVM intermediate representation using the Alive2 tool, and then will also present some applications of this technique. These applications include hunting for bugs in LLVM optimization passes, performing translation validation during compilation of applications of interest, and synthesizing novel optimizations. The synthesis part of this tutorial will focus on some recent work for discovering SIMD optimizations, and will also discuss the problem of taking a concrete optimization that is produced using program synthesis and generalizing it so that it can be applied more broadly than the context in which it was originally discovered.