SAW turns a formal specification into a proof obligation your compiler cannot check

What SAW actually reasons about

SAW provides the ability to reason about formal models describing the denotation of programs written in languages such as C, Java, Rust, and Cryptol.

That sentence is the whole scope of the project, and each phrase in it is load-bearing. The subject is formal models, not source code. The models describe the denotation of programs, which is the meaning of what a program computes rather than the program text itself. And the target languages are listed, which tells you that the input to SAW is a program and the output is a proof about it.

So SAW is a proof assistant specialised for software, rather than a general theorem prover or a verifier for one language. The user writes a specification of what a function should compute, SAW translates both the specification and the program into a common intermediate representation, and a solver discharges the resulting proof obligations.

The languages named are the interesting part, because they are not arbitrary. Cryptol is a specification language for hardware, and its presence explains the rest of the project. SAW's design is that a Cryptol specification of a cryptographic primitive can be compared against an implementation in C, Java or Rust, and the difference between them is discharged by the solver rather than asserted by the reviewer.

The primary language of the implementation is Haskell, and the repository is saw-script, which is named after SAWScript, the scripting language that serves as the primary user interface to SAW. The README notes the repository is named after it for historical reasons, which is a small indication of how old the arrangement is.

The examples directory makes the intended workload visible. There are aes, chacha20, salsa20, simon-speck and zuc, which are block ciphers and stream ciphers, along with openssl_aes and ecdsa, plus allsat which is an all-satisfiability example, and a set of directories that are about the mechanics rather than the mathematics: partial-spec, multi-override, global_based_override, fresh-post, sequential_aigs and ghost.

A cryptographic verification suite, plus the tooling directories for partial specifications and ghost state, tells you this is a research and verification tool for cryptographic implementations rather than a general code analyser.

SAWScript is the interface, and the interpreter is the product

SAWScript is the scripting language that serves as the primary user interface to SAW, and the documentation is organised around it.

There are two tutorials. One gives an introduction to verifying C code using LLVM and Java code using the JVM. The other gives an introduction to verifying Rust code using MIR. There is also a longer manual that describes the breadth of SAW's features.

The division into three languages by front end tells you the architecture. SAW has a front end per source language, LLVM for C and others, the JVM for Java, and MIR for Rust, and each produces something SAW can reason about. What SAW does with that is language independent, and SAWScript is how you drive it.

The repository layout confirms the split at a finer grain. There are separate front end packages: saw-core-isabelle and saw-core-rocq for the proof assistants, saw-core-sbv for the SMT-related core and saw-core-aig for the AIG core, saw-core-what4 as the term language core, and then the cross-cutting pieces: saw-core, saw-script, saw-support, saw-tools, saw-central, saw-version, saw-python, saw-remote-api and saw-server. There is also cryptol-saw-core, which is the bridge to Cryptol specifications.

The presence of saw-remote-api and saw-server alongside the local components is worth noting, because it means the tool is not purely a single-machine batch program. There is a server component and a remote API, which is what you would need to drive SAW from something else or to keep a session alive.

The examples directory also shows the two ways you can specify behaviour. A partial-spec directory and a multi-override and global_based_override pair suggest that you can state a property once and then specialise it, and a ghost directory suggests the usual technique of adding state to a model that is not present in the implementation. These are all research-grade features, and their presence is a good signal about who the tool is for.

The build is the first real obstacle

The README's installation instructions are unusually detailed, and that detail is itself a signal about what adopting SAW involves.

The system requirements come first. You need the C libraries and header files for terminfo, which generally comes as part of ncurses on most platforms, and on Fedora it is part of the ncurses-compat-libs package. You also need the C headers and libraries for zlib. Some platforms split library packages into runtime and development portions, and you need the development packages.

Then the Haskell toolchain. You need the cabal and ghc executables on your PATH, and the README recommends ghcup to install them if you do not have them. It recommends Cabal 3.10 or newer, and GHC 9.4, 9.6 or 9.8. You may need additional system packages, most likely gmp and perl.

The repository ships version freeze files for each supported compiler, cabal.GHC-9.4.8.config, cabal.GHC-9.6.7.config and cabal.GHC-9.8.4.config, and the freeze file is selected with a symlink:

        ln -s cabal.<ghc version>.config cabal.project.freeze

