Project Everest is a large, collaborative research effort that aims to verify and deploy a new, secure HTTPS stack. All of our code is verified using the F programming language. Using KreMLin, a dedicated compiler, the verified F code is compiled to readable C, meaning existing systems projects can readily integrate our verified code. Going to C is what allows people to use our code without having to buy into exotic, strange languages with lambdas.