`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/.
A little list: http://anna.fi.muni.cz/yahoda/