And then the build itself, which is a script and not a cabal invocation:

        ./build.sh

The README is explicit about this. Note that running `cabal build` or `cabal install` directly will not work. The executables end up in the bin directory, and you can optionally run `./stage.sh` to create a binary tarball.

That last point is the one to plan around. A Haskell project where the documented build is a wrapper script means the script encodes the flag combinations, the package set and the environment the project expects, and building it yourself by other means is not supported. If you are integrating SAW into a reproducible build, that wrapper is part of the contract.

There is also the submodule step, which the README warns you about. After cloning, you need to clone the submodules too, and the instruction is to run git submodule update --init. The commonly used --recursive option is not required, and also not recommended, as it results in cloning a considerable number of additional unused subtrees.

Z3 is mandatory, and the version matters

SAW can use many theorem provers, but because of its use of Cryptol it always needs to have Microsoft Research's Z3 SMT solver installed.

That is the sentence to notice. Other solvers are optional, Z3 is not, and the reason is architectural rather than a preference. Cryptol specifications are bit-precise, and the symbolic bit-vector reasoning SAW performs on them needs an SMT solver that handles bit-vector theory, which Z3 provides and which the solver interface is built around.

The README recommends Z3 4.8.10. That is an old pin for a tool whose releases in the repository listing run to v1.6 in September 2026, and pinning an old solver is the kind of thing that can surprise you. The README also says you can download binaries for Z3 and other solvers from the what4-solvers package, which is Galois's own distribution of solver binaries, so you have a source that matches what the tool was tested against.

Path satisfiability checking has an extra requirement. If you plan to use it, you will also need Yices version 2.6.1 or newer. Path satisfiability is the technique for asking whether some execution path can lead to a bad state, which is how you express security properties like the absence of a timing side channel, and it is the kind of analysis that is the reason to reach for a formal tool rather than a fuzzer.

After installation, the requirement is simply that z3, or z3.exe on Windows, is on your PATH. That is a hard dependency with no fallback, so a SAW installation on a machine without Z3 does not run at all.

The one thing the README does not tell you is which other solvers SAW can use. It says it can use many theorem provers, and mentions Yices for path satisfiability, and the presence of saw-core-isabelle and saw-core-rocq in the repository layout shows that the Isabelle and Rocq proof assistants are integrated as well. The full set is in the user manual.

The Rust path has a schema contract, and that is where it bites

SAW also has support for analyzing Rust programs, based on the MIR intermediate representation, and the mechanism has a wrinkle that the other two language front ends do not have.

To analyse Rust you compile the code using mir-json, a tool which compiles Rust code to a machine-readable, JSON-based format. A copy of mir-json is bundled with SAW as a git submodule, and for best results you should always use that version of it.

Then comes the contract. Sometimes as mir-json evolves, its output format changes, and these changes are captured in a schema version. SAW and mir-json must agree on the schema version. So far, backwards compatibility with old schema versions has proven impractical.

That sentence has real consequences. It means the Rust front end is version-locked in two directions: SAW must be paired with a mir-json that speaks the same schema, and mir-json itself is a Rust compiler plugin that works with a specific version of the Rust compiler. So a Rust user of SAW is pinned to a specific compiler version, a specific mir-json commit, and a matching SAW release.

The README gives the failure mode and the remedy. If after updating SAW, preexisting JSON output files no longer load because of a schema version mismatch, recompile them with the corresponding updated version of mir-json. In other words, the artefacts are not durable across upgrades, and you have to keep the toolchain in step.

There is also an environment variable to set. The mir-json installation instructions tell you to set the SAW_RUST_LIBRARY_PATH environment variable to point at the compiled standard libraries, and SAW uses this variable to find them. It must be set to use the Rust verification subsystem, so a Rust verification job needs the environment set up as well as the binaries installed.

The current schema version supported is 13, according to the README's link to the mir-json schema changelog.

Where SAW is the wrong tool

The first limitation is the division of labour with the solver. SAW does not check your code, it discharges obligations you have given it. If you have no formal specification, SAW has nothing to prove, and what you actually want is type checking, a linter, property based testing or a fuzzer. Those are different tools with different cost curves, and a formal tool applied to code without a specification is a large investment with no output.

