CompCert

Tool

CompCert is a formally verified C compiler developed at INRIA. It is specified, programmed, and proved correct in the Coq interactive theorem prover, and it targets several processor architectures. Beyond being a compiler, its operational semantics for C and its Coq libraries for low-level data representations are reused as foundational components by other formally verified tools and projects, including those targeting instruction-set simulation, hardware verification, and space-grade microcontrollers.

First seen 5/25/2026

Last seen 9/22/2026

Evidence 9 chunks

Wiki v2

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

6 connections

Towards Verified Faithful Simulation ← uses 95% 2e

The paper uses CompCert for formal C semantics and as a certified compiler

formal verification implements → 100% 1e

CompCert is a formally verified compiler.

operational semantics implements → 95% 1e

CompCert uses operational semantics to define C program execution

ISO-C 99 standard uses → 90% 1e

CompCert considers C programs compliant with ISO-C 99 standard

calculus of inductive constructions uses → 85% 1e

CompCert is coded in Coq which uses calculus of inductive constructions

INRIA published by → 95% 1e

CompCert is provided by INRIA

LINKED ENTITIES

2 links

Coq implementation_language Multiple sources state CompCert is specified, programmed, and proved in Coq; its C subset and low-level libraries are coded in Coq.

SimSoC used_by The verified SimSoC ARM v6 ISS relies on CompCert's machine code, C operational semantics, and Coq libraries for words and bitwise operations.

CITATIONS

11 sources

11 citations — click to expand

[1] CompCert is a formally verified C compiler provided by INRIA, specified, programmed, and proved in Coq, currently targeting Power, ARM, and 32-bit x86 architectures. Towards Verified Faithful Simulation

[2] The generated assembly code of CompCert is proved to behave exactly the same as the input C program according to a formally defined operational semantics of the language. Towards Verified Faithful Simulation

[3] CompCert accepts only a subset of C whose semantics are unambiguous, and rejects programs containing constructions with unspecified behavior as defined by the ISO C 99 standard. Towards Verified Faithful Simulation

[4] The execution of C programs (or programs in the subset of C considered by CompCert) is defined using operational semantics, an approach convenient for proving compiler correctness. Towards Verified Faithful Simulation

[5] The verified SimSoC ARM v6 ISS uses three parts of CompCert: correct compiled machine code, C operational semantics in Coq providing a formal model of the program, and the CompCert Coq library for words, half-words, bytes, and bitwise operations. Towards Verified Faithful Simulation

[6] CompCert provides formalized properties of built-in external functions such as memset and memcpy, enabling formal reasoning about their potential side effects. Towards Verified Faithful Simulation

[7] The verification of the SimSoC ARM v6 ISS relates a C-level "concrete state" to a Coq "abstract state" of the ARM model via a projection, and proves that executing an instruction preserves equivalence of the two states. Towards Verified Faithful Simulation

[8] One cited source states that the subset of C accepted by CompCert is even larger than the subset of C accepted in the SEL4 verification. Towards Verified Faithful Simulation

[9] In a certification-oriented discussion, deductive verification covering the C-to-processor-model transition, as in CompCert, does not remove the need for test sets checking conformance of the processor model against real hardware. Towards Verified Faithful Simulation

[10] The MORAL H2020 project targets a formally verified C compiler, RTOS, and toolchain for a rad-hard microcontroller based on the PEAKTOP architecture with an open ISA, and cites CompCert as an example of a formally verified C compiler. Rad-hard Microcontroller with Open Access ISA for Space Applications

[11] CompCert is hosted on GitHub as AbsInt/CompCert, described as "The CompCert formally-verified C compiler" and primarily written in the Rocq Prover (formerly Coq) language. AbsInt/CompCert