CompCert ships a proof, and a non-commercial licence

What is proved, and about which C

The claim is narrow and precise, and it is worth reading exactly as written. CompCert is a compiler for the core C language that generates code for the ARM, PowerPC, RISC-V and x86 processors, and its distinguishing feature is that it has been 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. That is a different kind of statement from a compiler being well tested. A test campaign shows that the compiler agreed with another compiler on the programs somebody thought to write, while a proof covers the programs nobody thought of, within the language the proof is about. The boundary of that language is where the practical work starts, because the README scopes the compiler to core C and then sends you to the website for the list of supported C features, so anything you rely on outside core C is outside the theorem. The README also declines to describe the supported platforms, installation or usage in the repository itself and points to compcert.org and the user's manual instead.

The licence is the first thing to read

CompCert is not free software, and the README says so in the second section. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version, without that restriction and with professional support and extra features, can be purchased from AbsInt, and the LICENSE file in the repository holds the details. The build system shows the same arrangement from another angle, because the header of the Makefile states that the file is distributed under the GNU Lesser General Public License, version 2.1 or later or any later version, and also under the terms of the INRIA Non-Commercial License Agreement. So the picture is a permissive licence with a non-commercial rider attached, not an open source release, and copyright is held by the Institut National de Recherche en Informatique et en Automatique together with AbsInt Angewandte Informatik GmbH. None of this is legal advice, and the point for an engineer evaluating the tool is narrower: if your use is commercial, the free release is not available to you, and that conversation starts with AbsInt rather than with a pull request.

The directory tree is the compiler pipeline

The repository layout describes the architecture more honestly than a diagram would. cparser/ holds the C parser, cfrontend/ the verified front end, backend/ the verified code generation, driver/ the compiler driver, and runtime/ the runtime support, with lib/ and common/ carrying shared definitions. The per-processor directories match the four families in the README exactly, with arm/, aarch64/, x86/, x86_32/, x86_64/, powerpc/ and riscV/ in the tree, and the build selects among them from a single ARCH variable. Two entries are less obvious. export/ is only added to the build when a flag is set, which the Makefile spells CLIGHTGEN, and the README does not explain what that directory produces. debug/, doc/, test/ and tools/ are the ordinary supporting directories, and extraction/ is the Coq extraction step that turns proofs into executable code. For someone deciding whether to read the source, the useful fact is that the proof and the compiler are the same artefacts here, not two implementations kept in step by hand.

The build is a Coq build, and the Makefile says which directories

Building this is not a configure and compile exercise in the usual sense, because the verification is compiled alongside the compiler. The Makefile includes Makefile.config and a VERSION file, so the version is single-sourced, and it derives the list of directories to build from the architecture and from two optional switches. The core of it is one line:

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

From that list it constructs the Coq include paths, mapping each directory to a logical path of the form compcert.<directory>, which is how a proof in cfrontend/ can refer to definitions from lib/ without any manual path juggling. The architecture selection has a small piece of logic worth knowing, because if a directory named for the architecture and bit size does not exist, the build falls back to the architecture directory alone, so a target that has both a 32-bit and a 64-bit variant builds both, and a target with only one builds the one. The .gitmodules file at the root indicates that some components arrive as submodules rather than living in the tree, which is the usual shape for a project that depends on external Coq libraries.

flocq and MenhirLib are optional switches, not assumptions

Two external-looking parts of the build are controlled by variables, and that detail tells you they can be provided from outside the repository. When LIBRARY_FLOCQ is set to local, the build adds four subdirectories, flocq/Core, flocq/Prop, flocq/Calc and flocq/IEEE754, and registers them as the Flocq library. The last of those names is the important one for anyone evaluating a compiler for numeric code, since IEEE 754 floating point is treated as something to be specified rather than assumed. When LIBRARY_MENHIRLIB is set to local, the build adds MenhirLib, and the repository has both a Makefile.menhir and a MenhirLib directory, so the parser generator's runtime library is a build input with its own makefile. Both of these are floating point and parsing concerns, which is a reasonable summary of where a verified C compiler's hard problems sit. There is also a pg directory in the tree that the README does not mention, another sign that the repository carries more than the README documents.

The Makefile documents which proof warnings are silenced

There is a small section in the Makefile about silenced Coq warnings, and it is worth more attention than it gets. The first entry is unused-pattern-matching-variable, with a note recording which Coq version introduced the warning. This is the practical texture of proof-carrying code: the proofs are compiled with a proof assistant that reports style problems in patterns, someone decided the reports were noise, and the decision is written down in the build file rather than buried in a local configuration. That is exactly the behaviour you want from a project whose credibility rests on its proofs, because a reader can see what has been switched off instead of inferring it from silence. It also sets an expectation for anyone contributing: the bar is a clean build with the documented suppressions, and the contribution guide in the repository sets out the process for a project with this structure.

Release cadence, documentation location and who answers questions

Three releases are visible and they are roughly six months apart: v3.16 on 2025-09-01, v3.17 on 2026-02-13 and v3.18 on 2026-08-30, with the last push to master on 2026-09-24. A version numbering that has reached 3.18 after more than a decade of development, and a master branch that is still moving after the 3.18 tag, is the profile of a project that is stable in its interfaces and conservative in its releases. Documentation is deliberately not in the repository. The README routes everything, supported platforms, supported C features, installation instructions and usage, to the website and to the user's manual at compcert.org/man/, which is a sensible division, because manuals that track a release are better served from a site than from a moving branch. General discussion goes to the [email protected] mailing list, and commercial enquiries go to [email protected]. The Makefile header also credits the project's origin at INRIA Paris-Rocquencourt, which is where the verification work behind this compiler has been done.

A proof and a test campaign answer different questions

The alternative approaches to trusting a compiler are not really alternatives so much as a different answer to the same question. A conventional compiler such as GCC or Clang accepts far more of C than the core language, is free, and is validated by testing, including large-scale differential testing against other compilers. That is a weaker guarantee in the logical sense and a much better one in the practical sense for code that lives outside the verified subset. A proof gives you a guarantee that holds for every input in the language, which is exactly what you want for code where a miscompilation is a safety problem, and gives you nothing at all for the parts of C the theorem does not cover, including whatever the front end handles outside the verified path. The commercial route is a third option rather than a different technology: the same verified compiler with the non-commercial restriction removed, professional support and extra features, which is the version to evaluate if the licence is your binding constraint.

Editorial conclusion

Adopt CompCert if you are writing safety-critical C and want the compiler's correctness to be a theorem rather than a test campaign, and if your licence situation lets you use a non-commercial release or a purchase from AbsInt. Do not adopt it to compile ordinary application C, where the supported subset is narrower than what GCC or Clang accept and the licence is the binding constraint, not the proof. Verify four things before you plan around it: which C features you need are inside the core language the guarantee covers, since the README defers that list to the website, that the build completes on your toolchain, since the Makefile is a Coq build driven by configure and Makefile.config, that your organisation can accept the licence terms in the LICENSE file, and that the version you build is one you can reproduce, given releases v3.16 on 2025-09-01, v3.17 on 2026-02-13 and v3.18 on 2026-08-30. Copyright sits with INRIA and AbsInt, and the last push to master was 2026-09-24.

Frequently asked questions

Official sources

1. AbsInt/CompCert on GitHub
2. Issues
3. Project website
4. README
5. Releases