The second limitation is that the specification is the expensive part. The examples directory shows partial-spec and ghost directories, which tell you that partial specifications and ghost state are supported techniques, and both are techniques for managing the fact that writing a full specification of a real function is a lot of work. The tooling is there to help, but the effort does not go away.

The third is the build. This is a Haskell project with a pinned GHC and Cabal range, a required wrapper script, three language front ends with their own toolchains, a bundled compiler plugin for Rust and a mandatory external solver. For a research group with a CI setup already provisioned for it, that is fine. For a team that wants to add a proof check to an existing build, the operational surface is large, and the README's own warning that cabal build will not work means you are depending on the project's build script rather than on the ecosystem's normal entry point.

The alternative to weigh is the language-specific verification tools. For C, a combination of a compiler with sanitizers and a fuzzer covers a lot of what a formal proof would find, at a fraction of the setup cost, though it cannot prove the absence of a bug. For Rust, the Rust type system and the Miri interpreter cover memory safety without a specification. The difference in approach is that SAW establishes properties that hold for all inputs by construction, while testing and fuzzing establish that a bug does or does not appear in the cases you tried. If the property is something like constant-time behaviour of a cipher, a sanitizer cannot help you at all and SAW is the only kind of tool on the list that can answer it.

There is also the option of proving in Cryptol and stopping there, which the project structure supports, since cryptol-saw-core is a first-class component. If your requirement is a specification you can inspect and trust rather than a proof about a specific implementation, a Cryptol model with SAW's testing machinery may be the whole job.

Precompiled binaries, Docker, and where the project stands

There are three ways to get SAW, and the README lists them in order of convenience.

Precompiled binaries for a variety of platforms are on the releases page. Alternatively there is a Docker image available from the packages page. And for everything else there is the source build described above.

The Docker route is worth a second look for CI, because it removes both the Haskell toolchain and the Z3 installation from the problem. The image is published under the Galois organization packages, which is a GitHub Container Registry package rather than a Docker Hub one, so pulling it requires a registry login in some setups.

The releases themselves carry a source tarball, and starting with SAW 1.4 there is a specific file to get. You need saw-<release>-sources.tar.gz and not the default GitHub-generated file v<release>.tar.gz. The latter does not include SAW's submodules and is, alas, therefore unbuildable. The README attributes this to a GitHub problem and notes there is no sign of it being likely to get fixed. For releases prior to 1.4, the recommended route is to clone the repository and check out the release tag, such as v1.3.

That is an unusual amount of warning for a release download, and it is the kind of detail that tells you the maintainers have been bitten by it.

The release history shows v1.6 on 2026-09-17, v1.5.1 on 2026-05-22 and v1.5 in February 2026. The last push was on 2026-10-20 and the repository is not archived, so the project is being actively worked on.

The repository also carries the artefacts of a large formal methods project. There is a CHANGES.md, a CODE_OF_CONDUCT.md, a CONTRIBUTING.md, a Makefile that generates Emacs tags, a compute-coverage.sh script and a jenkins-junit-munge.xsl file, which suggests a test and coverage process that predates the GitHub Actions workflows in .github/. There are intTests/, otherTests/ and s2nTests/ directories, and the s2nTests one refers to Amazon's s2n TLS library, so there is integration testing against a real production TLS stack. There are also directories for the other language front ends, crucible-mir-comp/ for the Rust path and crux-mir-comp/ alongside it.

The licence is BSD-3-Clause, which is a permissive grant with no copyleft obligation on code you build with it. That is a licensing note rather than legal advice, and it is worth noting that the licence covers the tool, not the specifications you write with it.

Editorial conclusion

Adopt SAW if you are verifying cryptographic or security-critical code against a formal specification and want a single tool across C, Java and Rust rather than three separate verification stacks. Do not adopt it if you need type checking or property testing, since SAW sits above those and expects you to write the specification yourself. Verify first that your Z3 version is one SAW supports, since it recommends 4.8.10, and that your Rust code compiles with the bundled mir-json so the schema versions match.

Frequently asked questions

Official sources

1. GaloisInc/saw-script on GitHub
2. License: BSD-3-Clause
3. Project website
4. README
5. Releases