hax & hacspec

We have been applying hax to verify several Rust pieces of software recently. hax was used to verify Libcrux’s implementation of ML-KEM with F*, but also for smart contracts verification with Coq, and even on protocols with F* and our new ProVerif backend. Meanwhile, we also presented hax at several conferences and workshops. The need for more documentation and guidance was becoming apparent: it was about time to have a tutorial!...

This has been in the making for a while now. But we are finally happy to announce the first release of hax. It is still early days and we only tagged v0.1. But a ton of work has gone into this release. Wait, what is hax? Let’s start at the beginning. A group of us started hacspec (high assurance crypto specifications), a language for specifying cryptographic primitives as the basis for formal verification, in early 2018 at the HACS workshop....