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.