There's a section in the tweetNaCl paper that discusses some limited formal verification. For some interesting commentary on the difficulty in formally verifyi

There's a section in the tweetNaCl paper that discusses some limited formal verification. For some interesting commentary on the difficulty in formally verifying c code (with crypto examples) see: https://www.imperialviolet.org/2014/09/07/provers.html https://www.imperialviolet.org/2014/09/07/provers.html and the followup https://www.imperialviolet.org/2014/09/11/moveprovers.html https://www.imperialviolet.org/2014/09/11/moveprovers.html