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. Windows binaries are distributed as an
.msi installer package which places a shortcut to the Cryptol interpreter in the Start menu.
Cryptol currently depends on the Z3 SMT solver to solve constraints during typechecking, and as the default solver for the
:prove commands. You can download Z3 binaries for a variety of platforms from their releases page.
Cryptol also integrates with the Yices, CVC4, 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 SBV versions page.
Cryptol is licensed under a standard 3-clause BSD license.