CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing C compiler.
Indeed, some optimizations of ``\texttt{gcc~-O1}'' such as \emph{Lazy Code Motion} (LCM) or \emph{Strength Reduction} (SR) were still missing: developing these efficient optimizations together with their formal proofs remained a challenge.

Cyril Six et al. have developed efficient formally verified translation validators for certifying the results of superblock schedulers and peephole optimizations. We revisit and generalize their approach into a framework (integrated into CompCert) able to validate many more optimizations: an enhanced superblock scheduler, but also \emph{Dead Code Elimination} (DCE), \emph{Constant Propagation} (CP), and more noticeably, LCM and SR. In contrast to other approaches to translation validation, we co-design our untrusted optimizations and their validators. Our optimizations provide hints, in the forms of \emph{invariants} or \emph{CFG morphisms}, that help keep the formally verified validators both simple and efficient. Such designs seem applicable beyond CompCert.