For anyone interested, here is another paper concerning similar topics: `Verification of a Cryptographic Primitive: SHA-256', https://www.cs.princeton.edu/~ap

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 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 http://compcert.inria.fr/compcert-C.html. Or the `Vellvm' project, http://www.cis.upenn.edu/~stevez/vellvm/ http://www.cis.upenn.edu/~stevez/vellvm/.