Certified compiler and optimizations in Coq/Agda
this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification.  some of this technology is apparently utilized in the CompCert C compiler.

A structured approach to proving compiler
optimizations based on dataflow analysis

it considers the correctness of two optimizations, constant propagation (CP) and common subexpression elimination (CSE), section 4. these optimizations are more advanced than those that are associated with the non Coq-based compiler(s) for the same language. see eg this benchmark chart compared to gcc. (the Coq-based compiler is presumably slower to compile although this is rarely mentioned!) 


  An original aspect of ConCert is that most of the compiler is written directly
  in the Coq specification language, in a purely functional style. The executable
  compiler is obtained by automatic extraction of Caml code from this specification.


however at the end of the paper they do note that there are some compiler optimizations in real compilers that cant be modelled in their framework.

improved optimization is not the only element of consideration here, another aspect is that compiler optimization logic can be subject to subtle defects esp due to its complex nature. over the years gcc has been found to have bugs in its numerous optimization logic routines. eg gcc bug?