# CompCert: a verified C compiler under three different licence descriptions

> This is the C compiler whose generated assembly is formally guaranteed to follow the semantics of the source, built on a proof assistant and shipping as a non-commercial release with a commercial version sold separately. The README is 190 words and points at a website, so the interesting material is in the build system: a directory list that becomes the proof namespace, and an explicit list of suppressed prover warnings.

**AbsInt/CompCert** — The CompCert formally-verified C compiler

- Repository: https://github.com/AbsInt/CompCert
- Website: https://compcert.org
- Stars: 2,236 · Forks: 263
- Language: Rocq Prover
- License: NOASSERTION
- Published: 2026-09-29 · Updated: 2026-09-29 · Language: en
- Canonical page: https://hysenlabs.com/projects/absint-compcert

## Non-commercial in the README, LGPL and an INRIA agreement in the build file

The licence is described three ways and only one of them is in the README.

The README is unambiguous about intent. CompCert is not free software, this non-commercial release can only be used for evaluation, research, educational and personal purposes, and a commercial version without that restriction, with professional support and extra features, can be purchased from AbsInt.

The build file says something different in its own header comment, naming Xavier Leroy and INRIA Paris-Rocquencourt as the authors of the file and stating that it is distributed under the GNU Lesser General Public License, either version 2.1 or later, and also under the terms of the INRIA Non-Commercial License Agreement. Two terms, not one.

The repository's licence metadata field reads as not asserted, so a tool reading the API learns nothing. A LICENSE file exists at the root and is pointed to by the README for more information.

This review does not resolve which terms govern your use. What can be said is that the free-of-charge release has an explicit non-commercial restriction in its own documentation, and that a differently licensed version exists for purchase.

Copyright is held by INRIA and by AbsInt Angewandte Informatik GmbH, and the README routes general discussion to a mailing list at inria.fr while commercial inquiries go to a separate address.

## The guarantee is about core C, and the prover has been renamed

The overview is three sentences and the third one is the whole project.

CompCert is a compiler for the core C language that generates code for the ARM, PowerPC, RISC-V and x86 processors. The distinguishing feature is that it is formally verified using the Coq proof assistant, so the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.

Two things are worth pulling out of that sentence. The first is that the target is the core language, so the guarantee is scoped to what the front end accepts rather than to the extensions a real codebase uses. The second is the direction of the guarantee: it is about the generated assembly matching the semantics of the source, which is not the same claim as the compiler being free of defects in every other respect.

There is a small naming detail in the same paragraph. The README says Coq, while the repository's primary language is reported as the Rocq prover. That is the same proof assistant under its newer name, and it means documentation written before the rename and tooling configured after it will use different words for the same thing.

Everything else a user would ask, supported platforms, supported C features, installation instructions and how to drive the compiler, is delegated to the project website and its user's manual.

## The repository is the source, not the manual

The README is 190 words, which is a deliberate choice rather than an omission. Its job is to say what the project is, where to read more and who to contact.

That means the questions a new user actually has are answered somewhere else. The README points at the website for supported platforms, and at a separate user's manual for installation, usage and the supported subset of C. It also points at a changelog and a licence file in the repository, and at a mailing list for general discussion.

So the practical shape of adopting this project is: clone the repository to get the source, then follow the manual for everything about running it. The supported processor list in the README is one line long and names four families, while the supported C feature list is not in the repository at all.

That division is defensible for a project of this kind, where a manual is versioned separately from the source tree and the source tree is a proof artifact first and a program second. It does mean an evaluation has to leave the repository, and that the gap between the tree and the manual is where surprises live.

## Four processor families in the prose, seven directories in the tree

The README names ARM, PowerPC, RISC-V and x86. The top level of the repository has seven architecture directories: aarch64, arm, powerpc, riscV, x86, x86_32 and x86_64.

The split is not arbitrary. The build takes an architecture name and a bit size, and the makefile has a rule that decides which directories to build:

```
ifeq ($(wildcard $(ARCH)_$(BITSIZE)),)
ARCHDIRS=$(ARCH)
else
ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
endif
```

So when a directory named for the architecture and bit size exists, both that directory and the architecture-level one are built. That is why x86 appears next to x86_32 and x86_64, and why arm appears next to aarch64.

The directory names are also the identity of the code, not just folders to copy. A reader who wants to know what the compiler supports has two sources of truth that do not agree in count, and the makefile is the one that decides what gets built.

The remaining top-level entries follow the same pattern of naming what the build does: a backend directory, a cfrontend for the front end, a cparser, a driver, a common directory, a runtime and a lib, plus debug, doc, export, extraction and tools directories and a test directory.

## The proof namespace is generated from the build order

The build is driven by a list of directories, and that list becomes the logical path space of the proofs.

```
DIRS := lib common $(ARCHDIRS) backend cfrontend driver cparser
```

