CompCert est un compilateur pour un large sous-ensemble du langage C qui génère du code pour plusieurs architectures de processeurs. Il est unique car il a été formellement vérifié à l'aide de l'assistant de preuve Coq, garantissant ainsi le comportement du code assembleur généré par rapport aux semantiques du code source C.