Cryptol binaries for Mac OS X, Linux, and Windows are available from the GitHub releases page. Binaries are distributed as a tarballs which you can extract to a location of your choice. The 3.1.0 release also includes optional downloads including supported versions of several solvers.
Cryptol is also packaged using Docker and can be fetched using one of the following commands (for the REPL and RPC server, respectively):
docker pull ghcr.io/galoisinc/cryptol:3.1.0
docker pull ghcr.io/galoisinc/cryptol-remote-api:3.1.0
Cryptol currently depends on the
Z3 SMT solver to solve constraints during
typechecking, and as the default solver for the
commands. You can download Z3 binaries for a variety of platforms
from their releases page.
Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking here.
Cryptol also integrates with the Yices, Boolector, CVC4, CVC5, and other SMT
solvers. If you download and install them, you can select which one
Cryptol uses as follows:
:set prover=yices, etc.
For a list of currently-supported solvers, see the solvers we use in
and the SBV versions page.
Cryptol is licensed under a standard 3-clause BSD license.