cryptol

[![Cryptol](https://github.com/GaloisInc/cryptol/workflows/Cryptol/badge.svg)](https://github.com/GaloisInc/cryptol/actions?query=workflow%3ACryptol)
[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/GaloisInc/cryptol)


# Cryptol, version 3

    This version of Cryptol is (C) 2013-2024 Galois, Inc., and
    distributed under a standard, three-clause BSD license. Please see
    the file LICENSE, distributed with this software, for specific
    terms and conditions.

# What is Cryptol?

The Cryptol specification language was designed by Galois for the NSA
Laboratory for Advanced Cybersecurity Research as a public standard for
specifying cryptographic algorithms. A Cryptol reference specification
can serve as the formal documentation for a cryptographic module.
Unlike current specification mechanisms, Cryptol is fully executable,
allowing designers to experiment with their programs incrementally as
their designs evolve.

This release is an interpreter for version 3 of the Cryptol
language. The interpreter includes a `:check` command, which tests
predicates written in Cryptol against randomly-generated test vectors
(in the style of
[QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is
also a `:prove` command, which calls out to SMT solvers, such as
Yices, Z3, or CVC5, to prove predicates for all possible inputs.

# Getting Cryptol Binaries

Cryptol binaries for Mac OS X, Linux, and Windows are available from the
GitHub [releases page](https://github.com/GaloisInc/cryptol/releases).
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
both as tarballs and as `.msi` installer packages which place a shortcut
to the Cryptol interpreter in the Start menu.

On Mac OS X, Cryptol is also available via
[Homebrew](http://brew.sh/). Simply run `brew update && brew install cryptol`
to get the latest stable version.

## Getting Z3

Cryptol currently uses Microsoft Research's [Z3 SMT
solver](https://github.com/Z3Prover/z3) by default to solve constraints
during type checking, and as the default solver for the `:sat` and
`:prove` commands.  Cryptol generally requires the most recent version
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20260622).

You can download Z3 binaries for a variety of platforms from their
[releases page](https://github.com/Z3Prover/z3/releases). If you
install Cryptol using Homebrew, the appropriate version of Z3 will be
installed automatically. If you're using Linux, the package manager for
your distribution may include Z3, as well, though sometimes the
available versions are somewhat old.

After installation, make sure that `z3` (or `z3.exe` on Windows)
is on your PATH.

### Note for 64-bit Linux Users

On some 64-bit Linux configurations, 32-bit binaries do not work. This
can lead to unhe