I'm happy to announce the first release of libsparkcrypto.
Further information, license and source code is available here:
Version 0.1.0 of libsparkcrypto can be downloaded here:
libsparkcrypto is a formally verified implementation of several widely
used symmetric cryptographic algorithms using the SPARK 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.
The distribution contains test cases for all implemented algorithms and
a benchmark to compare its performance with the OpenSSL library. The
achieved speed has been found to be very close to the optimized C and
Assembler implementations of OpenSSL.