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

F* - A proof assistant and verification language for effectful programs

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