The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs.

The main result of the project is the CompCert C verified compiler, a high-assurance compiler for almost all of the ISO C90 / ANSI C language, generating efficient code for the PowerPC, ARM and x86 processors. Get CompCert C »

The CompCert project is funded by ANR (grants ANR-05-SSIA-0019, ANR-08-SEGI-021, ANR-11-INSE-003) with additional support from FNRAE and Digiteo. See the list of partners for more information.

Diagram of the CompCert compiler


[09/2014] The working sources for CompCert are now hosted on Github.

[09/2014] CompCert C version 2.4 is released, with a revised handling of single-precision floating-point arithmetic and support for C99 compound literals and switch statements over 64-bit integers.

[06/2014] As part of a licensing agreement with Inria, AbsInt Angewandte Informatik GmbH will market and provide support for the CompCert verified C compiler.

[05/2014] CompCert C version 2.3 is released. Novelties includes a formally-verified parser, and support for C99 designated initializers.

[02/2014] Release of CompCert C version 2.2, featuring more aggressive optimizations, support for more features of ISO C99 (especially variable-argument functions), and improved conformance with the target ABIs.

[10/2013] Minor release of CompCert C version 2.1. The main novelty is support for the _Alignas attribute from ISO C2011, for finer control of alignment.

[06/2013] CompCert C version 2.0 is now available, featuring two major improvements: 1- support for 64-bit integer arithmetic (type long long) and 2- a new register allocator based on a posteriori validation.

[03/2013] Release of version 1.13 of the CompCert C compiler. The semantics of pointers "one past the end of an array" is now properly defined as in the ISO C standard.

[01/2013] CompCert C versions 1.12 and 1.12.1 are released. The two versions are functionally identical, but 1.12 is for Coq 8.3 and 1.12.1 for Coq 8.4.

[12/2012] The Microsoft Research Verified Software Milestone Award was awarded to Xavier Leroy for his work on the CompCert verified compiler.

[07/2012] CompCert C version 1.11 is released. Novelties include a full formalization and proof of floating-point arithmetic, and performance improvements: function inlining, more aggressive constant propagation and CSE.

[06/2012] A technical report describing the memory model used in CompCert versions 1.7 and up.

[03/2012] Release of version 1.10 of the CompCert C compiler. Now with a provably-correct implementation of volatile accesses and by-value structure passing and assignment, plus various small performance improvements, and a user's manual.

[02/2012] Publication: Formally verified optimizing compilation in ACG-based flight control software, with Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Marc Pantel and Jean Souyris, symposium ERTS2 2012.

[11/2011] Release of version 1.9.1 of the Compcert C compiler.

[10/2011] The 2011 La Recherche prize in Information Sciences was awarded to Xavier Leroy, Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan for their work on the CompCert verified C compiler.

[08/2011] Release of version 1.9 of the Compcert C compiler. Novelties include a reference C interpreter and stronger semantic preservation results.

[05/2011] Release of version 1.8.2 of the Compcert C compiler.

[03/2011] Release of version 1.8.1 of the Compcert C compiler. Now compatible with Coq 8.3pl1, and including algorithmic improvements (lower compilation times) and better handling of initialized global variables.

[09/2010] Version 1.8 of the Compcert C compiler is available. It includes a larger subset of C (including side-effects within expressions) as its source language; a new port generating x86-32 bits code; and more precise semantics for volatile accesses.

[03/2010] Release of version 1.7 of the Compcert C compiler, featuring a new C type-checker/elaborator/simplifier and a refined memory model.

[01/2010] Release of version 1.6 of the Compcert C compiler.

[11/2009] Publication: A formally verified compiler back-end. An extensive (80 pages!) description of the back-end part of Compcert, published in Journal of Automated Reasoning 43(4).

[08/2009] Release of version 1.5 of the Compcert C compiler. Now with full support for goto statements!

[07/2009] Publication: Formal verification of a realistic compiler. A short overview of the CompCert verified compiler, published in Communications of the ACM, July 2009, along with a perspective written by Greg Morrisett.

[06/2009] Release of version 1.4.1 of the Compcert C compiler. (This version is functionally identical to version 1.4, but compatible with Coq 8.2-1.)

[04/2009] Release of version 1.4 of the Compcert C compiler.

[01/2009] Publication: Mechanized semantics for the Clight subset of the C language. A description of the Clight source language, published in Journal of Automated Reasoning 43(3).

[08/2008] Release of version 1.3 of the Compcert C compiler.

[03/2008] First public release (version 1.2) of the Compcert C compiler.

[02/2008] Creation of this Web site.