The source for the implementation is available on the Skein Hash site. It uses an older version of SPARK though. This has been updated to work with the SPARK 2014 release, as noted here, which reduces the number of loop annotations needed and performs better. There’s more on what the updated SPARK allowed in the sparkstein section here.

It’s interesting that it picked up an error in the C implementation. Also of note in the report that they had an error in their implementation initially showing that even proofs and types don’t prevent all errors:

The first attempt to run this test case failed - the resulting hashes were wrong, illustrating that type- safe code is not necessarily correct. This problem was traced to a simple typing error in the value of the shifting constant R_512_6_3 which had the incorrect value 34 instead of 43

Also of note in the report that they had an error in their implementation initially showing that even proofs and types don’t prevent all errors

It was an error in the formal specification. This is always possible. Formal specs reduce errors in specification in general by eliminating ambiguity. Then, next goal is to use them to prove code correct. Good news is it’s easiest to see and fix errors in specifications as they’re closer to the problem. In the general case anyway.

The source for the implementation is available on the Skein Hash site. It uses an older version of SPARK though. This has been updated to work with the SPARK 2014 release, as noted here, which reduces the number of loop annotations needed and performs better. There’s more on what the updated SPARK allowed in the sparkstein section here.

It’s interesting that it picked up an error in the C implementation. Also of note in the report that they had an error in their implementation initially showing that even proofs and types don’t prevent all errors:

It was an error in the formal specification. This is always possible. Formal specs reduce errors in specification in general by eliminating ambiguity. Then, next goal is to use them to prove code correct. Good news is it’s easiest to see and fix errors in specifications as they’re closer to the problem. In the general case anyway.