Overview

CompCert is a formally verified compiler for the C programming language. According to published sources, the compiler is provided by INRIA, is specified, programmed, and proved in the Coq theorem prover, and at the time of writing targets the Power, ARM, and 32-bit x86 architectures. CompCert is intended for embedded systems requiring high reliability: the generated assembly code is formally proved to behave exactly like the source C program with respect to a formally defined operational semantics of the language.

Programming language subset and semantics

CompCert does not accept the full ISO C 99 language. It compiles a subset of C whose semantics are unambiguous; in particular, it rejects programs that contain constructions with unspecified behavior as defined by the ISO C 99 standard. The subset accepted by CompCert is described in one cited source as being even larger than the subset of C accepted in the SEL4 microkernel verification.

The execution of C programs in CompCert, or more precisely programs in the subset of C considered by the project, is defined using operational semantics. This operational-semantics approach is convenient for proving compiler correctness because the same style can be applied to source and target languages and to intermediate languages.

Reuse of CompCert components in other verification efforts

The operational semantics of C provided by CompCert and its Coq libraries are not only used to reason about compiled C code but are also reused as building blocks in other formally verified systems.

Instruction-set simulation (SimSoC, ARM v6)

In work on verifying the ARM v6 instruction-set simulator (ISS) of SimSoC, three parts of CompCert are used:

1. The correct machine code generated by the C compiler, used to actually run simulations.
2. The operational semantics of C in Coq, which provides a formal model of the simulator program derived from its C source.
3. The CompCert Coq library for words, half-words, bytes, and bitwise operations. These low-level functions are used to describe the instruction-set model and can be re-used safely because they are already proved inside CompCert.

The verification proceeds by relating, via a projection, a "concrete state" represented by C data structures in the simulator to an "abstract state" representing the formal ARM model in Coq, and by proving that executing the same instruction on both sides yields a new pair of equivalent states. CompCert also provides formalized properties of built-in external functions (e.g., memset, memcpy) used by the simulator, enabling reasoning about their potential side effects. A benefit cited in this work is that CompCert C itself is coded in Coq, so formal models and proofs can be developed in the same logical framework rather than translating semantics between systems.

Space-grade microcontrollers (MORAL / PEAKTOP)

In the MORAL H2020 project, AbsInt and partners developed a rad-hard microcontroller based on the novel PEAKTOP architecture with an open Instruction Set Architecture (ISA). One stated objective of the project is a formally verified C compiler, RTOS, and toolchain for this microcontroller. CompCert is presented as an example of such a formally verified C compiler in this context.

Verification limits and certification testing

The use of CompCert does not eliminate all testing. In a discussion of higher-assurance certification for verified systems, the authors note that even when the transition from C programs to a processor model has been completely covered by deductive verification methods, as in CompCert, certification bodies still require test sets that check whether the underlying processor model conforms to real hardware. This observation motivates model-based generation of test programs from a formal processor model rather than relying only on manually developed certification kits.

Provenance and availability

The CompCert source code is publicly available. The official repository is hosted on GitHub by AbsInt under the name AbsInt/CompCert, described as "The CompCert formally-verified C compiler," and is primarily written in the Rocq Prover (formerly Coq) language.

Relationship to other tools and projects

• Coq / Rocq Prover: CompCert is specified, programmed, and proved in Coq; its components are reused inside Coq developments such as the verified SimSoC ARM v6 ISS.
• SimSoC: an open-source full-system SoC simulator whose ARM v6 ISS has been verified against a Coq ARM model using CompCert's C semantics and libraries.
• sel4: a formally verified operating-system kernel whose C subset is compared in the literature with the C subset accepted by CompCert.
• CerCo: a project that uses operational semantics for C and compiler-correctness techniques in the style of CompCert.
• PEAKTOP / MORAL: a rad-hard European microcontroller project that targets a formally verified C compiler, with CompCert cited as an example of such a compiler.