Getting Cryptol

Download a Binary

Linux (Ubuntu) macOS Windows

Cryptol binaries for Mac OS X, Linux, and Windows are available from the GitHub releases page. Mac OS X and Linux binaries are distributed as a tarball which you can extract to a location of your choice. A Windows .msi installer package also exists, and will place a shortcut to the Cryptol interpreter in the Start menu.

GPG signatures are available for each release, and we encourage you to check the signature against our public key before installing to ensure the integrity of the release you downloaded.

Cryptol is also available on DockerHub and can be fetched using one of the following commands (for the REPL and RPC server, respectively):

docker pull galoisinc/cryptol:2.10.0

docker pull galoisinc/cryptol-remote-api:2.10.0

Getting Z3

Download Z3

Cryptol currently depends on the Z3 SMT solver to solve constraints during typechecking, and as the default solver for the :sat and :prove commands. You can download Z3 binaries for a variety of platforms from their releases page.

Getting other SMT solvers

Cryptol also integrates with the Yices, Boolector, CVC4, and other SMT solvers. If you download and install them, you can select which one Cryptol uses as follows: :set prover=cvc4, :set prover=yices, etc. For a list of currently-supported solvers, see the SBV versions page.

Licensing Terms

Cryptol is licensed under a standard 3-clause BSD license.