Here’s some new software that I’ve been working on in my spare time over the last few months. I’ve decided to make the code freely available under the simplified BSD licence.
SPARKNaCl has been verified “type-safe” (aka “no runtime errors”) by the SPARK toolset, and the proof is fully “auto-active” meaning the standard set of provers discharge every single verification condition, with no interactive proof at all, based solely on the contracts in the code and nothing else. In addition, some interesting correctness properties have been verified en-passant.
This was all something of a challenge – cryptographic code like TweetNaCl sets some particularly difficult challenges for both the human brain and for automated verification tools alike. Read all about it here.