GET IN TOUCH
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.
Galois Releases New Versions of Verification Tools SAW and Cryptol
Galois has released updated versions of our Software Analysis Workbench (SAW) and Cryptol, including a wide variety of new features, bugfixes, and enhancements.
SAW 1.4
SAW — our semi-automated tool for formally verifying code written in Rust, C, SPARK, Java, and Cryptol — now supports passing arguments to SAW scripts. This is a breaking change, in that options passed after the script name will not be recognized by SAW, and the behavior of the 'get_opt' SAW built-in has changed.
In addition, the ‘crux-mir-comp’ tool, a Crux frontend for MIR, is now included in the binary distribution.
This release also includes myriad developer ergonomic and performance enhancements. Users can refer to our changelog for more details.
Cryptol 3.4.0
The 3.4.0 release of Cryptol, our tool for writing formal specifications of cryptographic algorithms, includes a new prover, w4-rme. This prover works on goals using booleans and bit vectors, and does not call out to an external solver. It's particularly suited to problems using Galois field arithmetic.
The changes mentioned above are not comprehensive. See below for full changelogs, binary distributions, and source.
