HACL* in OCaml: safe bindings for verified C code using Ctypes

Ecosystem
1

I wanted to share a blog post that we wrote a while back at Nomadic Labs. I thought this might be interesting to folks here, particularly the more in-depth discussion on how we use Ctypes to safely interface with the formally verified C code of the HACL* cryptography library in OCaml and on the design of our high-level API.

4 Likes
2

@vdum thanks! I have a different but related question: recently @dbuenzli announced OCaml bindings to TweetNaCL; if I remember correctly, Nomadic Labs had similar bindings at some point (which were replaced by HACL* bindings?). Do you have a pointer to your TweetNaCL bindings?

1 Like
3

Indeed, Nomadic Labs used Tweetnacl before switching over to HACL*. The bindings have since been removed from the repo. A copy can be found here.