Galois Releases SAW 1.5 and Cryptol 3.5.0

Galois has released updated versions of the Software Analysis Workbench (SAW) and Cryptol.

SAW 1.5

This release of SAW — our semi-automated tool for formally verifying code written in Rust, C, SPARK, Java, and Cryptol — brings Rust (MIR) verification out of experimental status, along with numerous improvements to scripting ergonomics and language consistency. LLVM versions up to 20 are now supported as well.

SAW now supports verifying Rust versions up to 1.91, and includes new capabilities like mir_extract for extracting MIR functions to terms and mir_find_name for locating instantiations of polymorphic functions.

Improved Consistency and Developer Ergonomics

This release brings verification commands into alignment across all supported languages. mir_verify now enforces the same correctness checks as llvm_verify and jvm_verify, including requirements for mir_return statements on non-void functions.

Housekeeping

Deprecated Heapster, MRSolver, and Monadify features have been removed. The Coq-related commands have been renamed to reflect the Rocq rebranding (e.g., write_coq_term → write_rocq_term), with old names remaining available but deprecated.

See the full changelog for complete details, binary distributions, and source.

Cryptol 3.5.0

In the 3.5.0 release of Cryptol – our tool for writing formal specifications of cryptographic algorithms – user-defined newtype and enum types can now derive instances for standard constraints like Eq and Cmp. This means you can use standard operations like == with your custom types. In addition, the default behavior of -p/--project has been changed to check all files not previously verified in addition to files that have changed since the last run.