EverCrypt—developed and verified by the Project Everest team—offers the same features, convenience, and performance as popular existing cryptographic libraries without the bugs that leave protocols and applications vulnerable. Usable by verified and unverified clients alike, EverCrypt emphasizes both multiplatform support and high performance. We accomplish this by producing both platform-agnostic C code and optimized assembly code for specific hardware targets through the combination of two components of Project Everest: the HACL* cryptographic library developed jointly between Inria and Microsoft Research and the Vale-Crypto library of assembly primitives developed collectively between Microsoft Research and Carnegie Mellon University.By Jonathan Protzenko, Researcher; Bryan Parno, Associate Professor, Carnegie Mellon University
The verification process is likely more complex than the code itself. Anyway, this is one great step. Read the full article over at Microsoft.