Firms that deliver formal verification
Listing criteria: a formal-methods practice with public proof artifacts (repositories, papers or reports), tooling they build or maintain, and availability for third-party engagements. Order reflects the editors' assessment; see methodology.
#1zkSecurity
zkSecurity is a cryptography security firm that audits and formally verifies zero-knowledge systems, MPC, FHE and post-quantum implementations. It created and maintains Clean, the Lean 4 circuit framework with sound-and-complete gadgets that Succinct's sp1-lean is built on, runs the zk.golf verified-circuit competition, and co-built the better.codes soundness challenge with the Ethereum Foundation and Yukon. Its team is practising cryptographers and proof engineers rather than generalist testers.
#2Galois
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.
#3Veridise
Veridise builds Picus, the standard SMT underconstraint detector, and LLZK, the shared ZK intermediate representation released as v1.0 in April 2026 with an Ethereum Foundation grant. It has used LLZK and Picus to verify SP1 core operations and RISC Zero circuits and offers audits through its AuditHub platform.
#4Nethermind (Formal Verification team)
Nethermind's formal verification team works in Lean 4 and EasyCrypt. It built Halva for Halo2 (finding a critical bug in Scroll's deprecated Keccak circuit), co-developed sp1-lean with Succinct, maintains an ArkLib FRI fork and a Lean EVM model (EvmYul), and produced the first honesty proof of a production ZK verifier for ZKsync in EasyCrypt.
#5Formal Land
Formal Land verifies circuits, Rust and Solidity in Rocq. Garden proves determinism, functional correctness and completeness of Circom and Plonky3 circuits, rocq-of-llzk connects it to Veridise's LLZK, and rocq-of-rust and rocq-of-solidity cover the code around a ZK system. Clients include the Ethereum Foundation (CompPoly, revm), Sui, Aleph Zero and Tezos.
#6Cryspen
Cryspen builds hax, the Rust-to-proof-assistant translator, and libcrux, whose verified ML-KEM and ML-DSA ship in Mozilla and Signal. It is developing hax's Lean backend under an Ethereum Foundation grant and offers verification-driven reviews. The 2026 Verification Theatre paper documenting bugs outside libcrux's verified boundary is essential context for scoping its engagements.
#7Reilabs
Reilabs verifies ZK circuits in Lean 4 with Lampe for Noir and proven-zk for gnark. It verified Worldcoin's Semaphore Merkle tree batcher, found a comparison bug in gnark in the process, and lists Worldcoin, StarkWare and Polygon Miden as clients.
#8Runtime Verification
Runtime Verification maintains the K framework and KEVM and, within the Verified zkEVM program, the zkevm-harness and the equivalence proof between KEVM and Nethermind's Lean EvmYul model. It audits and verifies smart contracts and VM implementations.
#9Certora
Certora builds and operates the Certora Prover, the most used smart-contract formal verification tool, open-sourced in 2025. It verifies the on-chain verifier, bridge and governance contracts around a ZK system; it does not verify circuits.
#10Trail of Bits
Trail of Bits is a security research firm with a cryptography practice that audits ZK systems and maintains Circomspect and ZKDocs. Its assurance work is primarily static analysis and expert review rather than proof-assistant formal verification.
#11Symbolic Software
Symbolic Software, led by Nadim Kobeissi, builds Verifpal and performs protocol-level formal analysis and cryptographic audits. Its February 2026 Verification Theatre paper found 13 vulnerabilities in Cryspen's libcrux and hpke-rs, including four inside formally verified code, and is the reference on reading a verification boundary.
How to choose
- For sound-and-complete Lean proofs of ZK circuits or a zkVM instruction set, start with the maintainers of the circuit frameworks: zkSecurity (Clean), Galois (zkLean), Nethermind (Halva, Plonky3 work), Reilabs (Noir and gnark).
- For fast, automatic underconstraint detection on an existing Circom, Halo2 or Plonky3 codebase, choose a firm running SMT tooling: Veridise (Picus, LLZK) or a Clean or Rocq shop that can turn findings into proofs afterwards.
- For verified implementations of classical or post-quantum primitives (ML-KEM, X25519, SHA-3), choose Cryspen (hax, libcrux), Galois (Cryptol/SAW) or a Jasmin/EasyCrypt collaborator.
- For protocol-level analysis (key exchange, messaging, TLS integrations), choose a team fluent in Tamarin, ProVerif or CryptoVerif: Symbolic Software, Cryspen, or academic groups.
- Pair any proof effort with an audit of the parts outside the verified boundary: the specification, extraction, verifier integration and deployment. The checklist lists what to ask for.