SPARKNaCl: A verified, fast cryptographic library
Director, Protean Code
SPARKNaCl https://github.com/rod-chapman/SPARKNaCl is a new, freely-available, verified and fast reference implementation of the NaCl cryptographic API, based on the TweetNaCl distribution. It has a fully automated, complete and sound proof of type-safety and several key correctness properties. In addition, the code is surprisingly fast - out-performing TweetNaCl's C implementation on an Ed25519 Sign operation by a factor of 3 at all optimisation levels on a 32-bit RISC-V bare-metal machine. This talk will concentrate on how "Proof Driven Optimisation" can result in code that is both correct and fast.