It exists. It&#x27;s called CompCert.<p><a href="https:&#x2F;&#x2F;github.com&#x2F;AbsInt&#x2F;CompCert" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;AbsInt&#x2F;CompCert</a><p>It&#x27;s free for non-commercial use. I&#x27;ve used it for several months now to build things like Tor. I haven&#x27;t noticed any disadvantage compared to GCC or Clang.