Cryptol and SAW
Direct answerCryptol 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
- Repository
- https://github.com/GaloisInc/saw-script
- Category
- Verified implementations
- Targets
- C / LLVMJavax86-64AWS-LC and s2nBLSTSoroban (Formal Verso)
- Approach
- Executable specifications in Cryptol; SAW proves implementations equivalent via SMT and symbolic simulation
- Access
- Open source (BSD-3)
- Status (2026-09-13)
- Active (SAW 1.4, Cryptol 3.4 in 2025)
What Cryptol and SAW does
SAW is the workhorse of industrial cryptographic verification in the United States. Its equivalence-checking style suits hand-optimised code that already exists; you write the spec, not the code.
Where it is strong
- Verifies existing optimised code.
- Deep industrial track record (AWS, Apple).
- Executable specs double as test oracles.
Limits and caveats
- SMT-bounded reasoning; loops and large state need care.
- Specification effort in Cryptol.
- Not a circuit tool (Galois's zkLean covers that).
When to choose it
Choose Cryptol/SAW to verify existing C or assembly primitives against a spec, particularly in AWS-style environments.
Who works with Cryptol and SAW
Top-listed for implementation verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in Verified implementations
Jasmin and libjade, hax, Fiat-Crypto, HACL*, Vale and EverCrypt, Aeneas, Kani, CBMC, CryptoLine, Verus.