Formally verified compilation for ARM

CompCert for ARM is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It ac­cepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for 32-bit and 64-bit ARM.

What sets CompCert apart?

ACM Software System Award

CompCert is the only production compiler that is formally verified, using machine-assisted math­ematical proofs, to be exempt from mis­compilation issues. The code it pro­duces is proved to behave exactly as specified by the semantics of the source C program.

This level of confidence in the correctness of the compilation process is unprecedented and con­tributes to meeting the highest levels of software assurance.

In 2022, the Association for Computing Machinery, ACM, presented the CompCert development team with the prestigious ACM Software System Award. Subsequently, the team also received the ACM SIGPLAN Programming Languages Software Award.

Formally verified optimizations

CompCert implements the following optimizations, all of them formally verified:

Compilation with execution time in mind

On typical embedded processors, code generated by CompCert typi­cally runs twice as fast as code generated by GCC without optimizations, and only 20% slower than GCC code at optimization level 3.

Chart of CompCert vs. GCC execution times for 23 benchmarks
Execution times of 23 benchmark programs compiled with ■ gcc -O0, ■ CompCert, ■ gcc -O1, and ■ gcc -O2

Your benefits

With CompCert it is possible to decrease the execution time of our flight control algo­rithms by a sig­nif­icant amount. The reduction of the execution time can be used for additional functionality.”

TU Munich, Institute of Flight System Dynamics


The computed WCET bounds lead to a total processor load which is about 28% smaller with the CompCert-generated code than with the code generated by the conventional compiler. The main reason for this behaviour is the improved memory performance. The result is consistent with our expectations and with previously published CompCert research papers.”

MTU Friedrichshafen

Supported targets

Supported target system is Linux. 32-bit EABI is supported with the GNU toolchain.

Postpass validation

An optional tool called Valex is available for the postpass validation of the assembling and linking steps. It compares the instructions in the abstract assembly code produced by CompCert to the instructions in the linked binary executable, checks whether symbols are used consistently, whether variable size and initialization data match up, and whether variables are placed in the proper sections in the executable.

Free trial

Request your free trial package today.