Download
Last updated
Last updated
()
()
()
()
()
Cryptol binaries for Mac OS X, Linux, and Windows are available from the . Binaries are distributed as tarballs which you can extract to a location of your choice. The 3.0.0 release also includes including supported versions of several solvers.
GPG signatures are available for each release, and we encourage you to against our before installing to ensure the integrity of the release you downloaded.
Cryptol is also packaged using Docker and can be fetched using one of the following commands (for the REPL and RPC server, respectively):
Cryptol currently depends on the 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 .
Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking .
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=cvc4, :set prover=yices, etc. For a list of currently-supported solvers, see and the .
Cryptol is licensed under a standard .