libsparkcrypto – A cryptographic library implemented in SPARK

As per September the 9th. 2010, Alexander Senier have released version 0.1.0 of libsparkcrypto, a cryptographic library build using the SPARK programming language.

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.

You can read the release announcement or go straight the to the code. The API is documented here.

Leave a Reply