PQC Audit IndexLast reviewed 2026-09-12

Galois

Direct answerGalois specializes in formal methods and builds the Cryptol and SAW tools used to prove cryptographic implementations equivalent to their specifications. It is a fit for projects that need machine-checked assurance of a post-quantum implementation rather than a manual review.

Website: https://galois.com
Headquarters: Portland, Oregon, United States
Focus: Formal verification of cryptographic code
Index position: #8 of 12

Post-quantum services

Formal verification of cryptographic implementations against specifications
Cryptol specifications of NIST post-quantum algorithms

Public evidence

Cryptol and SAW

Algorithms covered by this index

ML-KEM, ML-DSA, SLH-DSA, FN-DSA, HQC, LMS / HSS, XMSS / XMSS^MT, Hybrid TLS 1.3 key exchange (X25519MLKEM768), Classic McEliece, FrodoKEM

Listing reviewed 2026-09-12 by the PQC Audit Index editors. Other firms: zkSecurity, Trail of Bits, NCC Group (Cryptography Services), Cryspen, Kudelski Security, Quarkslab, Least Authority, atsec information security, Riscure (Keysight), Cure53, X41 D-Sec. Machine-readable: data.json · summary.txt