CompCert es un compilador optimizador verificado formalmente para un gran subconjunto del lenguaje de programación C99 (conocido como Clight) que actualmente apunta a las arquitecturas PowerPC , ARM , RISC-V , x86 y x86-64 [3] . [4] Este proyecto, dirigido por Xavier Leroy , comenzó oficialmente en 2005, financiado por los institutos franceses ANR e INRIA . El compilador está especificado, programado y probado en Coq . Su objetivo es ser utilizado para la programación de sistemas integrados que requieren fiabilidad . El rendimiento de su código generado es a menudo cercano al de GCC (versión 3) en el nivel de optimización -O1, y siempre mejor que el de GCC sin optimizaciones. [5]
Desde 2015, AbsInt ofrece licencias comerciales, [6] brinda soporte y mantenimiento, y contribuye al avance de la herramienta. CompCert se publica bajo una licencia no comercial y, por lo tanto, no es software libre , aunque algunos de sus archivos fuente tienen doble licencia con la Licencia Pública General Reducida de GNU versión 2.1 o posterior o están disponibles bajo los términos de otras licencias. [2]
Por el desarrollo de CompCert, el primer compilador optimizador prácticamente útil dirigido a múltiples arquitecturas comerciales que tiene una prueba completa y verificada mecánicamente de su corrección, Xavier Leroy y el equipo de desarrollo de CompCert recibieron el premio ACM Software System Award 2021 .