Paper 2025/142 Original: eprint.iacr.org/2025/142 ↗

hax: Verifying Security-Critical Rust Software using Multiple Provers

Abstract

We present hax, a verification toolchain for Rust targeted at security-critical software such as cryptographic libraries, protocol imple- mentations, authentication and authorization mechanisms, and parsing and sanitization code. The key idea behind hax is the pragmatic observation that different verification tools are better at handling different kinds of verification goals. Consequently, hax supports multiple proof backends, including domain-specific security analysis tools like ProVerif and SSProve, as well as general proof assistants like Coq and F*. In this paper, we present the hax toolchain and show how we use it to translate Rust code to the input languages of different provers. We describe how we systematically test our translated models and our models of the Rust system libraries to gain confidence in their correctness. Finally, we briefly overview various ongoing verification projects that rely on hax.