--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on April 2020 ---
If you're interested in Monocypher, then you might also take a look at SPARKNaCl.  https://github.com/rod-chapman/SPARKNaCl In short - this is TweetNaCl, re-written in SPARK and with an automatic "auto-active" proof of type safety and some other interesting properties. A more detailed blog entry also here:  https://blog.adacore.com/proving-constant-time-crypto-code-in-sparknacl  - Rod Chapman