Especially see the CompCert section on page 6 of the Csmith PDF to see what a difference formal verification made. Note that compilers don&#x27;t have to go that far: typed, functional, thoroughly-tested code in something like Ocaml or Haskell can achieve 80-90% of that quality with relatively little effort. Hence, why I promote rewriting and further extending things like LLVM in languages like ML, Ada, or Eiffel that support advanced checks.