A cryptographic library called EverCrypt was released on April 2, 2019. It was written in a programming language - F* (fstar) - which was specifically created in order to write EverCrypt. Basically it allows code to be written, formally verified, and then compiled into C and assembly language. The project of which EverCrypt is a part - Everest - is meant to surround EverCrypt with formally verified software with which the library can interact. The main goal of Everest at the time of writing is a set of libraries which will result in an implemented https ecosystem.

In an ideal world I would learn FStar and write everything in it! But the article indicates that we are a long way away from that, due to the complexity of modern software. We need to start with small components and build up from there. Still, this doesn't mean we can't start getting used to writing in F*, even at this early stage. In that spirit, I will investigate one of the other links in the article - fstar-lang.org.