Galois Releases New Versions of Verification Tools Cryptol, Crux, and SAW
Galois this week announced the release of Cryptol 3.0.0, Crux 0.7, and SAW 1.0. This significant update brings extensive overhauls and new features—an exciting leap forward for our core verification tools.
Cryptol, a language for writing and specifying cryptographic algorithms, now sports a significantly more expressive module system, declarations that may use numeric constraint guards, and a foreign function interface which allows Cryptol to call functions written in C.
Crux, a tool for verifying programs with inline specifications, offers expanded solver compatibility, support for abduction using CVC5, and enhanced LLVM support.
SAW, a tool for constructing mathematical models of computational behavior and validating their properties, now implements Heapster, which enables extracting functional specifications of memory-safe C programs to Coq; and includes new commands for dealing with C union types, experimental loop verification capabilities, and more.
With these feature-packed new releases, we are leading the charge in advancing cryptographic processes, program verification, and computational modeling.
Binary distributions, source distributions, and more detailed changelogs can be downloaded from the links below: