For inquiries about Compcert, please contact the project leader or the industrial partner AbsInt.


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, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan.

The following scientists contributed ideas, code, or feedback: Andrew Appel, Ricardo Bedin França, Lennart Beringer, Frédéric Besson, Sylvie Boldo, Timothy Bourke, Yves Bertot, Christoph Cullmann, Rob Dockins, Damien Doligez, Denis Favre-Felix, Benjamin Grégoire, Robbert Krebbers, Guillaume Melquiond, Thomas Moniot, Prashanth Mundkur, 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 an industrial-strength version of CompCert with more features, technical support, and unlimited licensing. AbsInt participates in the development and evolution of CompCert.


The CompCert project has been supported by the following grants:

Related projects