<story><title>CompCert – Formally-verified C compiler</title><url>https://github.com/AbsInt/CompCert</url></story><parent_chain></parent_chain><comment><author>Cu3PO42</author><text>I have had the pleasure of visiting AbsInt and hearing talks on, amongst other things, CompCert. It really is a fascinating piece of software. I would highly recommend looking at the 2016 paper [1] for a bit more detail on how it works. If you&amp;#x27;re interested you can find other publications as well.&lt;p&gt;The core idea is that every phase of the compiler is proven not to change the behavior of the program. I.e. if you ran any intermediate representation you&amp;#x27;d always get the same behavior.&lt;p&gt;The main limitation is, in my opinion, that the C specification isn&amp;#x27;t available in any form that a proof assistant can consume. Therefore, they had to translate the specification into that form manually. It is possible that this step contains mistakes. On the upside, every C compiler has this problem.&lt;p&gt;[1] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;hal.inria.fr&amp;#x2F;hal-01238879&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;hal.inria.fr&amp;#x2F;hal-01238879&lt;/a&gt;</text></comment>
<story><title>CompCert – Formally-verified C compiler</title><url>https://github.com/AbsInt/CompCert</url></story><parent_chain></parent_chain><comment><author>userbinator</author><text>I think a lot of others here are going to have the question &amp;quot;what does it do with UB&amp;quot;, which is partially answered in the doc:&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;compcert.org&amp;#x2F;man&amp;#x2F;manual005.html#language-reference&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;compcert.org&amp;#x2F;man&amp;#x2F;manual005.html#language-reference&lt;/a&gt;&lt;p&gt;&lt;i&gt;Overflow in arithmetic over signed integer types is defined as taking the mathematically-exact result and reducing it modulo 2^32 or 2^64 to the range of representable signed integers. Bitwise operators (&amp;amp;, |, ^, ~, &amp;lt;&amp;lt;, &amp;gt;&amp;gt;) over signed integer types are interpreted following two’s-complement representation.&lt;/i&gt;&lt;p&gt;...so at least for that case, it behaves sanely, but it&amp;#x27;s unclear what happens for other types of UB.</text></comment>