vst-crypto
SHA-256 and HMAC specs and lemmas. Compiled Coq modules are included in the folder, so SHA256.v, sha_lemmas.v, and the various HMAC specs should be usable on their own.
From:
https://svn.princeton.edu/appel/vst/sha/
Credit for code: L. Beringer, A. Petcher, A. Appel, and collaborators