Cryptol 2.9

Cryptol by Galois is an open-source, domain-specific, functional language and toolchain for designing, implementing, testing, and formally verifying cryptographic algorithms. Centered on bit-precise, mathematically rigorous types and sequences, it enables clear, executable specifications that eliminate ambiguity. With an interactive REPL and automated reasoning back ends, Cryptol lets you generate test vectors, check properties, find counterexamples, and establish equivalence between algorithm variants or against reference specifications.

Key capabilities:

• Bit-precise, strongly typed DSL tailored to cryptography (e.g., modular arithmetic, finite fields, and sequence operations)
• Property-based testing and solver-backed verification with automatic counterexample discovery
• Equivalence checking for algorithm refinements and implementation validation
• Interoperability with the SAW tool to connect specifications to implementations in common languages (such as C, Java, and LLVM bitcode) for end-to-end verification
• Cross-platform command-line tooling and an interactive environment for rapid iteration
• A rich standard library covering common cryptographic building blocks

Cryptol is well suited for cryptographers, security engineers, and assurance teams who need high-confidence specifications, reproducible test vectors, and rigorous proofs of correctness for software or hardware implementations.

Cryptol is developed by Galois. The most popular versions of this product among our users are: 2.1, 2.2, 2.4, 2.7 and 2.9. The name of the program executable file is cryptol.exe.