Cryptol and SAW: Specifications in Cryptol, equivalence proofs of C, LLVM, Java and x86 in SAW
================================================================================

Cryptol is a specification language for cryptographic algorithms and SAW proves that C, LLVM, Java or x86 implementations match those specifications. Galois has used the pair on AWS s2n and AWS-LC (with NSym for AArch64), the BLST BLS library, Apple corecrypto and Stellar's Soroban.

Maintainer: Galois
Website: https://github.com/GaloisInc/saw-script
Category: Verified implementations
Targets: C / LLVM, Java, x86-64, AWS-LC and s2n, BLST, Soroban (Formal Verso)
Approach: Executable specifications in Cryptol; SAW proves implementations equivalent via SMT and symbolic simulation
Access: Open source (BSD-3)
Status: Active (SAW 1.4, Cryptol 3.4 in 2025)
Strengths: Verifies existing optimised code. | Deep industrial track record (AWS, Apple). | Executable specs double as test oracles.
Limits: SMT-bounded reasoning; loops and large state need care. | Specification effort in Cryptol. | Not a circuit tool (Galois's zkLean covers that).
Firms using it: Galois
Sources: https://github.com/GaloisInc/saw-script | https://tools.galois.com/cryptol | https://github.com/awslabs/aws-lc-verification

Source page: https://sorryfree.com/frameworks/cryptol-saw/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13