hax & hacspec

This first blog post inaugurates our series named “This Month in hax”: a series of short highlights of what happened in the development of hax and it’s ecosystem in the month. In June, 23 PRs have been merged 🎉! The detail is available below. On the Rust side, we have updated the Rust compiler to a very recent nightly thanks to @Nadrieril! We also added support for more Rust features in the frontend (dyn Trait), more disciminant informations on ADTs, fixed various bugs, and improved the general experience of using hax....

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....