It&#x27;s a verified subset of the C standard rather than all behaviors of all compilers. There&#x27;s some semantics and work covering a lot of that already that just needs to be integrated into CompCert or static analyzers. Likewise, there&#x27;s static analyzers that already cover it too but not formally verified.<p>Here&#x27;s an example of investigating that with Compcert:<p><a href="http:&#x2F;&#x2F;robbertkrebbers.nl&#x2F;research&#x2F;articles&#x2F;compcert_formalin.pdf" rel="nofollow">http:&#x2F;&#x2F;robbertkrebbers.nl&#x2F;research&#x2F;articles&#x2F;compcert_formali...</a><p>Here&#x27;s a semantics that looks for flaws and undefined behavior:<p><a href="https:&#x2F;&#x2F;www.ideals.illinois.edu&#x2F;bitstream&#x2F;handle&#x2F;2142&#x2F;34297&#x2F;Ellison_Charles.pdf?sequence=1" rel="nofollow">https:&#x2F;&#x2F;www.ideals.illinois.edu&#x2F;bitstream&#x2F;handle&#x2F;2142&#x2F;34297&#x2F;...</a>