CompCert is a C compiler mathematically verified for correctness. It was sole survivor of Regehr et al’s Csmith testing which found no implementation bugs in it. There were two, specification errors. Full verification is hard enough that verified compilers use few optimizations. Regehr’s proposal is interesting as it’s sort of a cheat to get a lot more optimization in the middle end combining superoptimization and equivalence checks. Also, people might find that topic and its inventor (esp Synthesis OS) interesting in and of itself. I like adding bonus material to my submissions for readers to blow their mind a few times. :)
https://en.wikipedia.org/wiki/Superoptimization
https://courses.cs.washington.edu/courses/cse501/15sp/papers/massalin.pdf