Galois Releases New Versions of Verification Tools SAW, Cryptol, and Crux

Galois has issued new versions in our suite of verification tools: SAW 1.3, Cryptol 3.3.0, and Crux 0.10. These updates reflect a new push to make these tools more accessible and user-friendly.

SAW 1.3

SAW is our tool for proving equivalences and refinements among different kinds of things – program implementations of multiple kinds and formal models of them. The 1.3 release features ergonomic improvements, including a search ability in the REPL and many improved error messages, as well as support for the bitwuzla solver and numerous bug fixes.

Cryptol 3.3.0

The 3.3.0 release of Cryptol, our tool for writing formal specifications of cryptographic algorithms, adds new features for managing whole projects. It also, like SAW, features many improved error messages, bitwuzla support, and many bug fixes.

Crux 0.10

Crux is our tool for verifying programs with inline specifications. Release 0.10 adds the ability to use the Crucible debugger. It also supports bitwuzla and includes improvements to the handling of both mir-json files and LLVM bitcode files.

‍

Binary distributions, source, and full changelogs can be found here:

• SAW 1.3
• Cryptol 3.3.0
• Crux 0.10