Alive2 is a translation validation tool: given two versions of a function in LLVM IR–usually these correspond to some code before and after an optimization has been performed on it–Alive2 tries to either prove that the optimization was correct, or prove that it was incorrect. Alive2 is used in practice by compiler engineers: more than 600 LLVM issues link to our online Alive2 instance.
— John Regehr & Vsevolod Livinskii
Really interesting read on how Alive2 is used alongside the Minotaur superoptimizer and llvm-mca.