hacl

Experiments in applying formal methods to cryptographic software to provide higher assurance.

Contributions welcome!

Setup

Run

$ git submodule init
$ git submodule update

libsodium-verifast

libsodium with some verification by VeriFast.

tis-ct.tb2

Pre-packaged tis-ct (constant time verifier) for x86-64 MacOS X and x86-64 Linux.

Unpack with

$ tar xvfy tis-ct.tb2

then see the README.