Crellvm: verifying LLVM optimisations with Coq: https://sf.snu.ac.kr/crellvm/ Impressively, they find bugs with optimisation passes which showed no bugs with fuzz testing!