Les compilateurs peuvent dégrader certaines garanties en apportant des optimisations sur l'exécutable. CompCert d'AbsInt apporte ces garanties de compilation de code C tout en optimisant les performances d'exécution. Indispensable pour la validation, la vérification et la certification de logiciels embarqués critiques qui doivent satisfaire aux exigences de sureté de fonctionnement et de cybersécurité tels que les DO178B/C, ISO 26262, IEC 61508, EN 50128 ou ISO 21434.