With hax, you can achieve a new level of confidence in the safety and reliability of your software.
Key benefits of Hax:
- Uncover potential bugs and vulnerabilities early: Hax’s rigorous analysis can identify potential errors and security flaws before they reach production, saving you time and resources.
- Reduce development time and costs: By formalizing your code, you can reduce the need for manual testing and reduce the risk of regressions.
- Gain a competitive edge: Demonstrate the high quality and reliability of your software to your customers and partners.
Contact Get in touch when you are interested in using hax.
How does it work
hax is Cryspen’s Rust verification framework. hax is a tool for high assurance translations that translates a large subset of safe Rust into the formal languages accepted by proof assistants such as F* or Coq. Backends for other provers like ProVerif are under construction. A more detailed technical description can be found on the hax blog.
The toolchain supports security analysis and full functional verification of production software. Software engineers, cryptographers, and proof engineers work together to implement the software and formalise critical properties. Once verification is complete, the toolchain guarantees clean, well-documented, deployable code in Rust, C, or WebAssembly. Conversely, if an attack or bug is found, it is presented back to the cryptography or software engineer.
Hax is the basis for the integrated development and verification environment (IDVE) for Rust that is developed together with Inria in the Circus project.
