Tutorial

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! New resources to learn more about hax The hax book has three new chapters: ...