For those interested, here’s the publications list of the group behind KLEE:
They do a lot of great stuff. The equivalence check they built for it might have promise in detecting compiler errors. Make a simpler solution for newer languages or compilers than the formal verification done in projects such as VeLLVM. Make an obviously correct translation, optimize it, check, and repeat.