CompCert is a formally verified optimizing compiler for a large subset of the C99 programming language (known as Clight) which currently targets PowerPC, ARM, RISC-V, x86 and x86-64[3] architectures.

[4] This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA.

It aims to be used for programming embedded systems requiring reliability.

[5] Since 2015, AbsInt offers commercial licenses,[6] provides support and maintenance, and contributes to the advancement of the tool.

[2] For the development of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness, Xavier Leroy and the development team of CompCert received the 2021 ACM Software System Award.