Comment by johnisgood

Whoops, I completely forgot about libsparkcrypto (https://github.com/Componolit/libsparkcrypto) which is a "formally verified implementation of several widely used cryptographic algorithms using the SPARK 2014 programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.".

Features:

* AES-128, AES-192, AES-256

* AES-CBC (all supported AES modes)

* SHA-1

* HMAC-SHA1

* SHA-256, SHA-384, SHA-512

* HMAC-SHA-256, HMAC-SHA-384, HMAC-SHA-512

* PRF-HMAC-SHA-256, PRF-HMAC-SHA-384, PRF-HMAC-SHA-512

* RIPEMD-160

* HMAC-RIPEMD-160

* ECDSA, ECGDSA

It is pretty awesome. :)