Project Everest
Building and deploying provably secure communication software
Summary
The main Project Everest web page (opens in new tab) is hosted on GitHub. This site serves only to aggregate all content on the Microsoft site related to Everest.
Related work
The project brings together the following Microsoft Research projects and tools:
- miTLS (opens in new tab) – a verified implementation of TLS 1.2 and 1.3
- HACL* (opens in new tab) – a verified library of cryptographic primitives
- EverCrypt (opens in new tab) – a verified cryptographic library
- EverParse (opens in new tab) – an automatic generator for verified parsers and serializers for binary data formats
- Vale (opens in new tab) – a verified assembly language
- Low* and KReMLin (opens in new tab), a language subset of F* and a C code generator to model and verify C programs
- F* (opens in new tab) – an ML-like functional programming language aimed at program verification
- Dafny (opens in new tab) – a verification-aware programming language
- Z3 (opens in new tab) – a SMT theorem prover
