⚠️ Warning: this is an experimental fork. It extends CompCert 3.17 with a-leanbackend forclightgenand a Lean 4 formalization of Clight. This work is under active development and is not part of the official CompCert distribution.
The formally-verified C compiler.
The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors.
The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.
For more information on CompCert (supported platforms, supported C features, installation instructions, using the compiler, etc), please refer to the Web site and especially the user's manual.
This fork adds a -lean backend to clightgen (see the export/ directory).
It exports a C program's Clight abstract syntax as Lean 4, and comes with a
Lean 4 port of the Clight operational semantics, an executable interpreter, and a separation-logic program logic for proving
properties of the exported C code.
This work is experimental and under active development: interfaces,
file layout and proof libraries may change without notice. See
export/LEAN.md for a full description.
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
A commercial version of CompCert, without this restriction and with
professional support and extra features, can be purchased from
AbsInt. See the file LICENSE for more
information.
The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH.
General discussions on CompCert take place on the compcert-users@inria.fr mailing list.
For inquiries on the commercial version of CompCert, please contact info@absint.com