• 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