AFAK Intel used to have some kind of formal verification, either Haskell or OCaml based for their chips, but I am not having much luck with my Google-fu.