Verified Applications

Several verification projects are based on HACL* and EverCrypt.


The miTLS verified TLS implementation being developed as part of Project Everest relies on EverCrypt for all its cryptography. The current development of miTLS can be found here.


The Signal* verified implementation of the Signal protocol is written in F* and compiles to both C and WebAssembly. Both versions rely on HACL* for their crypto.


The HACL* repository includes a verified Merkle Tree library in /secure_api/merkle_tree which uses the EverCrypt Hash API to build and modify Merkle Trees.