CompCert – Formally Verified C Compiler
Can you trust your compiler? With CompCert, you can. CompCert is a formally verified C compiler for safety-critical software. It helps eliminate compiler-related defects and reduces duplicate testing effort in high-assurance embedded development.
Our brands
Our brands
Related articles
Partner Insyde Software Launches TapRUUT™
Our partner Insyde has launched TapRUUT, a production-ready Platform Root of Trust designed to deliver standards-aligned firmware security across AI PCs, servers and data centers. Built on full NIST SP...
Read more
Partner IAR Adds Long Term Support Option
Read more
Embedded World 2026 Recap
Read more
EU CRA Compliance with Insyde Software at Embedded World 2026
Read more
The Top 5 Vulnerabilities in Embedded Software and How to Prevent Them
Read more
What CompCert does
CompCert is a formally verified C compiler for safety-critical and high-assurance software. It helps engineering teams trust that the generated machine code preserves the intended behavior of the source code.
Conventional compilers can introduce defects that are hard to detect and costly to investigate. CompCert reduces this risk by using a mathematically verified compilation process, helping teams avoid duplicate testing and reduce toolchain uncertainty.
- Formally verified compilation of C code
- Strong guarantees on compiler correctness
- Reduced risk of compiler-introduced defects
- Less effort spent monitoring compiler bugs
- Reliable code generation for safety-critical systems
By increasing trust in the compilation process, CompCert helps teams build more reliable embedded software and strengthen the foundation for certification and safety assurance.
General Features
Formally verified compiler
Mathematically proven to preserve source code semantics during compilation.
Compiler correctness
Reduces the risk of incorrect behavior introduced by the compiler.
Trusted code generation
Generates reliable machine code for high-assurance embedded systems.
Reduced testing effort
Helps avoid duplicate testing caused by compiler-related uncertainty.
Certification support
Supports safety-critical and regulated software development environments.
Award-winning technology
Recognized with the ACM Software System Award.
Why CompCert
In safety-critical software, source code quality is not enough. The compiler itself must also be trusted.
From compiler uncertainty
to verified compilation
to verified compilation
From hidden toolchain risk
to trusted code generation
to trusted code generation
From duplicate testing
to reduced verification effort
to reduced verification effort
This results in:
Higher confidence
in compiled behavior
in compiled behavior
Reduced risks
in critical applications
in critical applications
Stronger assurance
for certification
for certification
When to use CompCert
CompCert is most valuable in environments where:
Compiler correctness is critical
Toolchain risks must be minimized
Duplicate compiler testing must be reduced
High-assurance embedded software is developed
Typical domains include aerospace, automotive, industrial automation and other safety-critical embedded systems.
André De Ceuninck
Software Quality | Testing | Certification
Can you trust your compiler? With CompCert, you can.
The embedded compiler used for development of safety-critical software has a significant influence on the effort and success of your product development. Eliminate the effort of monitoring compiler bugs and avoids duplicate testing with CompCert.
