(... to be written)


[ZBPB17] explains HACL* in detail. The underlying F*/Low* to C translation (with KreMLin) is explained in [B17]. HACL* is available on GitHub[HACL*] as is KreMLin[KreMLin]. The main application and motivation driving the design and implementation of HACL* is implementing and proving the TLS 1.3 Record Layer[B16], but HACL* can, of course, be used everywhere: it has a NaCl/libsodium like API.

Some people, not being fluent in ML/OCaml, don't like writing cryptographic specifications in F*/Low*. Project hacspec[hacspec] aims to create a Python-like language for specs that translates to cryptol, Coq, F*, EasyCrypt. It is in a very early stage though. A paper[BKS18] and slides outline this effort.

This crypto bite is inspired by Karthikeyan Bhargavan's talk "Verified Cryptographic Libraries", starting at 21:02, at the 8th BIU Winter School on Cryptography, Secure Key Exchange, February 11-15 2018 (all videos).

and the followup talk "Verified Cryptographic Protocol Implementations":

A similar presentation on Low* is "Verified Low-Level Programming Embedded in F*" [B17]: