We propose a design of a refinement checker for the LLVM compiler infrastructure and several potential applications. The inputs to the checker are two LLVM programs and a symbolically-specified relation between their state spaces, and its output is whether this relation is a proper refinement between the two programs. Where the programs are the input and output of a sequence of optimization passes, the relation can be generated during compilation, thus the checker establishes a translation validation of the compilation.