Project Everest

Building and deploying provably secure communication software


The main Project Everest web page is hosted on GitHub. This site serves only to aggregate all content on the Microsoft site related to Everest.

The project brings together the following Microsoft Research projects and tools:

  • miTLS – a verified implementation of TLS 1.2 and 1.3
  • HACL* – a verified library of cryptographic primitives
  • EverCrypt – a verified cryptographic library
  • EverParse – an automatic generator for verified parsers and serializers for binary data formats
  • Vale – a verified assembly language
  • Low* and KReMLin, a language subset of F* and a C code generator to model and verify C programs
  • F* – an ML-like functional programming language aimed at program verification
  • Dafny – a verification-aware programming language
  • Z3 – a SMT theorem prover
INRIA graphic
In collaboration with Inria Joint Center