Academic usage
The lead developer of CompCert is Xavier Leroy with INRIA. Uses for educational, research or evaluation purposes are free of charge.
Source code and documentation for the academic version, including the compiler proofs, can be downloaded from INRIA’s dedicated CompCert site. The source code is also hosted at GitHub.
Note that academic releases use a different numbering scheme from commercial ones, and that the Valex add-on for postpass validation is only available from AbsInt.
Commercial usage
AbsInt offers commercial licenses, provides industrial-strength support and maintenance, and actively contributes to the advancement of CompCert.
To request a free 30-day trial of the latest commercial release 24.04, fill out and sign the Evaluation License Agreement form (PDF) and email or fax it to us.
Training and support
Every commercial trial includes a free interactive Web-based training via WebEx, on a date and time of your own choosing, as well as tech support via email, WebEx, and phone.
Price quote
We offer:
- project licenses, limited to a particular project, department, and number of installations
- temporary licenses, limited to a particular time frame
- the optional Valex add-on
Email us for a quote tailored to your personal requirements.