Everest is a recursive acronym: It stands for the “Everest VERified End-to-end Secure Transport”. //
Project Everest addresses this problem by constructing a high-performance, standards-compliant, formally verified implementation of components in HTTPS ecosystem, including TLS, the main protocol at the heart of HTTPS, as well as the main underlying cryptographic algorithms such as AES, SHA2 or X25519. //
We aim for our verified components to be drop-in replacements suitable for use in mainstream web browsers, servers, and other popular tools and are actively working with the community at large to improve the ecosystem.
Project Everest is the combination of the following projects. Read below for an easy way to install all these projects together.
- F*, a verification language for effectful programs
- miTLS, reference implementation of the TLS protocol in F*
- KreMLin, a compiler from a subset of F* to C
- HACL, a verified library of cryptographic primitives written in F
- Vale, a domain-specific language for verified cryptographic primitives in assembly
- EverCrypt, a verified crypto provider that combines HACL* and Vale via an agile, multi-platform, self-configuring cryptographic API.
