SPARKNaCl is a SPARK version of the TweetNaCl cryptographic library, developed by formal methods and security expert Rod Chapman. For two years now, Rod has been developing and optimizing this open-source cryptographic library while preserving the automatic type-safety proof across code changes and tool updates. He has recently given a talk about this experience that I highly recommend.
Rod Chapman - SPARKNaCl: a verified, fast re-implementation of TweetNaCl
In case you'd like to know more, but you're not yet ready to jump into the code on GitHub, you can check out the blog series that Rod has posted over the last two years about the project:
- Proving properties of constant-time crypto code in SPARKNaCl
- Performance analysis and tuning of SPARKNaCl
- Doubling the Performance of SPARKNaCl (again...)
- SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance
Makes for nice reading over Christmas!