We have been developing the hax toolchain over the last two years, in collaboration with research teams at Inria and the University of Aarhus. To showcase its capabilities we have successfully applied it to ML-KEM and Bertie. Others are using it to create new ground-breaking research results.

Key benefits of using hax:

• Uncover potential bugs and vulnerabilities early: Hax’s rigorous formal analysis can identify potential errors and security flaws before they reach production, saving you time and resources.
• Reduce development time and costs: By formally verifying 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.

Today, we’re announcing a collaboration with SandboxAQ to help them verify their software using hax. We are excited to see what new applications we come up with together and how we can evolve hax to be directly usable by software engineers. Read SandboxAQ’s post on the collaboration here.

This collaboration marks a significant step towards making hax accessible to a wider audience and transforming it into a valuable tool for software architects, engineers, and crypto experts. We are excited to share more details about our joint endeavors in the coming months. Stay tuned for updates and insights!

If this peaked your interest and you want to learn more about high assurance software and what Cryspen and tools like hax can do for you, reach out!