Author here. I guess what I was trying to say is that CompCert as a system has been trusted for over 10 years, yet only now do we find such a silly correctness bug. People won't read the paper to find out that parsing is unverified, they'll just trust CompCert because they hear it's been rubber-stamped as "formally verified". And that's dangerous.

A better way to do it is pull up C compilers, get their bug rates, and compare it to CompCert for both unverified and verified parts. First tests formal specs + safe language where latter tests verification. You can use smaller, C compilers if uou want to be fair. Two or three spec errors versus what you find in other compilers would corroborate CompCert team's claims. Likewise for verified TLS versus ad hoc protocols or implementations.

Hi, author here. I definitely agree the valuable part is thinking through the verification process, which devotes a lot of time to understanding the system and adds resilience in edge cases. Someone on Twitter brought that up: https://twitter.com/jetapiador/status/943909582279233536. Perhaps that's what I should have concluded my argument with.