Galois
Direct answerGalois 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
- Founded
- 1999
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
Frameworks this firm builds or uses
Cryptol and SAW, zkLean, LLZK, Lean 4 and Mathlib.
Public evidence
Best fit
Choose Galois for verifying an existing optimised C or assembly library against a specification, or for lookup-centric ZK systems in zkLean.
Other firms on this index
zkSecurity, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software