Almost as fun as SPARK's own Rod Chapman doing some tweetnacl porting and proof https://blog.adacore.com/sparknacl-two-years-of-optimizing-c...