CompCert est un compilateur C formellement vérifié, c'est-à-dire qu'il y a une preuve mathématique que le code produit correspond au code source, au sens qu'il produit les mêmes exécutions. Toutefois, il contient des bugs, qui parfois conduisent à générer du code incorrect. Cela peut paraître paradoxal ; nous expliquerons comment cela est possible, et ce que nous avons fait pour rechercher des bugs (ou parfois en trouver un peu par hasard), et ce qu'il faudrait faire pour aller plus loin.