CompCert : une révolution pour le développement avionique

Temps de lecture : 6 minutes • Avril 2026

Dans les systèmes avioniques critiques, la moindre erreur logicielle peut avoir des conséquences majeures. Parmi les maillons les plus sensibles de la chaîne de développement figure le compilateur, cet outil chargé de transformer le code source en code machine. Or, même les compilateurs les plus répandus comportent des bugs, parfois invisibles, générant du code machine incorrect. Ce phénomène, appelé miscompilation peut rester indétecté malgré des milliers d’heures de test. L’ensemble des acteurs de l’industrie de l’aviation tel que Airbus en ont conscience et connaissent les enjeux qui y sont liés.
C’est précisément cette problèmatique que résout CompCert, le premier compilateur C optimisant et formellement vérifié, développé par AbsInt.

Dans cet article, nous revenons sur les enjeux de cette technologie, son intégration dans l’écosystème avionique d’Airbus, et les raisons pour lesquelles elle constitue un levier clé pour la certification DO‑178C/DO‑330.

Contrairement aux compilateurs traditionnels, CompCert repose sur :

• Une preuve mathématique formelle, validée par le prouveur Coq ;
• Une préservation sémantique démontrée entre le code source et le code machine ;
• Une absence prouvée de miscompilation, ce qui élimine une grande partie des risques classiques liés aux outils.
• 20 passes de compilation et 11 langages intermédiaires, chacun vérifié individuellement puis composés pour assurer une fiabilité de bout en bout.

Grâce à sa preuve formelle de préservation sémantique, le code machine généré par CompCert se comporte conformément au programme C d’origine. Cette propriété est au cœur de sa conception et résulte de la vérification formelle de chacune des étapes de compilation. Cette combinaison, optimisation et preuve formelle, fait de CompCert une solution disponible assez unique et adaptée aux environnements critiques où la confiance dans le compilateur est essentielle.

Dans l’avionique, les standards tels que DO 178C / DO 330 / DO 333, imposent des contraintes fortes pour garantir la sûreté logicielle.

Avec CompCert, de nombreuses obligations deviennent plus simples, plus fiables, et moins coûteuses.

Historiquement, les compilateurs n’étaient pas qualifiés : on compensait par davantage de tests. Avec CompCert, c’est l’inverse : la preuve formelle devient la base de la qualification.

AbsInt fournit un kit de qualification fourni comprenant :

• Les TOR (Tool Operational Requirements) couvrant l’intégralité de la norme ISO C99,
• Les TR (Tool Requirements) détaillés, formels et informels,
• Des jeux de tests complets (TVCP, TOVVCP),
• Les outils de traçabilité et des revues structurées,
• Un support adapté à l’obtention d’un TQL‑3 DO‑330 avec allègements documentés.

Cette approche dépasse largement les méthodes traditionnelles basées principalement, voir uniquement, sur des suites tests

Conclusion : Ce que cela change pour les industriels ?

L’intégration de CompCert dans le développement avionique n’est pas simplement une évolution technique : c’est un changement de paradigme, on passe d’un monde où « on teste beaucoup » à un monde où on prouve que le compilateur est correct.
En éliminant les risques liés aux miscompilations et en apportant des preuves formelles exploitables dans la DO‑178C/DO‑330, CompCert permet :

• De développer plus rapidement
• De certifier plus sereinement
• De conserver des performances optimales en conservant les optimisations
• D’éliminer toute une classe de risques historiques
• De réduire drastiquement les coûts vérification