and then each of those directories is mapped into the prover's namespace with a recursive flag:

```
COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d))
```

So a directory called cfrontend is addressable in proofs as compcert.cfrontend, and the architecture directories follow the rule from the previous section. Renaming or moving a directory is therefore a change to the proof namespace, not just to the build.

The list is not fixed. One entry is conditional: when CLIGHTGEN is true, an export directory joins the list, which is the intermediate language export path. Another variable set controls the build identity, with the makefile including both a generated configuration file and the repository's VERSION file, then defaulting a build version, a build number, a tag and a branch from it.

Nothing in the repository is hard-coded to one release. The version comes from the VERSION file that the build includes, which is also how the same tree can produce a development build.

## Two OCaml dependencies are local submodules or system libraries

Two directories in the tree are third-party components that the build can either use locally or take from the system.

The first is a parser generator library, present as MenhirLib. The second is a floating-point correctness library, present as flocq, with subdirectories for its core, its properties, its calculus and an IEEE 754 directory. There is a .gitmodules file at the root, so at least one of these is also available as a submodule.

The makefile switches on two variables:

```
ifeq ($(LIBRARY_FLOCQ),local)
DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754
COQINCLUDES += -R flocq Flocq
endif
```

and the same pattern for the parser library. When the value is local, the subdirectories are appended to the build list and a recursive flag is added under its own namespace.

That the IEEE 754 directory is part of the default local build is the useful detail here. It says floating-point semantics are proved rather than assumed, which is consistent with a project whose central claim is about the generated code following the source semantics.

For a contributor the choice is a build-time decision with a consequence: the local path builds those proofs as part of the project, and the system path assumes they are already installed and compatible.

## The build silences a named set of prover warnings

Partway down the makefile there is a block of comments headed with notes on silenced Coq warnings, and the first entry is a warning introduced in a particular prover version, concerning unused pattern matching variables.

That block exists because a verification build produces warnings, and a project that treats the build output as evidence has to decide what to do with them. Listing them is a defensible choice: a reader can see exactly which warnings are being suppressed rather than discovering a blanket flag.

It is also the kind of thing that ages. A warning name that a prover renames in a later version will either stop matching or start matching something else, and the block has to be maintained by hand.

The rest of the project signals are consistent with a long-lived academic codebase. Releases come at roughly six-month intervals, with 3.16 in September 2025, 3.17 in February 2026 and 3.18 in August 2026, and the last push to master was 2026-10-02. The copyright holders, the mailing list for users and the separate address for commercial inquiries all point at a project run as research infrastructure with a commercial arm alongside it.

## Conclusion

Adopt CompCert when you need a C compiler whose output you can argue about, since the guarantee it offers is narrow and precise: the generated assembly behaves as the semantics of the source C prescribe, for the core C language and for the processor families in the tree. Do not expect it to replace a general compiler toolchain without reading the manual, because the supported C features and the installation instructions are not in the repository, and the guarantee covers the core language rather than the extensions you use. Before you build it, settle the licence question, since this release is non-commercial and a differently licensed version is sold by AbsInt, and read the list of silenced proof warnings so you know what the build is not telling you.

## FAQ

### What is a CompCert?

A C compiler from INRIA and AbsInt that targets the core C language and generates code for ARM, PowerPC, RISC-V and x86 processors. Its distinguishing feature is formal verification with the Coq proof assistant, so the generated assembly is guaranteed to behave as prescribed by the semantics of the source C code.

### compcert vs gcc

The repository does not make that comparison. It states that CompCert compiles the core C language, generates code for ARM, PowerPC, RISC-V and x86, and that the generated assembly is formally guaranteed to follow the semantics of the source. Supported C features and installation instructions are on the project website and in its user's manual.

### Is CompCert free software?

The README says it is not. The non-commercial release can only be used for evaluation, research, educational and personal purposes, and a commercial version without that restriction, with support and extra features, can be purchased from AbsInt. The build file's header also names the LGPL and an INRIA non-commercial agreement.

### Which processors does the CompCert source tree cover?

Seven architecture directories: aarch64, arm, powerpc, riscV, x86, x86_32 and x86_64. The build takes an architecture and a bit size and builds both the architecture directory and the architecture-and-bit-size directory when the latter exists, which is why the x86 family appears as three directories.

### What are MenhirLib and flocq in the CompCert repository?

Two local dependencies used by the build. A parser generator library and a floating-point correctness library, each of which can be built from the repository or taken from the system through a build variable, with the flocq build including its core, properties, calculus and IEEE 754 directories.

## Sources

- [AbsInt/CompCert on GitHub](https://github.com/AbsInt/CompCert)
- [Issues](https://github.com/AbsInt/CompCert/issues)
- [Project website](https://compcert.org)
- [README](https://github.com/AbsInt/CompCert/blob/master/README.md)
- [Releases](https://github.com/AbsInt/CompCert/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/absint-compcert