Check it out at www.skein-hash.info
There's also a technical paper describing the implementation and
results, available from
the same place.
- Rod Chapman, SPARK Team, Altran Praxis
> Altran Praxis and AdaCore have released SPARKSkein - a new reference
> implementation of Skein-512 written and verified using the SPARK
> language and toolset...
This is great! Thanks for pointing it out.
Peter
Was useful:
http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf
says
> [...]
> 4.1.1 Prover says no…a bug is discovered
> The subprogram Skein_512_Final caused someproblems, and led to the
> discovery of a subtle
> corner-case bug.
> [...]