Related Projects

miTLS - a verified reference implementation of TLS

HACL* - a verified library of cryptographic primitives

Vale - Verfied Assembly Language for Everest

EverCrypt - Verified crypto provider that combines HACL* and Vale via an agile cryptographic API

EverParse - Automatic generation of verified parsers and serializers for binary data formats; used by miTLS

F* - a verification language for effectful programs; used by EverParse, miTLS, HACL* and Vale

KreMLin - a compiler from a subset of F* to C; used by EverParse, miTLS and HACL*

Z3 - SMT solver; used by F* and Dafny

Dafny - a program verifier; used by Vale