CompCert is a formally verified optimizing C compiler. It accepts most of the ISO-C 99 language, with some minor exceptions and a few useful extensions. Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance.
What sets CompCert apart from other production compilers is that it is formally verified, using machine-assisted mathematical proofs: the executable code it produces is proved to behave exactly as specified by the semantics of the source C program. Hence, all safety properties verified on the source code automatically hold as well for the generated executable.
In the course of the Scale4Edge project, CompCert was given a backend for RISC-V, which had not been supported before, and CompCert for RISC-V has been combined with picolibc, a C library designed for embedded 32- and 64-bit microcontrollers with small memory.
Installation packages for Linux and Windows are available for download from the AbsInt download server.
This distribution of CompCert can be used for evaluation and research, but not for commercial purposes (see also the license information in the installation packages). Commercial licenses can be obtained from AbsInt.
AbsInt Angewandte Informatik GmbH
Sales Department
Science Park 1
66123 Saarbrücken
Deutschland