--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on April 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] checking Monocypher



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