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:
- The Quick start chapter explains how to go from a simple Rust crate to an F* extraction via hax, including how to install the tooling.
- The Tutorial chapter goes more in-depth into using hax and F* together to prove various properties of Rust code.
- The FAQ chapter is a work in progress but is intended to answer pragmatically and with examples to precise common issues or questions. Feel free to open an issue on the book repository if you feel like a topic should be addressed!
We also added several examples of Rust verification via hax and F* in the example directory of hax, please check them out!