Countermeasures to various attacks can be introduced into programs, but this is cumbersome to do manually and furthermore some may be removed by the compiled. It seems a good idea to add such countermeasures at compile time. Yet, this must not disturb the normal execution of programs.
CompCert is a formally verified compiler. Adding countermeasures directly inside CompCert involves formally proving that these countermeasures do not alter the normal execution of the program.
See also this related proposal
