Galois: formal verification services for cryptography and ZK
============================================================

Galois is a formal-methods research and engineering firm that builds Cryptol, SAW and zkLean and has delivered verification of AWS-LC and s2n (with NSym for AArch64), the BLST BLS library, Stellar's Soroban (Formal Verso) and Halo2 recursion work with IOG. Its zkLean framework is funded by the Ethereum Foundation.

Website: https://www.galois.com
Headquarters: Portland, Oregon, United States
Focus: Industrial formal verification: Cryptol, SAW, zkLean; verified AWS-LC, s2n, BLST, Soroban
Index position: #2 of 11
Services: Implementation verification of C, assembly and Rust cryptography with Cryptol and SAW | ZK circuit verification in Lean with zkLean, including Jolt-style lookup systems | Long-horizon research contracts (DARPA, AWS) in high-assurance cryptography
Tools: Cryptol and SAW, zkLean, LLZK, Lean 4 and Mathlib
Evidence: https://github.com/awslabs/aws-lc-verification | https://github.com/GaloisInc/zk-lean | https://github.com/GaloisInc/saw-script

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