SPARKSkein released

Altran Praxis and AdaCore have released SPARKSkein - a new reference implementation of Skein-512 written and verified using the SPARK language and toolset. In particular, this release includes a complete proof of type-safety for the implementation, test cases for structural coverage, performance, and the reference test vectors from the Skein specification.

Download is available from the downloads page or here directly.

The SPARKSkein paper is also available alone.