cryptol ☆
« Back to VersTracker
Description:
Domain-specific language for specifying cryptographic algorithms
Type: Formula  |  Latest Version: 3.4.0@0  |  Tracked Since: Dec 17, 2025
Links: Homepage  |  formulae.brew.sh
Category: Security
Tags: cryptography verification dsl formal-methods security
Install: brew install cryptol
About:
Cryptol is a domain-specific language designed for specifying and implementing cryptographic algorithms. It allows developers to write high-level, verifiable descriptions of cryptographic primitives, which can then be simulated, tested, and even extracted into languages like C or Haskell. Its primary value is in reducing implementation errors and formally verifying the correctness of cryptographic designs.
Key Features:
  • Type-safe language for cryptographic specifications
  • Automatic test case generation
  • Support for formal verification and equivalence checking
  • Code extraction to C and Haskell
Use Cases:
  • Designing and prototyping new cryptographic algorithms
  • Verifying the correctness of existing cryptographic implementations
  • Generating test vectors for cryptographic libraries
Alternatives:
  • SAW – SAW (Software Analysis Workbench) is used for verifying existing code, while Cryptol is used for specifying algorithms from scratch.
  • F* – F* is a general-purpose language for verification, whereas Cryptol is specialized for the cryptographic domain.
License: BSD-3-Clause
Dependencies: gmp, z3
Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, sonoma, arm64_linux, x86_64_linux
Version History
Detected Version Rev Change Commit
Nov 21, 2025 10:01pm 0 VERSION_BUMP 23c9f761
Jan 5, 2025 5:40pm 0 VERSION_BUMP f2379dbc
« Back to VersTracker  |  Browse Packages  |  About