What appeals about this approach to me is you can make crash free C code, and just integrate it in normal C programs without anyone using your code needing any special tools. The proofs are just comments after all.
In such a case, you might be interested in this paper about the journey to write a RTE-free x509 parser.
There was a talk last week about it, but it’s in French :\.
That certainly has inspired me - I have a plan for an init system that may benefit from this approach.
Loved that paper. Thanks. The stuff they talk about on page 2 is exactly what I previously pushed for calling it Design for Verification. I learned it from early proving work where they said that just rewriting the specs and code in preparation for proofs often caught problems. Probably the clarity that came from simplifying them. Now, we have automated analyses, too. :)
IIRC, the tool also supports turning contracts into runtime checks in the event it’s too hard for the user to prove.