A shallow survey of formal methods for C code

Here's a link to an older thread for the same article, for convenience: https://news.ycombinator.com/item?id=8282949

For anyone interested, here is another paper concerning similar topics:

`Verification of a Cryptographic Primitive: SHA-256',

https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf.

And don't forget about `CompCert C compiler',

http://compcert.inria.fr/compcert-C.html.

Or the `Vellvm' project,

http://www.cis.upenn.edu/~stevez/vellvm/.

His update to this old blog post is much better: https://www.imperialviolet.org/2014/09/11/moveprovers.html but he hasn't found cbmc yet.

A little list: http://anna.fi.muni.cz/yahoda/