Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Project Everest – Verified Secure Implementations of the HTTPS Ecosystem


News & features

News & features

News & features

News & features



Project Everest aims to build and deploy a verified HTTPS stack.

The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year.

Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem. We are looking to cover from the HTTPS API down to  TLS and including cryptographic algorithms such as RSA and AES. At the TLS level, for instance, we will develop new implementations of existing and new protocol standards while formally proving that our implementations provide a secure-channel abstraction between the communicating endpoints. Project Everest aims to be a drop-in replacement for the HTTPS library in mainstream web browsers, servers, and other popular libraries and tools.

secure diagram insecure diagram

GitHub Repo

Project Everest is built as an open source project involving contributions from Microsoft, Microsoft-INRIA Partnership, Carnegie Mellon University, and the Community at large.

Related Projects

The project brings together the following Microsoft Research projects

  • miTLS – a verified implementation of TLS 1.2
  • F* – an ML-like functional programming language aimed at program verification
  • Dafny – a verification-aware programming language
  • Z3 – a SMT theorem prover
  • Ironclad – provably secure and reliable systems

Microsofr Research Inria Join Centre logo


Talks & workshops