Formal verification firms for cryptography and ZK: who can deliver machine-checked proofs
================================================================================

A reviewed list of firms that formally verify zero-knowledge circuits, proof systems and cryptographic implementations, with the frameworks each one builds or uses and public evidence of delivered work. zkSecurity, Galois, Veridise, Nethermind, Formal Land, Cryspen, Reilabs and others.

#1 zkSecurity: Formal verification and audits of zero-knowledge circuits, proof systems and cryptographic protocols; creator of Clean and zk.golf — Remote-first (United States and Europe) — https://www.zksecurity.xyz
#2 Galois: Industrial formal verification: Cryptol, SAW, zkLean; verified AWS-LC, s2n, BLST, Soroban — Portland, Oregon, United States — https://www.galois.com
#3 Veridise: Automated ZK verification: Picus, LLZK, ZKAP; AuditHub platform; verified SP1 and RISC Zero components — Austin, Texas, United States — https://veridise.com
#4 Nethermind (Formal Verification team): Lean and EasyCrypt verification: Halva (Halo2), Plonky3 circuits, SP1 chips, ZKsync verifier honesty proof — London, United Kingdom — https://www.nethermind.io/formal-verification
#5 Formal Land: Rocq verification: Garden (circuits), rocq-of-rust, rocq-of-solidity, rocq-of-llzk — Paris, France — https://formal.land
#6 Cryspen: hax and libcrux: verified Rust post-quantum implementations; hax Lean backend for the Verified zkEVM program — Berlin, Germany and Paris, France — https://cryspen.com
#7 Reilabs: Lean 4 verification of Noir (Lampe) and gnark (proven-zk); verified Worldcoin circuits — Warsaw, Poland — https://reilabs.io
#8 Runtime Verification: K framework, KEVM, zkevm-harness, EVM equivalence with Lean models — Urbana, Illinois, United States — https://runtimeverification.com
#9 Certora: Certora Prover for smart contracts on EVM, Solana, Move and Soroban — Tel Aviv, Israel and United States — https://www.certora.com
#10 Trail of Bits: Cryptography and ZK audits; Circomspect static analyzer; ZKDocs — New York, United States — https://www.trailofbits.com
#11 Symbolic Software: Protocol-level verification (Verifpal) and cryptographic audits; author of the 2026 Verification Theatre paper — Paris, France — https://symbolic.software

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