Cryptol: an executable specification language for cryptographic algorithms

A specification you can execute

The Cryptol specification language was designed by Galois for the NSA Laboratory for Advanced Cybersecurity Research as a public standard for specifying cryptographic algorithms. That origin is the most important fact about the project, because it explains the design.

The stated purpose is that 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.

That last clause is the point. A specification in most cryptographic workflows is a document, and a document does not fail. It is reviewed, and then the implementation is written, and the two drift apart, and the drift is only found when a test vector from the document and a test vector from the code disagree, usually much later. In Cryptol the specification is the program. You can run it, feed it inputs, and watch it compute.

This release is an interpreter for version 3 of the Cryptol language, and the copyright notice says the version is from 2013 to 2024 Galois, Inc., distributed under a standard three-clause BSD licence.

The implementation is Haskell, and the repository is large enough that the structure tells you how much is in the language front end versus the machinery. The `/cryptol` directory holds the Haskell sources for the front-end `cryptol` executable and the read-eval-print loop, and the `/src` directory holds the Haskell sources for the `cryptol` library, described as the bulk of the implementation. The `/lib` directory is the Cryptol standard library sources, and `/examples` holds Cryptol sources implementing several interesting algorithms.

:check for random testing and :prove for proof

Two commands carry most of the value, and they come from different traditions.

The `:check` command tests predicates written in Cryptol against randomly-generated test vectors, in the style of QuickCheck. You state a predicate that should hold, and the interpreter generates inputs and looks for a counterexample. This is the fast loop, and it is where most of the value per minute of effort sits. A property that fails shows you the inputs that broke it, which is often enough to identify the bug by inspection.

The `:prove` command is the heavier one. It calls out to SMT solvers, such as Yices, Z3 or CVC5, to prove predicates for all possible inputs. Where `:check` samples the input space, `:prove` reasons about it exhaustively.

That distinction is what makes the pair worth having together. Sampling finds bugs fast and cheaply, and it is the tool you run on every change. Proving is expensive and can take a long time, and it is the tool you run before you commit to a specification or before a review. A design where a property is proved holds by construction for every input of the given type, which is a stronger statement than passing a large number of random tests, and it is the kind of statement that matters when the input is an attacker.

The `:sat` command also exists, and the documentation mentions it in the same breath as the default solver configuration. It is the command for asking whether a constraint is satisfiable, which is how you explore what a specification actually permits.

The type system does work too, and that is where a lot of the safety comes from. Cryptol uses Microsoft's Z3 SMT solver by default to solve constraints during type checking, so a type error in a Cryptol program is often a constraint problem rather than a simple mismatch.

Getting Z3 right is most of the installation

The documentation spends more space on Z3 than on anything else, and that tells you where the friction is.

Cryptol uses 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, and the specific version tested in continuous integration can be seen in the linked what4-solvers release.

Z3 binaries are downloaded from the Z3 project's own releases page. If you install Cryptol using Homebrew, the appropriate version of Z3 is installed automatically. If you are on Linux, the package manager for your distribution may include Z3, though sometimes the available versions are somewhat old.

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

There is a specific gotcha for 64-bit Linux users that deserves repeating because the error message misleads. On some 64-bit Linux configurations, 32-bit binaries do not work, which leads to unhelpful error messages like `z3: no such file or directory` even when z3 is clearly present. The fix is either to install 32-bit compatibility packages for your distribution, or to download the `x64` version of Z3.

The Cryptol binaries themselves are simpler. They are available from the GitHub releases page for Mac OS X, Linux and Windows. Mac OS X and Linux binaries come as a tarball you extract anywhere, and Windows binaries come both as tarballs and as `.msi` installer packages which place a shortcut to the Cryptol interpreter in the Start menu. On Mac OS X you can also use Homebrew with `brew update && brew install cryptol`.

There is a Gitpod button in the README as well, which is a reasonable way to try the language without installing Z3 or a Haskell toolchain at all.

Building from source needs GHC, two C libraries and submodules

The source build is documented in a way that assumes you read it, which is fine because the steps are short.

The prerequisites are three recent versions of GHC, which at the time of the documentation were 9.6.7, 9.8.4 and 9.12.2. The easiest way to install an appropriate version of GHC is with ghcup. The repository carries a `cabal.GHC-9.6.7.config`, `cabal.GHC-9.8.4.config` and `cabal.GHC-9.12.2.config` file, so the dependency set is pinned per compiler version rather than left to the solver.

Two supporting non-Haskell libraries are required, and most systems already have them: the GNU Multiple Precision Arithmetic Library (GMP) and ncurses. You also need Z3 installed when running Cryptol.

After a fresh checkout, initialize the git submodules:

git submodule update --init

Then, from the Cryptol source directory, run:

./cry build

That builds Cryptol in place, and there are further targets: `./cry run` to run Cryptol in the current directory, and `./cry test` to run the regression test suite. If you run `cabal v2-install --installdir=DIR` in your source directory after running one of those `./cry` commands, you end up with a binary in `DIR`.

