[Jabbles]

Actually the bugs they found in CompCert were not in the proved sections. The CSmith paper says

"As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users."

https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

[nickpsecurity]

"The problem is that the 16-bit displacement field is overflowed. CompCert’s PPC semantics failed to specify a constraint on the width of this immediate value, on the assumption that the assembler would catch out-of-range values. In fact, this is what happened. We also found a handful of crash errors in CompCert."

That bug was in the backend. I believe it's verified code based on this paper's existence:

http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf

The code correctly implemented a bad spec far as I can tell. The crash errors aren't elaborated so I can't say what they imply. So, for backend, there was at least one bug found in verified versions due to inaccurate spec.

Shows value of multiple forms of verification which Orange Book era research already supported empirically. Corroborated by Altran-Praxis and others in recent times. I've included example papers on LOCK's design/cost and Altran-Praxis' CA since they're representative of trends I've observed over time. Proving part, for common errors at least, has gotten a lot easier though with tools like SPARK. I wanted CompCert derived into SPARK at one point.

http://www.cyberdefenseagency.com/publications/LOCK-An_Histo...

https://cryptosmith.files.wordpress.com/2014/10/lock-eff-acm...

http://www.anthonyhall.org/c_by_c_secure_system.pdf