Also, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~rege

Also, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf • https://compcert.org/motivations.html https://compcert.org/motivations.html I think things may have improved further since the 2011 paper, where they found bugs in parts of CompCert which were not, at the time at least, formally verified. The formally verified parts of CompCert withstood torture testing admirably.