The build environments that are regularly built and tested are macOS 15 on ARM64 and x86-64, Ubuntu 22.04 and Ubuntu 24.04 on x86-64, and Windows Server 2022 on x86-64.

One configuration detail is worth knowing. Cryptol can use several external files to control its operation, and normally the build embeds them into the executable. They can be overridden in two ways: copy the contents of the `lib` directory into `$HOME/.cryptol`, or set the `CRYPTOLPATH` environment variable to name another directory containing those files.

The examples directory is the best documentation

For anyone learning the language, the `examples/` directory is where the learning happens, and the file names describe the scope of what Cryptol covers.

The named algorithms include `AES.cry` and `DEStest.cry`, which together with `AE.cry` cover the symmetric block cipher side, plus `Karatsuba.cry` for a multiplication algorithm and `Cipher.cry` for a general cipher interface. There is a `ChaChaPolyCryptolIETF.md` file, which is a specification in prose rather than code, and a `SuiteB_FFI` directory, which is about calling foreign code. `MiniLock/` is a directory, which suggests a complete protocol implementation rather than a primitive.

The files that are not algorithms are the interesting ones. `props.cry` holds properties, which is what you would feed to `:check` and `:prove`. `maliciousSHA/` is a directory with a name that suggests deliberately broken hash constructions used as test cases, and `builtin_lifting.cry` and `builtins.cry` deal with the language's own type system. `funstuff/` and `append.cry` are about language features rather than cryptography, and `split.cry` and `inflist.cry` are about how Cryptol handles sequences.

Two of the file names point at the deeper design decisions. `param_modules/` and `module_system_example.txt` show the module system, which is how a large specification is split into reusable pieces. `demote.cry` suggests the type system has demotion, a mechanism where a value of a more precise type is used where a less precise one is expected.

The `examples/cryptol-specs` entry points at another repository, which is probably where the shared specifications live, and `examples/contrib/` is where community programs are collected, with the contributing guide asking that programs which would benefit the community be added there by pull request.

What Cryptol is not, and what the cost of using it is

The limitations here are not bugs, they are the price of the guarantees, and they are worth stating before anyone adopts the tool.

The first is that Cryptol is a specification language, not an implementation language. It is not what your production code is written in. The value is in the spec being executable and checkable, and the implementation still has to be written and still has to be verified against the spec, by hand or by other means. The documentation is careful about this, saying a Cryptol reference specification can serve as the formal documentation for a cryptographic module, which is a documentation claim rather than a correctness claim about your shipped code.

The second is the dependency on an SMT solver for ordinary use. Because Z3 is used during type checking, Cryptol is not usable at all without Z3 present and on the PATH. That is a heavier operational dependency than a script that parses a config file, and it is the reason the installation section is longer than the language documentation.

The third is the proof cost. `:prove` calls out to solvers, and the general shape of that is that a hard property can take a long time to discharge or may not discharge at all, and an inconclusive result is a fact you have to interpret rather than a failure you can ignore. The documentation does not give a picture of what proving costs in practice, and that is a genuine gap for someone planning a specification effort.

The alternative approach to the same problem is writing the specification in a general purpose language with property based testing, which is what most teams do. The difference in approach is that Cryptol's type system is built for the shape of cryptographic data, with bitvectors and words and sized integers as first class, so a spec written in Cryptol cannot make a whole class of mistake that a spec in a general purpose language can. The cost is that you learn a new language, you take on the SMT dependency, and you accept that your spec and your implementation are still two things.

A third option is to write the implementation in Cryptol itself, which the language allows and which the interpreter's incremental experimentation is designed to support, and which is what the MiniLock and SuiteB_FFI examples suggest people do. That is a bigger commitment than most teams want for production cryptographic code, but it is a legitimate answer when the specification and the implementation should not be allowed to diverge.

On maintenance, the project is in good shape. The last push was on 2026-10-15, the repository is not archived, and the recent releases are 3.4.0 in November 2025, 3.5.0 in January 2026 and 3.6.0 in September 2026. The licence is BSD-3-Clause.

Editorial conclusion

Cryptol fits a team that writes or reviews cryptographic algorithms and wants the specification to be executable, because the same text serves as the formal documentation and as a program you can test, and because `:check` and `:prove` catch a class of mistake that prose cannot. Skip it if your work is ordinary application code, since the type system and the SMT dependencies are a lot of machinery for a hash function call. Before you start, install Z3 and put it on your PATH, since Cryptol uses it during type checking and for `:sat` and `:prove`, and check the version, because Cryptol generally requires the most recent Z3. The last push was on 2026-10-15 with version 3.6.0 released on 2026-09-09.

Frequently asked questions

Official sources

1. GaloisInc/cryptol on GitHub
2. License: BSD-3-Clause
3. Project website
4. README
5. Releases