CompCert Qualification Achieved for Avionics Software

AbsInt is proud to announce that at the beginning of 2026 the CompCert compiler has officially been qualified for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircrafts. For the first time, certification credits from compiler usage can be claimed for critical avionics software in compliance with DO-178C, DO-333, and DO-330.

Successful qualification of CompCert for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircrafts

Claiming certification credits from a compiler allows applicants to eliminate, reduce, or automate specific objectives defined by DO-178C. The use of CompCert supports the objective of verifying property preservation between source and object code — even in the presence of compiler optimizations. As a result, test effort can be reduced. For example, formal verification performed at the source-code level can replace certain object-code testing activities otherwise required to demonstrate that the executable code complies with low-level requirements and maintains robustness.

The AbsInt Qualification Support Kit further reduces certification effort and cost. It represents a major advancement in the qualification of compilers for avionics software at the highest assurance levels under DO-178C.

CompCert is the first commercially available optimizing compiler to be formally verified. The machine code it generates is mathematically proven to conform exactly to the formal semantics of the source C program. CompCert supports multiple target architectures, including PowerPC, ARM, TriCore, RISC-V, and x86.

In recognition of its groundbreaking formal proof, CompCert received the ACM Software System Award in 2021. It has been successfully deployed in commercial projects for many years and has also been qualified in safety-critical industry applications certified under IEC 60880.

By adopting CompCert, organizations can achieve significant gains in application performance and development efficiency while reducing the risk of malfunctions due to miscompilation.

If you have any questions, please do not hesitate to contact us.