A practical example is the Alive theorem prover, which found many bugs in LLVM's instcombine pass (i.e. peephole optimizations) and which we now use to prove the correctness of new transformations.

https://rise4fun.com/Alive https://blog.regehr.org/archives/1170