• 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
  • F* - a verification language for effectful programs; used by miTLS, HACL*, and Vale
  • KreMLin - a compiler from a subset of F* to C; used by miTLS and HACL*
  • Z3 - SMT solver; used by F* and Dafny
  • Dafny - a program verifier; used by Vale