Well, not quite, because there are parts of CompCert that are not proven [1]: - Parsing, type-checking, and pre-simplifications - Assembling and linking And

Well, not quite, because there are parts of CompCert that are not proven [1]: - Parsing, type-checking, and pre-simplifications - Assembling and linking And there have been bugs on edge cases there. Moreover, correctness is limited to what is specified. COQ does not guarantee that there are no missing specifications or theorems. The C standard is written in English, people had to manually encode the standard in COQ. [1] http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html