Formally Verified Optimizing C Compiler
CompCert - AbsInt Angewandte Informatik GmbH (AbsInt)
Meet the highest levels of software assurance by compiling your application with the only C compiler that's been formally verified to be free of miscompilation issues. All safety properties verified on the source code, e.g. with Astre, are guaranteed to hold for the generated executable as well.