For inquiries about Compcert, please contact the project leader


Xavier Leroy is the architect and lead developer of the CompCert C verified compiler. The other developers are Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Bernhard Schommer, and Jean-Baptiste Tristan. The following scientists contributed ideas, code, or feedback: Andrew Appel, Ricardo Bedin França, Lennart Beringer, Sylvie Boldo, Yves Bertot, Rob Dockins, Damien Doligez, Denis Favre-Felix, Benjamin Grégoire, Robbert Krebbers, Guillaume Melquiond, Thomas Moniot, Alexandre Pilkiewicz, Tahina Ramananandro, Laurence Rideau, Silvain Rideau, Benoît Robillard, Valentin Robert, Gordon Stewart, Bernard Paul Serpette, Jean Souyris, Joseph Tassarotti, Andrew Tolmach.

Industrial partner

AbsInt Angewandte Informatik GmbH sells commercial licenses and technical support for CompCert, and participates in its development and evolution.


The CompCert project has been supported by the following grants:

Related projects