# sorryfree

> Formal verification frameworks for zero-knowledge circuits and cryptographic code: what each one proves, what it leaves out, and who can run it for you.

Compiled by the sorryfree editors (sorryfree). Last reviewed 2026-09-13. Every page has a summary.txt and data.json sibling; site-wide JSON at /api/index.json.

## ZK circuit verification

- [Category guide](https://sorryfree.com/categories/zk-circuits/): Frameworks that prove or check that a zero-knowledge circuit (R1CS, PLONKish, AIR, Circom, Noir, Halo2, Cairo) does what its specification says. Proof-assistant frameworks (Clean, zkLean, Halva, sp1-lean, Garden, Lampe) produce machine-checked soundness and sometimes completeness theorems; SMT and static tools (Picus, CIVER, Circomspect, zkFuzz) find underconstrained signals automatically but do not prove absence of bugs.
- [Clean](https://sorryfree.com/frameworks/clean/): Clean is an embedded Lean 4 language for writing zero-knowledge circuits in which every gadget carries a machine-checked proof of both soundness (any satisfying witness meets the specification) and completeness (every valid input has a satisfying witness). Created and maintained by zkSecurity, it targets AIR-style tables with lookups, PLONK and R1CS, composes verified gadgets into larger verified circuits, and since June 2026 models cross-table interactions so that whole multi-table systems such as zkVMs can be proved sound.
- [sp1-lean](https://sorryfree.com/frameworks/sp1-lean/): sp1-lean is Succinct's Lean 4 project, developed with Nethermind, that expresses the constraints of SP1 Hypercube's RISC-V chips in Clean and proves them sound against the Sail RISC-V reference model. As of the Ethereum Foundation's May 2026 review, 51 of 62 opcodes were fully proven; completeness is deferred for five chips.
- [zkLean](https://sorryfree.com/frameworks/zklean/): zkLean is Galois's Lean 4 framework for stating and proving soundness of extracted circuits, with native support for R1CS, lookups, multilinear-extension lookups and RAM in the style of the Jolt zkVM. It ships a SHA-3 example and a Jolt extractor, and is one of the proof backends LLZK lowers to.
- [Halva](https://sorryfree.com/frameworks/halva/): Halva extracts the gate, copy, permutation and lookup constraints of a Halo2 circuit at synthesis time and lets engineers prove soundness in Lean 4. In July 2025 Nethermind used it to find a critical soundness bug in Scroll's deprecated Keccak-256 circuit.
- [Picus](https://sorryfree.com/frameworks/picus/): Picus checks whether every output signal of a circuit is uniquely determined by its inputs, which is the automatic, specification-free way to detect underconstrained circuits. It runs on Circom, R1CS and gnark directly and on Halo2 and Plonky3 through LLZK, and Veridise has used it with LLZK to verify SP1 core operations and RISC Zero circuits.
- [LLZK](https://sorryfree.com/frameworks/llzk/): LLZK is a shared intermediate representation for ZK circuits built on MLIR. Frontends for Circom, Halo2 and Plonky3 (Noir in progress) lower into it, and backends emit Picus queries, zkLean models, R1CS and Rocq via Formal Land's rocq-of-llzk, so one circuit can be checked automatically and then proved.
- [Garden](https://sorryfree.com/frameworks/garden/): Garden is Formal Land's Rocq framework for proving determinism, functional correctness and completeness of circuits written in Circom or Plonky3, and of anything lowered through LLZK via rocq-of-llzk.
- [Lampe](https://sorryfree.com/frameworks/lampe/): Lampe extracts the semantics of Noir programs into Lean 4 so that properties of Aztec-ecosystem circuits can be stated and proved. It is the main proof-assistant route for Noir; NAVe is the automatic alternative.
- [proven-zk and gnark-lean-extractor](https://sorryfree.com/frameworks/proven-zk/): proven-zk is a Lean 4 library, with a companion gnark extractor, used by Reilabs to verify Worldcoin's Semaphore Merkle tree batcher circuits. The work surfaced a comparison bug in gnark itself.
- [CIVER](https://sorryfree.com/frameworks/civer/): CIVER is a verifier built into a fork of the Circom compiler by the team behind Circom's own maintainers' academic group. It checks weak safety (every output determined by inputs), tag specifications and user-written pre- and post-conditions template by template, reusing results bottom-up so large circomlib-style codebases scale.
- [Circomspect](https://sorryfree.com/frameworks/circomspect/): Circomspect is a static analyzer for Circom that flags unconstrained signals, unused or shadowed variables, unsafe `<--` assignments and other patterns behind known circuit bugs. It is a linter, not a verifier: fast, easy to add to CI, and blind to bugs that do not match a pattern.
- [zkFuzz](https://sorryfree.com/frameworks/zkfuzz/): zkFuzz fuzzes Circom programs for disagreements between what witness generation computes and what the constraints enforce, the root of most underconstraint bugs. Its paper reports 66 bugs across 354 circuits.
- [Coda](https://sorryfree.com/frameworks/coda/): Coda is a research language in which circuits carry refinement types; the type checker generates Coq lemmas whose proofs establish functional correctness. Its authors found six bugs in circomlib-derived circuits with it.
- [Ecne](https://sorryfree.com/frameworks/ecne/): Ecne was the first widely used tool for proving that an R1CS constraint set uniquely determines its outputs, the property later automated with SMT by Picus. It remains useful as a lightweight second opinion on small R1CS systems.
- [NAVe](https://sorryfree.com/frameworks/nave/): NAVe checks Noir programs for proper constrainedness using cvc5's finite-field theory, giving the Noir ecosystem an automatic underconstraint detector comparable to Picus for Circom.
- [Verified Cairo AIR (Stone and S-two)](https://sorryfree.com/frameworks/verified-cairo/): StarkWare, with Jeremy Avigad and Yoav Seginer, has proved in Lean 4 that satisfying the Cairo VM's AIR (for both the Stone and S-two provers) implies a correct Cairo execution, and in July 2026 used the same methodology to verify the STRK20 privacy pool with more than 230 theorems.

## Proof systems and computational proofs

- [Category guide](https://sorryfree.com/categories/proof-systems/): Frameworks for machine-checking the cryptographic argument itself: knowledge soundness of a polynomial IOP, the security reduction of a KEM, or the game-hopping proof in a paper. These work in the computational model, where the adversary is a probabilistic polynomial-time algorithm and security is a concrete bound, and they are the only tools on this index that verify the proof system rather than the circuit inside it.
- [ArkLib](https://sorryfree.com/frameworks/arklib/): ArkLib formalizes the building blocks of modern SNARKs in Lean 4: interactive oracle reductions and their composition, sum-check, polynomial commitment schemes, the FRI, STIR and WHIR proximity protocols, Fiat-Shamir and the BCS transform, with completeness and soundness theorems. It is the proof-system half of the Verified zkEVM program.
- [EasyCrypt](https://sorryfree.com/frameworks/easycrypt/): EasyCrypt is the reference tool for machine-checked computational security proofs: game-based reductions expressed over probabilistic programs with a relational Hoare logic. It underpins the verified ML-KEM, X-Wing, SHA-3 and X25519 implementations in libjade, and Nethermind used it for the first honesty proof of a production ZK verifier (ZKsync).
- [CryptoVerif](https://sorryfree.com/frameworks/cryptoverif/): CryptoVerif automates game-hopping proofs in the computational model, producing concrete security bounds for protocols. It has been applied to TLS 1.3, Signal and WireGuard and is the computational counterpart to ProVerif.
- [SSProve](https://sorryfree.com/frameworks/ssprove/): SSProve brings state-separating, modular game-based proofs to Rocq, letting large cryptographic proofs be assembled from packages. hax can target it from Rust, connecting implementations to proofs.
- [ProofFrog](https://sorryfree.com/frameworks/prooffrog/): ProofFrog checks that the game transitions in a provable-security proof are valid, giving paper authors and reviewers a mechanical check on the skeleton of a reduction. It ships an MCP server so AI assistants can drive it.
- [Squirrel](https://sorryfree.com/frameworks/squirrel/): Squirrel proves protocol security in a symbolic-looking logic whose results are computationally sound, bridging the gap between Tamarin-style automation and EasyCrypt-style guarantees.

## Symbolic protocol analysis

- [Category guide](https://sorryfree.com/categories/symbolic-protocols/): Automatic analyzers that model a protocol with perfect (Dolev-Yao) cryptography and search for attacks over unbounded sessions: authentication failures, key-compromise impersonation, downgrade, replay and unknown-key-share. Tamarin and ProVerif are the standard tools; Verifpal trades expressiveness for approachability; DY* embeds the analysis in F* for executable code.
- [Tamarin](https://sorryfree.com/frameworks/tamarin/): Tamarin is the most widely used symbolic protocol verifier for stateful, multi-role protocols. It has analysed TLS 1.3, 5G authentication, WPA2, the Noise framework and EMV, and supports interactive guidance when automation stalls.
- [ProVerif](https://sorryfree.com/frameworks/proverif/): ProVerif automatically analyses protocol models in the applied pi-calculus for secrecy, authentication and equivalence properties over unbounded sessions. It has a large model base and is a target of hax, so Rust implementations can be analysed symbolically.
- [Verifpal](https://sorryfree.com/frameworks/verifpal/): Verifpal is a symbolic protocol analyser designed for engineers rather than formal-methods specialists. Its modelling language is deliberately simple, which limits expressiveness relative to Tamarin and ProVerif but lowers the barrier to a first model.
- [DY*](https://sorryfree.com/frameworks/dystar/): DY* verifies protocol implementations written in F* against symbolic security properties, so the analysed model is the executable code. It has been applied to Signal and ACME and is the successor to ProScript.

## Verified implementations

- [Category guide](https://sorryfree.com/categories/implementations/): Frameworks that prove properties of the code that ships: functional correctness against a specification, memory safety, and constant-time behaviour, for C, Rust, assembly and generated field arithmetic. This is where post-quantum verification happens in practice: ML-KEM and ML-DSA implementations in libjade, libcrux, AWS-LC, mlkem-native and Apple corecrypto all carry machine-checked proofs from tools in this category.
- [Jasmin and libjade](https://sorryfree.com/frameworks/jasmin/): Jasmin is a language and verified compiler for writing cryptographic assembly whose functional correctness is proved in EasyCrypt and whose constant-time behaviour is checked by the compiler. libjade is the resulting library of verified implementations, including ML-KEM with AVX2 rejection sampling, ML-DSA, X-Wing, SHA-3 and X25519.
- [hax](https://sorryfree.com/frameworks/hax/): hax translates a large subset of Rust into F*, Rocq, ProVerif, SSProve and EasyCrypt, with a Lean backend in development. Cryspen used it to verify libcrux's ML-KEM (portable and AVX2 field arithmetic, NTT and serialization) in F*; libcrux ML-KEM ships in Mozilla and Signal.
- [Cryptol and SAW](https://sorryfree.com/frameworks/cryptol-saw/): Cryptol is a specification language for cryptographic algorithms and SAW proves that C, LLVM, Java or x86 implementations match those specifications. Galois has used the pair on AWS s2n and AWS-LC (with NSym for AArch64), the BLST BLS library, Apple corecrypto and Stellar's Soroban.
- [Fiat-Crypto](https://sorryfree.com/frameworks/fiat-crypto/): Fiat-Crypto generates field-arithmetic code (C, Rust, Go, Zig and more) from parameters with a Rocq proof that the output is correct. Its Curve25519 and P-256 code ships in BoringSSL and Go's standard library.
- [HACL*, Vale and EverCrypt](https://sorryfree.com/frameworks/hacl-star/): HACL* is a library of cryptographic primitives verified in F* for memory safety, functional correctness and secret independence, with Vale providing verified assembly and EverCrypt a unified API. Its code runs in Firefox, the Linux kernel, mbedTLS and WireGuard.
- [Aeneas](https://sorryfree.com/frameworks/aeneas/): Aeneas translates Rust into pure functional models for Lean, F* or Rocq through the Charon frontend. A May 2026 pipeline paper used it with hax, ArkLib and CompPoly, plus AI provers, to verify Plonky3 FRI folding and field arithmetic and RISC Zero Merkle checks.
- [Kani](https://sorryfree.com/frameworks/kani/): Kani is AWS's bounded model checker for Rust. It proves absence of panics, undefined behaviour and violated assertions within loop bounds, with no specification language to learn, and is used across AWS's Rust libraries and the Rust standard library verification challenge.
- [CBMC](https://sorryfree.com/frameworks/cbmc/): CBMC is the bounded model checker behind Kani and the memory-safety proofs of mlkem-native and AWS s2n. It proves absence of memory errors and assertion failures in C within loop bounds.
- [CryptoLine](https://sorryfree.com/frameworks/cryptoline/): CryptoLine verifies straight-line arithmetic assembly such as bignum multiplication and NTT butterflies, and has been applied to OpenSSL, BoringSSL, wolfSSL and post-quantum NTT implementations.
- [Verus](https://sorryfree.com/frameworks/verus/): Verus lets developers write specifications and proofs inside Rust and discharges them with an SMT solver, giving full functional correctness without a separate proof assistant.

## Proof assistants and general verifiers

- [Category guide](https://sorryfree.com/categories/provers/): The foundations underneath the specialised frameworks: interactive proof assistants (Lean 4, Rocq, Isabelle/HOL, F*, ACL2), a semantics framework (K), and SMT-based verifiers for smart contracts (Certora Prover, Halmos, hevm). Choosing one fixes the ecosystem, the available libraries, the hiring pool and, increasingly, which AI proving tools can help.
- [Lean 4 and Mathlib](https://sorryfree.com/frameworks/lean4/): Lean 4 is the proof assistant behind nearly every ZK verification project funded in 2025 and 2026: Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, proven-zk, Nethermind's EVM model and StarkWare's Cairo proofs. Mathlib supplies the finite-field and polynomial mathematics, and AI proving tools now target it.
- [Rocq (formerly Coq)](https://sorryfree.com/frameworks/rocq/): Rocq, the renamed Coq, underpins Fiat-Crypto's verified field arithmetic, SSProve's computational proofs, Formal Land's Garden circuit framework and its rocq-of-rust and rocq-of-solidity translators. It is the main alternative to Lean for cryptographic verification.
- [Isabelle/HOL](https://sorryfree.com/frameworks/isabelle/): Isabelle/HOL is the prover Apple used with AutoCorres2, SAW and Cryptol to verify the ML-KEM and ML-DSA implementations in corecrypto (published 2026). It offers strong automation and a refinement methodology for C.
- [F*](https://sorryfree.com/frameworks/fstar/): F* is the dependently typed language in which HACL* and libcrux proofs are written and the primary backend of hax. It combines proof-assistant expressiveness with SMT automation and extracts to C.
- [ACL2 (R1CS and PFCS books)](https://sorryfree.com/frameworks/acl2/): ACL2 has a mature library for R1CS and prime-field constraint systems and an acl2-jolt project. zkSecurity's 2025 comparison found it the lightest on tactic effort among circuit frameworks, at the cost of a smaller ecosystem.
- [K framework and KEVM](https://sorryfree.com/frameworks/k-framework/): K is a semantics framework in which KEVM defines the EVM executably. Runtime Verification uses it in the Verified zkEVM program for the zkevm-harness and for proving equivalence between KEVM and Nethermind's Lean EvmYul model.
- [Certora Prover](https://sorryfree.com/frameworks/certora-prover/): Certora Prover verifies smart contracts against rules written in CVL, on EVM, Solana, Move and Soroban. It is the tool to verify the on-chain verifier and bridge logic around a ZK system; it does not verify circuits.

## Challenges and programs

- [Category guide](https://sorryfree.com/categories/challenges/): Live venues where verified artifacts are produced competitively or under a coordinated program: zk.golf (cheapest circuit with a Lean proof of soundness and completeness), better.codes (raise a Lean-checked soundness bound for Reed-Solomon proximity), and the Ethereum Foundation's Verified zkEVM program that funds most of the frameworks on this index.
- [zk.golf](https://sorryfree.com/frameworks/zk-golf/): zk.golf is zkSecurity's competition to build the cheapest zero-knowledge circuits that are proven correct in Lean 4. Each challenge fixes a Lean specification; a submission is a Clean circuit plus a proof that it is sound and complete against it, kernel-checked in a sandbox (20-minute timeout, no native_decide, axiom allowlist). Challenges include SHA-256, Keccak-f[1600], RSA PKCS#1 v1.5 verification, secp256k1 scalar multiplication and GF(2) BLAKE3 and KangarooTwelve compression.
- [better.codes](https://sorryfree.com/frameworks/better-codes/): better.codes is an open autoresearch challenge built by the Ethereum Foundation Formal Verification team with Yukon and zkSecurity. A self-contained problem from the Proximity Prize (koalaIRS12, a Reed-Solomon proximity question that governs the provable soundness of hash-based SNARKs such as FRI, STIR and WHIR) is formalised in Lean 4, and solvers direct AI agents at raising the proven soundness lower bound. As of 2026-09-13 the bound stood at 68.07 bits against a 128-bit target, up from a 64-bit literature baseline, with 74 promoted submissions from 22 solvers.
- [Verified zkEVM program](https://sorryfree.com/frameworks/verified-zkevm/): The Verified zkEVM program is the Ethereum Foundation initiative that funds and coordinates most of the ZK verification tooling on this index: Clean (zkSecurity), zkLean (Galois), Halva (Nethermind), ArkLib, LLZK (Veridise), the Sail RISC-V Lean model, KEVM equivalence work (Runtime Verification), VCV-io and hax's Lean backend (Cryspen), with a stated goal of formally verified zk(E)VMs by 2027.

## Firms (in index order)
- [zkSecurity](https://sorryfree.com/firms/zksecurity/): Formal verification and audits of zero-knowledge circuits, proof systems and cryptographic protocols; creator of Clean and zk.golf
- [Galois](https://sorryfree.com/firms/galois/): Industrial formal verification: Cryptol, SAW, zkLean; verified AWS-LC, s2n, BLST, Soroban
- [Veridise](https://sorryfree.com/firms/veridise/): Automated ZK verification: Picus, LLZK, ZKAP; AuditHub platform; verified SP1 and RISC Zero components
- [Nethermind (Formal Verification team)](https://sorryfree.com/firms/nethermind/): Lean and EasyCrypt verification: Halva (Halo2), Plonky3 circuits, SP1 chips, ZKsync verifier honesty proof
- [Formal Land](https://sorryfree.com/firms/formal-land/): Rocq verification: Garden (circuits), rocq-of-rust, rocq-of-solidity, rocq-of-llzk
- [Cryspen](https://sorryfree.com/firms/cryspen/): hax and libcrux: verified Rust post-quantum implementations; hax Lean backend for the Verified zkEVM program
- [Reilabs](https://sorryfree.com/firms/reilabs/): Lean 4 verification of Noir (Lampe) and gnark (proven-zk); verified Worldcoin circuits
- [Runtime Verification](https://sorryfree.com/firms/runtime-verification/): K framework, KEVM, zkevm-harness, EVM equivalence with Lean models
- [Certora](https://sorryfree.com/firms/certora/): Certora Prover for smart contracts on EVM, Solana, Move and Soroban
- [Trail of Bits](https://sorryfree.com/firms/trail-of-bits/): Cryptography and ZK audits; Circomspect static analyzer; ZKDocs
- [Symbolic Software](https://sorryfree.com/firms/symbolic-software/): Protocol-level verification (Verifpal) and cryptographic audits; author of the 2026 Verification Theatre paper

## Glossary
- [Circuit soundness](https://sorryfree.com/glossary/circuit-soundness/): A circuit is sound with respect to a specification if every witness that satisfies its constraints also satisfies the specification, so a malicious prover cannot produce an accepting proof of a false statement.
- [Circuit completeness](https://sorryfree.com/glossary/circuit-completeness/): A circuit is complete with respect to a specification if every input the specification allows has a satisfying witness, so an honest prover is never blocked from proving a true statement.
- [Underconstrained circuit](https://sorryfree.com/glossary/underconstrained-circuit/): A circuit whose constraints admit witnesses outside the specification, typically because a value computed during witness generation is never pinned down by a constraint. It is the dominant class of exploitable ZK bug.
- [Overconstrained circuit](https://sorryfree.com/glossary/overconstrained-circuit/): A circuit that rejects inputs the specification allows, so honest provers fail. It is the failure of completeness.
- [Symbolic vs computational model](https://sorryfree.com/glossary/symbolic-vs-computational/): The symbolic (Dolev-Yao) model treats cryptographic primitives as perfect black boxes and searches for logical attacks automatically; the computational model reasons about probabilistic polynomial-time adversaries and concrete security bounds, matching cryptographers' proofs.
- [Specification gap](https://sorryfree.com/glossary/specification-gap/): A mismatch between the property that was formally proved and the property that was actually needed, so a valid proof fails to cover real behaviour.
- [Trusted computing base and verification boundary](https://sorryfree.com/glossary/trusted-computing-base/): Everything that must be correct for a proof to mean what it claims: the prover kernel, the axioms used, the extraction or translation from code to model, the specification itself, and any unverified glue code. The edge of that set is the verification boundary.
- [Proof assistant vs SMT-based verifier](https://sorryfree.com/glossary/proof-assistant-vs-smt/): A proof assistant (Lean, Rocq, Isabelle, F*) checks human- or AI-written proofs against a small kernel and can express arbitrary mathematics; an SMT-based verifier (Picus, CIVER, Certora Prover, Kani) discharges properties automatically but only within decidable fragments and may return 'unknown'.
- [Bounded model checking](https://sorryfree.com/glossary/bounded-model-checking/): Exhaustive exploration of all program executions up to a fixed depth or loop bound, reporting concrete counterexamples; sound only within the bound.
- [Equivalence checking](https://sorryfree.com/glossary/equivalence-checking/): Proving that two artifacts compute the same function, for example optimised assembly against a Cryptol reference, or the KEVM semantics against a Lean EVM model.
- [Refinement](https://sorryfree.com/glossary/refinement/): A relation showing that an implementation's behaviours are a subset of a more abstract specification's behaviours, layered so low-level code refines a high-level model.
- [Constant-time verification](https://sorryfree.com/glossary/constant-time-verification/): Proving that a program's control flow and memory access pattern do not depend on secret data, so timing and cache side channels cannot leak keys.
- [Arithmetization (R1CS, PLONKish, AIR)](https://sorryfree.com/glossary/arithmetization/): The encoding of a computation as polynomial constraints over a finite field: rank-1 constraint systems (Groth16, gnark), PLONKish gates with copy and lookup constraints (Halo2), or algebraic intermediate representations over execution traces (STARKs, Plonky3, SP1).
- [Extraction (code to model)](https://sorryfree.com/glossary/extraction/): The step that turns a deployed circuit or program into the object a prover reasons about, whether by instrumenting synthesis (Halva), compiling to an IR (LLZK), or translating source (hax, Aeneas).
- [Witness generation vs constraints](https://sorryfree.com/glossary/witness-generation-vs-constraints/): Witness generation is the program that computes a satisfying assignment for honest inputs; constraints are what the verifier actually checks. Bugs arise when the two disagree.

## Other
- [Checklist](https://sorryfree.com/checklist/)
- [FAQ](https://sorryfree.com/faq/)
- [Timeline](https://sorryfree.com/news/)
- [About and methodology](https://sorryfree.com/about/)
- [JSON API](https://sorryfree.com/api/index.json)

---

# Full text summaries

ZK circuit formal verification frameworks: Clean, zkLean, Halva, Picus, LLZK and others compared
================================================================================

Frameworks that prove or check that a zero-knowledge circuit (R1CS, PLONKish, AIR, Circom, Noir, Halo2, Cairo) does what its specification says. Proof-assistant frameworks (Clean, zkLean, Halva, sp1-lean, Garden, Lampe) produce machine-checked soundness and sometimes completeness theorems; SMT and static tools (Picus, CIVER, Circomspect, zkFuzz) find underconstrained signals automatically but do not prove absence of bugs.

Clean: zkSecurity (hosted under Verified-zkEVM) — AIR, PLONK, R1CS, zkVM chips, Plonky3-style tables — Embedded Lean 4 DSL; proof assistant; soundness and completeness theorems per gadget, composed without re-proving — Active, funded by an Ethereum Foundation Verified zkEVM grant
sp1-lean: Succinct, with Nethermind — SP1 Hypercube, RISC-V (RV64) chips, AIR — Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model — Active
zkLean: Galois — R1CS, Lookups, MLE lookups, RAM (Jolt-style) — Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits — Active, Ethereum Foundation funded
Halva: Nethermind — Halo2, PLONKish — Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4 — Active, Ethereum Foundation grant
Picus: Veridise — Circom, R1CS, gnark, Halo2 (via LLZK), Plonky3 (via LLZK) — SMT (cvc5, Z3 with finite-field theory) uniqueness checking; fully automatic, no proofs to write — Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
LLZK: Veridise (Ethereum Foundation grant) — Circom, Halo2, Plonky3, Noir (in progress) — Shared MLIR dialect; lowers to Picus, zkLean, R1CS and Rocq (via Formal Land's rocq-of-llzk) — Active, v1.0 released 2026-04-08
Garden: Formal Land — Circom, Plonky3, LLZK — Rocq (Coq) proofs of determinism, functional correctness and completeness — Active
Lampe: Reilabs — Noir, ACIR — Semantics-first extraction of Noir programs into Lean 4, then property proofs — Active
proven-zk and gnark-lean-extractor: Reilabs — gnark, R1CS — Extract gnark circuits to Lean 4; prove properties with the proven-zk library — Maintained
CIVER: COSTA group, Universidad Complutense de Madrid (Albert Rubio et al.) — Circom 2.1.6 — Z3-backed weak safety (determinism), tag specifications, pre- and post-conditions, verified bottom-up per template — Research, maintained; R1CS, PLONK and ACIR support planned
Circomspect: Trail of Bits — Circom — Static analysis of Circom source for unconstrained signals and unsafe patterns; SARIF output — Maintained
zkFuzz: Hideaki Takahashi (Koukyosyumei) — Circom — Fuzzing for trace-constraint consistency (TCCT) violations between witness generation and constraints — Active research (IEEE S&P 2026)
Coda: Junrui Liu, Işıl Dillig et al. (UT Austin, Veridise) — Circom-style circuits reimplemented in Coda — Refinement-typed circuit language generating Coq proof obligations — Research (2023), not actively developed
Ecne: Franklyn Wang (0xPARC) — R1CS — Rule-based propagation to prove output uniqueness of R1CS constraint sets — Low activity research tool
NAVe: Pedro Antonino, Namrata Jain — Noir, ACIR — cvc5 with finite-field SMT-LIB theories — Research (January 2026)
Verified Cairo AIR (Stone and S-two): StarkWare with Jeremy Avigad and Yoav Seginer — Cairo VM AIR, Stone, S-two — Lean 4 proofs that AIR satisfiability implies a correct Cairo execution; Sierra-to-CASM building blocks — Active (paper June 2026); in-house at StarkWare, not a service
How to choose: Writing a new circuit and want it verified from day one: use **Clean** (AIR, PLONK, R1CS; sound and complete gadgets; Rust codegen on the roadmap) or **zkLean** (R1CS and lookup-based, Jolt-style). | Verifying an existing Halo2 circuit: **Halva**. An existing Noir program: **Lampe** or **NAVe**. An existing gnark circuit: **proven-zk**. An existing Circom circuit: **Picus** or **CIVER** for automatic checks, **Garden** or **Coda** for proofs. | Verifying a zkVM instruction set: **sp1-lean** (SP1, on Clean), **Clean Channels** for multi-table systems, or StarkWare's **Verified Cairo AIR** approach. | Need something automatic today, proofs later: run **Picus** or **zkFuzz** now, feed the same circuits through **LLZK** into a proof backend when the specification is written. | Require completeness as well as soundness (the circuit must never reject a valid input): only Clean, zk.golf submissions, Garden and CIVER's completeness mode state it explicitly; check the theorem statements of anything else.

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

Formal verification of proof systems and cryptographic security proofs: ArkLib, EasyCrypt, CryptoVerif, SSProve, ProofFrog
================================================================================

Frameworks for machine-checking the cryptographic argument itself: knowledge soundness of a polynomial IOP, the security reduction of a KEM, or the game-hopping proof in a paper. These work in the computational model, where the adversary is a probabilistic polynomial-time algorithm and security is a concrete bound, and they are the only tools on this index that verify the proof system rather than the circuit inside it.

ArkLib: Verified-zkEVM (Quang Dao et al., Ethereum Foundation) — Interactive oracle reductions, Sum-check, Polynomial commitments, FRI / STIR / WHIR, Fiat-Shamir, BCS — Lean 4 with VCV-io for probabilistic reasoning; completeness and soundness of proof-system components — Active; Nethermind maintains an ArkLibFri fork
EasyCrypt: Formosa Crypto (MPI-SP, Inria, Boston University, TU/e, Porto, Radboud) — KEMs and signatures (ML-KEM, X-Wing), Hash functions (SHA-3), Curve arithmetic (X25519), ZK verifiers — Interactive prover for game-based, code-based security proofs over probabilistic programs; paired with Jasmin for verified implementations — Active, mature
CryptoVerif: Bruno Blanchet, Inria (Prosecco) — Protocols: TLS 1.3, Signal, WireGuard, Key exchange, Authenticated encryption compositions — Automatic and guided sequences of games with concrete security bounds — Active, mature
SSProve: Aarhus University, MPI-SP and others — Primitives and protocols in the computational model — Rocq framework for state-separating proofs; hax backend available — Active research
ProofFrog: Ross Evans, Douglas Stebila (University of Waterloo) — Game-based security proofs (papers) — Custom language (FrogLang) and checker for game transitions; MCP server for AI assistants — Research (2025)
Squirrel: Inria (Bana-Comon logic) — Protocols — Interactive prover in the computationally complete symbolic attacker model — Active research
How to choose: Verifying a SNARK component (sum-check, FRI/STIR/WHIR, polynomial commitments, Fiat-Shamir): **ArkLib**, in Lean 4, with VCV-io for probabilistic reasoning. | Proving a primitive or protocol secure in the computational model with a team that already writes game-based proofs: **EasyCrypt** (paired with Jasmin for verified code) or **SSProve** in Rocq. | Automating a game sequence for a protocol like TLS, Signal or WireGuard: **CryptoVerif**. | Checking that a paper's game-hopping proof is well-formed: **ProofFrog**. | Proving a soundness bound for a Reed-Solomon proximity problem: the **better.codes** challenge is the live venue, with Lean-checked submissions.

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

Symbolic protocol verification tools: Tamarin, ProVerif, Verifpal, DY* compared
===============================================================================

Automatic analyzers that model a protocol with perfect (Dolev-Yao) cryptography and search for attacks over unbounded sessions: authentication failures, key-compromise impersonation, downgrade, replay and unknown-key-share. Tamarin and ProVerif are the standard tools; Verifpal trades expressiveness for approachability; DY* embeds the analysis in F* for executable code.

Tamarin: ETH Zürich, CISPA, University of Oxford — TLS 1.3, 5G AKA, WPA2, Noise, EMV, Messaging protocols — Symbolic (Dolev-Yao) analysis over unbounded sessions with user-guided lemmas — Active, mature
ProVerif: Bruno Blanchet, Inria (Prosecco) — Protocols, hax models extracted from Rust — Symbolic analysis of applied pi-calculus models, unbounded sessions, largely automatic — Active, mature
Verifpal: Symbolic Software (Nadim Kobeissi) — Protocols — Symbolic analysis with an intentionally simple modelling language — Maintained
DY*: Inria, CISPA, University of Stuttgart — Protocol implementations in F* (Signal, ACME) — Dolev-Yao reasoning inside the F* proof assistant, over executable protocol code — Research, active
How to choose: Stateful or complex protocols with many roles (TLS, 5G, Noise, EMV): **Tamarin**, which offers the most control and the best published track record. | Fast automatic analysis with a large existing model base and unbounded sessions: **ProVerif**. | A developer team writing its first model: **Verifpal**, then port to Tamarin or ProVerif when the model grows. | Analysis that must stay attached to the implementation: DY* in F*, or hax's ProVerif backend from Rust.

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

Verified cryptographic implementations: Jasmin, hax, Cryptol/SAW, Fiat-Crypto, HACL*, CryptoLine, Kani compared
================================================================================

Frameworks that prove properties of the code that ships: functional correctness against a specification, memory safety, and constant-time behaviour, for C, Rust, assembly and generated field arithmetic. This is where post-quantum verification happens in practice: ML-KEM and ML-DSA implementations in libjade, libcrux, AWS-LC, mlkem-native and Apple corecrypto all carry machine-checked proofs from tools in this category.

Jasmin and libjade: Formosa Crypto — ML-KEM (incl. AVX2), ML-DSA, X-Wing, Keccak / SHA-3, X25519, x86-64 assembly — Verified compiler from a low-level language to assembly; correctness proved in EasyCrypt; constant-time checked — Active (Jasmin 2026.03.2 released July 2026)
hax: Cryspen — Rust, libcrux ML-KEM and ML-DSA, Protocol models (ProVerif) — Translation of a large Rust subset into proof assistants; properties proved on the extracted model — Active; Lean backend under development with EF funding
Cryptol and SAW: Galois — C / LLVM, Java, x86-64, AWS-LC and s2n, BLST, Soroban (Formal Verso) — Executable specifications in Cryptol; SAW proves implementations equivalent via SMT and symbolic simulation — Active (SAW 1.4, Cryptol 3.4 in 2025)
Fiat-Crypto: MIT PLV — Finite-field arithmetic, Curve25519, P-256, Custom primes — Correct-by-construction code generation from Rocq proofs — Active, mature; deployed in BoringSSL and Go
HACL*, Vale and EverCrypt: Project Everest (Inria Prosecco, Microsoft Research, CMU) — C and assembly primitives, Firefox NSS, Linux kernel, mbedTLS, WireGuard — Verified C extracted from F* (HACL*) and verified assembly (Vale), unified in EverCrypt — Maintained; post-quantum work moved to libcrux/hax
Aeneas: Inria (Son Ho) and AeneasVerif — Rust, Plonky3 and RISC Zero code (2026 pipeline paper) — Functional translation of Rust into pure models for Lean, F* or Rocq — Active
Kani: AWS — Rust, Rust standard library verification challenge, AWS Rust libraries — Bounded model checking (CBMC backend) for panics, memory safety and user assertions — Active
CBMC: Diffblue, AWS and community — C, mlkem-native, s2n — Bounded model checking for memory safety and assertions — Active, mature
CryptoLine: Academia Sinica (Bow-Yaw Wang) — Bignum and NTT assembly, OpenSSL, BoringSSL, wolfSSL, PQC NTTs — Algebraic and range reasoning on straight-line arithmetic code — Active research
Verus: CMU, Microsoft and community — Rust (systems and some cryptographic code) — Ghost specifications and SMT-discharged proofs in Rust itself — Active
How to choose: High-speed assembly for a primitive with a matching EasyCrypt proof: **Jasmin** and **libjade**. | Production Rust that must stay readable: **hax** (to F*, Rocq, Lean, ProVerif) or **Aeneas** (to Lean), with **Kani** for panic and memory-safety proofs on the rest. | Hand-optimised C or assembly against a reference: **Cryptol and SAW**, **CryptoLine** for bignum and NTT arithmetic, **CBMC** for memory safety. | Field arithmetic for a new curve or field: **Fiat-Crypto** generates it with a proof. | A whole verified library rather than a proof of your own code: HACL* / EverCrypt or **libcrux**.

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

Proof assistants and general verifiers used in cryptography: Lean 4, Rocq, Isabelle, F*, ACL2, K, Certora Prover
================================================================================

The foundations underneath the specialised frameworks: interactive proof assistants (Lean 4, Rocq, Isabelle/HOL, F*, ACL2), a semantics framework (K), and SMT-based verifiers for smart contracts (Certora Prover, Halmos, hevm). Choosing one fixes the ecosystem, the available libraries, the hiring pool and, increasingly, which AI proving tools can help.

Lean 4 and Mathlib: Lean FRO and the Mathlib community — Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, EvmYul, Cairo AIR proofs — Interactive theorem prover with a small trusted kernel, a large mathematics library and a growing AI-prover ecosystem — Active
Rocq (formerly Coq): Inria and the Rocq community — Fiat-Crypto, SSProve, Garden, rocq-of-rust, rocq-of-solidity — Interactive theorem prover based on the calculus of inductive constructions — Active
Isabelle/HOL: TU München and University of Cambridge — C and ARM64 via AutoCorres2, Apple corecrypto — Higher-order logic with strong automation; refinement via AutoCorres2 — Active
F*: Microsoft Research and Inria — HACL*, hax (main backend), DY*, libcrux — Dependently typed effectful programming with SMT automation; extraction to C and OCaml — Active
ACL2 (R1CS and PFCS books): ACL2 community (Kestrel Institute) — R1CS, Prime-field constraint systems, acl2-jolt — First-order logic with strong automation; R1CS and PFCS libraries; acl2-jolt for Jolt circuits — Mature, niche
K framework and KEVM: Runtime Verification — EVM (KEVM), zkevm-harness, Lean backend for K — Rewriting-based semantics from which interpreters, symbolic executors and provers are derived — Active, mature
Certora Prover: Certora — Solidity, Vyper, Solana (Rust), Move, Soroban — Rule-based specification (CVL) discharged by SMT over bytecode — Active
How to choose: New ZK verification project in 2026: **Lean 4**. The libraries, the funded projects and the AI provers are there. | Rust implementation verification with a Rocq team, or reuse of Fiat-Crypto: **Rocq**. | C and ARM64 code with a refinement-style methodology: **Isabelle/HOL** with AutoCorres2, as Apple did. | Executable semantics that both runs and proves (EVM, zkVM ISAs): the **K framework**. | On-chain verifier contract properties: **Certora Prover** for full rule-based verification, **Halmos** or **hevm** for bounded symbolic checks.

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

Formal verification challenges and programs for ZK: zk.golf, better.codes, Verified zkEVM
================================================================================

Live venues where verified artifacts are produced competitively or under a coordinated program: zk.golf (cheapest circuit with a Lean proof of soundness and completeness), better.codes (raise a Lean-checked soundness bound for Reed-Solomon proximity), and the Ethereum Foundation's Verified zkEVM program that funds most of the frameworks on this index.

zk.golf: zkSecurity — R1CS over BN254, GF(2) hash compression track, Clean circuits — Fixed Lean interface and specification per challenge; submissions are Clean circuits plus kernel-checked proofs; score = allocations + constraints — Active (launched 2026-07-02)
better.codes: Ethereum Foundation Formal Verification team, Yukon and zkSecurity — koalaIRS12 proximity problem, FRI / STIR / WHIR soundness, Lean 4 — A formalised open problem from the Proximity Prize; solvers point AI agents at improving the machine-checked lower bound; every submission is kernel-checked and promoted proofs are credited — Active (launched 2026-08-20)
Verified zkEVM program: Ethereum Foundation — Clean, zkLean, Halva, ArkLib, LLZK, Sail RISC-V Lean, KEVM equivalence, hax Lean backend — Grants and coordination for a formally verified, bug-free zk(E)VM stack, targeted for 2027 — Active
How to choose: Learn how a sound-and-complete circuit proof is structured, or benchmark an optimisation: **zk.golf**. | Contribute to or watch AI-assisted theorem proving on a real cryptographic bound: **better.codes**. | Track which frameworks are funded, maintained and interoperable: the **Verified zkEVM** program page and its Overview repository.

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

Clean (zkSecurity): Lean 4 formal verification framework for ZK circuits, sound and complete
================================================================================

Clean is an embedded Lean 4 language for writing zero-knowledge circuits in which every gadget carries a machine-checked proof of both soundness (any satisfying witness meets the specification) and completeness (every valid input has a satisfying witness). Created and maintained by zkSecurity, it targets AIR-style tables with lookups, PLONK and R1CS, composes verified gadgets into larger verified circuits, and since June 2026 models cross-table interactions so that whole multi-table systems such as zkVMs can be proved sound.

Maintainer: zkSecurity (hosted under Verified-zkEVM)
Website: https://clean.zksecurity.xyz
Category: ZK circuit verification
Targets: AIR, PLONK, R1CS, zkVM chips, Plonky3-style tables
Approach: Embedded Lean 4 DSL; proof assistant; soundness and completeness theorems per gadget, composed without re-proving
Access: Open source (MIT)
Status: Active, funded by an Ethereum Foundation Verified zkEVM grant
Strengths: Only circuit framework on this index whose default deliverable is both soundness and completeness for every gadget. | Compositional: verified gadgets are reused as subcircuits without re-proving, so large circuits and multi-table zkVMs are tractable. | Active ecosystem: sp1-lean, zk.golf, published verified hash gadgets, and a documented agent workflow for LLM-assisted proving.
Limits: Circuits are written in Clean; verifying an existing Circom or Halo2 codebase means porting, modelling or waiting for the LLZK frontend. | Backend code generation (Plonky3 Rust) is on the roadmap; until it ships, the correspondence between the Lean circuit and the deployed constraints is a review item. | Proof engineering in Lean 4 has a learning curve; zkSecurity's own comparison rates the Lean frameworks as the most sophisticated but heaviest on tactics.
Firms using it: zkSecurity
Sources: https://clean.zksecurity.xyz | https://blog.zksecurity.xyz/posts/clean/ | https://blog.zksecurity.xyz/posts/clean-verified-zkvms/ | https://blog.zksecurity.xyz/posts/poseidon-clean/ | https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/

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

sp1-lean: Lean verification of SP1 Hypercube's RISC-V chips, built on Clean
===========================================================================

sp1-lean is Succinct's Lean 4 project, developed with Nethermind, that expresses the constraints of SP1 Hypercube's RISC-V chips in Clean and proves them sound against the Sail RISC-V reference model. As of the Ethereum Foundation's May 2026 review, 51 of 62 opcodes were fully proven; completeness is deferred for five chips.

Maintainer: Succinct, with Nethermind
Website: https://github.com/succinctlabs/sp1-lean
Category: ZK circuit verification
Targets: SP1 Hypercube, RISC-V (RV64) chips, AIR
Approach: Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model
Access: Open source (MIT / Apache-2.0)
Status: Active
Strengths: Real, deployed zkVM constraints proved against an independent ISA model rather than a hand-written spec. | Built on Clean, so proofs compose with other Clean gadgets and benefit from the Channel work for multi-table soundness. | Openly reviewed by a third party (the EF Formal Verification team), with gaps published.
Limits: Specific to SP1 Hypercube; not a general framework. | Completeness deferred for several chips and some opcodes still unproven at last public review. | Correspondence between the Lean restatement and the Rust constraints is a manual step (a Plonky3 codegen backend for Clean would close it).
Firms using it: zkSecurity, Nethermind (Formal Verification team)
Sources: https://blog.succinct.xyz/nethermind-lean/ | https://zkevm.ethereum.foundation/blog/sp1-fv

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

zkLean: Galois's Lean 4 framework for R1CS and lookup-based circuits, Jolt-style
================================================================================

zkLean is Galois's Lean 4 framework for stating and proving soundness of extracted circuits, with native support for R1CS, lookups, multilinear-extension lookups and RAM in the style of the Jolt zkVM. It ships a SHA-3 example and a Jolt extractor, and is one of the proof backends LLZK lowers to.

Maintainer: Galois
Website: https://github.com/GaloisInc/zk-lean
Category: ZK circuit verification
Targets: R1CS, Lookups, MLE lookups, RAM (Jolt-style)
Approach: Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits
Access: Open source (BSD-3)
Status: Active, Ethereum Foundation funded
Strengths: First-class lookups, MLE lookups and RAM, matching Jolt-era zkVM designs. | Extraction-oriented, so existing code can be verified without rewriting. | Maintained by a firm with two decades of verification delivery.
Limits: Primarily soundness; check the completeness story per project. | Younger than Clean on published verified gadgets. | Hoare-style proofs require familiarity with Std.Do.
Firms using it: Galois
Sources: https://github.com/GaloisInc/zk-lean | https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/

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

Halva: Nethermind's Lean 4 verification of Halo2 circuits
=========================================================

Halva extracts the gate, copy, permutation and lookup constraints of a Halo2 circuit at synthesis time and lets engineers prove soundness in Lean 4. In July 2025 Nethermind used it to find a critical soundness bug in Scroll's deprecated Keccak-256 circuit.

Maintainer: Nethermind
Website: https://github.com/NethermindEth/Halva
Category: ZK circuit verification
Targets: Halo2, PLONKish
Approach: Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4
Access: Open source
Status: Active, Ethereum Foundation grant
Strengths: Works on real Halo2 code without rewriting it. | Public critical finding in a production-grade circuit. | Same team maintains CertiPlonk (Plonky3) and Lean EVM work, so zkEVM stacks can be covered end to end.
Limits: Halo2 only. | Soundness-focused; completeness is a separate exercise. | Extraction is a trusted step; review it.
Firms using it: Nethermind (Formal Verification team)
Sources: https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean | https://github.com/NethermindEth/Halva

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

Picus: Automatic SMT-based underconstraint detection for Circom, R1CS, gnark and LLZK
================================================================================

Picus checks whether every output signal of a circuit is uniquely determined by its inputs, which is the automatic, specification-free way to detect underconstrained circuits. It runs on Circom, R1CS and gnark directly and on Halo2 and Plonky3 through LLZK, and Veridise has used it with LLZK to verify SP1 core operations and RISC Zero circuits.

Maintainer: Veridise
Website: https://github.com/Veridise/Picus
Category: ZK circuit verification
Targets: Circom, R1CS, gnark, Halo2 (via LLZK), Plonky3 (via LLZK)
Approach: SMT (cvc5, Z3 with finite-field theory) uniqueness checking; fully automatic, no proofs to write
Access: Open source (MIT); newer versions ship in Veridise AuditHub
Status: Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
Strengths: No specification, no proof engineering, fast on small and medium circuits. | Broad frontend coverage through LLZK. | Widely used and cited; the reference tool for its property.
Limits: Proves uniqueness, not functional correctness. | Timeouts and 'unknown' results on large circuits. | Cutting-edge features are in the commercial AuditHub version.
Firms using it: Veridise
Sources: https://github.com/Veridise/Picus | https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/

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

LLZK: MLIR-based intermediate representation connecting ZK frontends to verification backends
================================================================================

LLZK is a shared intermediate representation for ZK circuits built on MLIR. Frontends for Circom, Halo2 and Plonky3 (Noir in progress) lower into it, and backends emit Picus queries, zkLean models, R1CS and Rocq via Formal Land's rocq-of-llzk, so one circuit can be checked automatically and then proved.

Maintainer: Veridise (Ethereum Foundation grant)
Website: https://github.com/project-llzk
Category: ZK circuit verification
Targets: Circom, Halo2, Plonky3, Noir (in progress)
Approach: Shared MLIR dialect; lowers to Picus, zkLean, R1CS and Rocq (via Formal Land's rocq-of-llzk)
Access: Open source
Status: Active, v1.0 released 2026-04-08
Strengths: Decouples frontend language from verification backend. | Backed by an EF grant and adopted by Galois and Formal Land backends. | Makes SP1 and RISC Zero style verification repeatable.
Limits: Infrastructure rather than a verifier; you still need a backend and a spec. | Noir frontend incomplete at v1.0. | Adds a translation step to the trusted computing base.
Firms using it: Galois, Veridise, Formal Land
Sources: https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/ | https://github.com/project-llzk

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

Garden: Formal Land's Rocq framework for Circom, Plonky3 and LLZK circuits
==========================================================================

Garden is Formal Land's Rocq framework for proving determinism, functional correctness and completeness of circuits written in Circom or Plonky3, and of anything lowered through LLZK via rocq-of-llzk.

Maintainer: Formal Land
Website: https://github.com/formal-land/garden
Category: ZK circuit verification
Targets: Circom, Plonky3, LLZK
Approach: Rocq (Coq) proofs of determinism, functional correctness and completeness
Access: Open source
Status: Active
Strengths: States completeness explicitly. | Same ecosystem as rocq-of-rust and rocq-of-solidity. | LLZK backend gives it Halo2 reach.
Limits: Smaller public gadget library than Clean. | Rocq talent pool is narrower than Lean's in ZK. | Frontend coverage depends on LLZK for non-Circom inputs.
Firms using it: Formal Land
Sources: https://github.com/formal-land/garden | https://formal.land

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

Lampe: Reilabs' Noir-to-Lean semantics extraction
=================================================

Lampe extracts the semantics of Noir programs into Lean 4 so that properties of Aztec-ecosystem circuits can be stated and proved. It is the main proof-assistant route for Noir; NAVe is the automatic alternative.

Maintainer: Reilabs
Website: https://github.com/reilabs/lampe
Category: ZK circuit verification
Targets: Noir, ACIR
Approach: Semantics-first extraction of Noir programs into Lean 4, then property proofs
Access: Open source
Status: Active
Strengths: Only maintained proof-assistant path for Noir. | Team has shipped verified production circuits (Worldcoin). | Lean 4, so interoperable with the rest of the ecosystem.
Limits: Noir only. | Semantics extraction is part of the TCB. | Public examples still growing.
Firms using it: Reilabs
Sources: https://github.com/reilabs/lampe | https://reilabs.io

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

proven-zk and gnark-lean-extractor: Lean 4 verification of gnark circuits
=========================================================================

proven-zk is a Lean 4 library, with a companion gnark extractor, used by Reilabs to verify Worldcoin's Semaphore Merkle tree batcher circuits. The work surfaced a comparison bug in gnark itself.

Maintainer: Reilabs
Website: https://github.com/reilabs/proven-zk
Category: ZK circuit verification
Targets: gnark, R1CS
Approach: Extract gnark circuits to Lean 4; prove properties with the proven-zk library
Access: Open source
Status: Maintained
Strengths: Production track record (Worldcoin). | Found a real bug in the underlying framework. | Reusable lemma library for common gadgets.
Limits: gnark only. | Extractor coverage of gnark APIs is partial. | Less active than Lampe.
Firms using it: Reilabs
Sources: https://github.com/reilabs/proven-zk

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

CIVER: Modular SMT verification integrated in a Circom fork
===========================================================

CIVER is a verifier built into a fork of the Circom compiler by the team behind Circom's own maintainers' academic group. It checks weak safety (every output determined by inputs), tag specifications and user-written pre- and post-conditions template by template, reusing results bottom-up so large circomlib-style codebases scale.

Maintainer: COSTA group, Universidad Complutense de Madrid (Albert Rubio et al.)
Website: https://github.com/costa-group/circom_civer
Category: ZK circuit verification
Targets: Circom 2.1.6
Approach: Z3-backed weak safety (determinism), tag specifications, pre- and post-conditions, verified bottom-up per template
Access: Open source (GPL)
Status: Research, maintained; R1CS, PLONK and ACIR support planned
Strengths: No extraction step; verifies what the compiler emits. | Modular, so circomlib-scale codebases are feasible. | Supports functional pre- and post-conditions, not just determinism.
Limits: Circom only, pinned to a compiler version. | SMT limits: timeouts on nonlinear-heavy templates. | Academic maintenance cadence.
Firms using it: none listed
Sources: https://github.com/costa-group/circom_civer

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

Circomspect: Trail of Bits' static analyzer and linter for Circom
=================================================================

Circomspect is a static analyzer for Circom that flags unconstrained signals, unused or shadowed variables, unsafe `<--` assignments and other patterns behind known circuit bugs. It is a linter, not a verifier: fast, easy to add to CI, and blind to bugs that do not match a pattern.

Maintainer: Trail of Bits
Website: https://github.com/trailofbits/circomspect
Category: ZK circuit verification
Targets: Circom
Approach: Static analysis of Circom source for unconstrained signals and unsafe patterns; SARIF output
Access: Open source (GPL-3.0)
Status: Maintained
Strengths: Zero setup, runs in CI. | Built by an audit firm from real findings. | Good developer ergonomics.
Limits: Pattern-based; no semantic guarantee. | Circom only. | No completeness or soundness statement of any kind.
Firms using it: Trail of Bits
Sources: https://github.com/trailofbits/circomspect

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

zkFuzz: Fuzzer for trace-constraint inconsistencies in Circom
=============================================================

zkFuzz fuzzes Circom programs for disagreements between what witness generation computes and what the constraints enforce, the root of most underconstraint bugs. Its paper reports 66 bugs across 354 circuits.

Maintainer: Hideaki Takahashi (Koukyosyumei)
Website: https://github.com/Koukyosyumei/zkFuzz
Category: ZK circuit verification
Targets: Circom
Approach: Fuzzing for trace-constraint consistency (TCCT) violations between witness generation and constraints
Access: Open source
Status: Active research (IEEE S&P 2026)
Strengths: Concrete exploits, not warnings. | Scales where solvers do not. | Strong published results.
Limits: No guarantee on a clean run. | Circom only. | Single-maintainer research project.
Firms using it: none listed
Sources: https://github.com/Koukyosyumei/zkFuzz

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

Coda: Certified circuits via refinement types in Coq
====================================================

Coda is a research language in which circuits carry refinement types; the type checker generates Coq lemmas whose proofs establish functional correctness. Its authors found six bugs in circomlib-derived circuits with it.

Maintainer: Junrui Liu, Işıl Dillig et al. (UT Austin, Veridise)
Website: https://eprint.iacr.org/2023/547
Category: ZK circuit verification
Targets: Circom-style circuits reimplemented in Coda
Approach: Refinement-typed circuit language generating Coq proof obligations
Access: Research artifact
Status: Research (2023), not actively developed
Strengths: Clear methodology paper. | Found real bugs. | Refinement types keep specs close to code.
Limits: Requires rewriting circuits in Coda. | No active maintenance. | Coq only.
Firms using it: Veridise
Sources: https://eprint.iacr.org/2023/547

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

Ecne: Early R1CS uniqueness checker in Julia
============================================

Ecne was the first widely used tool for proving that an R1CS constraint set uniquely determines its outputs, the property later automated with SMT by Picus. It remains useful as a lightweight second opinion on small R1CS systems.

Maintainer: Franklyn Wang (0xPARC)
Website: https://github.com/franklynwang/EcneProject
Category: ZK circuit verification
Targets: R1CS
Approach: Rule-based propagation to prove output uniqueness of R1CS constraint sets
Access: Open source (GPL-3.0)
Status: Low activity research tool
Strengths: Simple, fast, historically significant. | Works directly on R1CS output of any compiler.
Limits: Incomplete rule set; many false negatives. | Julia dependency; little maintenance. | No functional properties.
Firms using it: none listed
Sources: https://github.com/franklynwang/EcneProject

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

NAVe: Automatic proper-constrainedness checking for Noir
========================================================

NAVe checks Noir programs for proper constrainedness using cvc5's finite-field theory, giving the Noir ecosystem an automatic underconstraint detector comparable to Picus for Circom.

Maintainer: Pedro Antonino, Namrata Jain
Website: https://arxiv.org/abs/2601.09372
Category: ZK circuit verification
Targets: Noir, ACIR
Approach: cvc5 with finite-field SMT-LIB theories
Access: Research
Status: Research (January 2026)
Strengths: Automatic, no spec required. | Targets Noir directly.
Limits: Young research tool. | Solver limits on large programs. | Determinism, not correctness.
Firms using it: none listed
Sources: https://arxiv.org/abs/2601.09372

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

Verified Cairo AIR (Stone and S-two): StarkWare's Lean 4 soundness proofs of the Cairo VM AIR
================================================================================

StarkWare, with Jeremy Avigad and Yoav Seginer, has proved in Lean 4 that satisfying the Cairo VM's AIR (for both the Stone and S-two provers) implies a correct Cairo execution, and in July 2026 used the same methodology to verify the STRK20 privacy pool with more than 230 theorems.

Maintainer: StarkWare with Jeremy Avigad and Yoav Seginer
Website: https://arxiv.org/abs/2606.04311
Category: ZK circuit verification
Targets: Cairo VM AIR, Stone, S-two
Approach: Lean 4 proofs that AIR satisfiability implies a correct Cairo execution; Sierra-to-CASM building blocks
Access: Open source
Status: Active (paper June 2026); in-house at StarkWare, not a service
Strengths: Whole-VM soundness statement for a deployed prover. | Long track record and academic rigour. | Extended to an application (STRK20).
Limits: Cairo specific and in-house. | Not packaged as a reusable framework. | Completeness is not the headline property.
Firms using it: none listed
Sources: https://arxiv.org/abs/2606.04311 | https://starkware.co/blog/strk20-formal-verification/ | https://github.com/NethermindEth/horus-checker

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

ArkLib: Lean 4 library for verifying SNARK components: IORs, sum-check, FRI, STIR, WHIR, Fiat-Shamir
================================================================================

ArkLib formalizes the building blocks of modern SNARKs in Lean 4: interactive oracle reductions and their composition, sum-check, polynomial commitment schemes, the FRI, STIR and WHIR proximity protocols, Fiat-Shamir and the BCS transform, with completeness and soundness theorems. It is the proof-system half of the Verified zkEVM program.

Maintainer: Verified-zkEVM (Quang Dao et al., Ethereum Foundation)
Website: https://github.com/Verified-zkEVM/ArkLib
Category: Proof systems and computational proofs
Targets: Interactive oracle reductions, Sum-check, Polynomial commitments, FRI / STIR / WHIR, Fiat-Shamir, BCS
Approach: Lean 4 with VCV-io for probabilistic reasoning; completeness and soundness of proof-system components
Access: Open source
Status: Active; Nethermind maintains an ArkLibFri fork
Strengths: Only library formalizing the actual proof-system components used in production zkEVMs. | Lean 4, composable with Clean and other circuit proofs. | Backed by the EF and Nethermind.
Limits: Research-shaped; APIs and coverage change quickly. | Requires deep familiarity with both Lean and proof-system theory. | Not a tool you point at a codebase.
Firms using it: Nethermind (Formal Verification team)
Sources: https://github.com/Verified-zkEVM/ArkLib | https://blog.ethereum.org/2025/12/18/zkevm-security-foundations | https://verified-zkevm.org

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

EasyCrypt: Computational security proofs with relational Hoare logic
====================================================================

EasyCrypt is the reference tool for machine-checked computational security proofs: game-based reductions expressed over probabilistic programs with a relational Hoare logic. It underpins the verified ML-KEM, X-Wing, SHA-3 and X25519 implementations in libjade, and Nethermind used it for the first honesty proof of a production ZK verifier (ZKsync).

Maintainer: Formosa Crypto (MPI-SP, Inria, Boston University, TU/e, Porto, Radboud)
Website: https://easycrypt.info
Category: Proof systems and computational proofs
Targets: KEMs and signatures (ML-KEM, X-Wing), Hash functions (SHA-3), Curve arithmetic (X25519), ZK verifiers
Approach: Interactive prover for game-based, code-based security proofs over probabilistic programs; paired with Jasmin for verified implementations
Access: Open source
Status: Active, mature
Strengths: Proofs match how cryptographers reason. | End-to-end with Jasmin: proof, spec and assembly agree. | Post-quantum track record: ML-KEM and X-Wing.
Limits: Steep learning curve; small pool of practitioners. | Proofs do not transfer automatically to code outside Jasmin. | Not a circuit tool.
Firms using it: Nethermind (Formal Verification team)
Sources: https://easycrypt.info | https://formosa-crypto.org

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

CryptoVerif: Automatic game sequences in the computational model
================================================================

CryptoVerif automates game-hopping proofs in the computational model, producing concrete security bounds for protocols. It has been applied to TLS 1.3, Signal and WireGuard and is the computational counterpart to ProVerif.

Maintainer: Bruno Blanchet, Inria (Prosecco)
Website: https://bblanche.gitlabpages.inria.fr/CryptoVerif/
Category: Proof systems and computational proofs
Targets: Protocols: TLS 1.3, Signal, WireGuard, Key exchange, Authenticated encryption compositions
Approach: Automatic and guided sequences of games with concrete security bounds
Access: Open source
Status: Active, mature
Strengths: Automation reduces proof effort. | Concrete bounds, not just yes/no. | Long record on major protocols.
Limits: Less flexible than EasyCrypt for novel primitives. | Modelling effort still significant. | Small user community.
Firms using it: none listed
Sources: https://bblanche.gitlabpages.inria.fr/CryptoVerif/

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

SSProve: State-separating modular game-based proofs in Rocq
===========================================================

SSProve brings state-separating, modular game-based proofs to Rocq, letting large cryptographic proofs be assembled from packages. hax can target it from Rust, connecting implementations to proofs.

Maintainer: Aarhus University, MPI-SP and others
Website: https://github.com/SSProve/ssprove
Category: Proof systems and computational proofs
Targets: Primitives and protocols in the computational model
Approach: Rocq framework for state-separating proofs; hax backend available
Access: Open source
Status: Active research
Strengths: Modular proof structure scales. | Rocq ecosystem and hax bridge. | Foundationally rigorous.
Limits: Research maturity. | Fewer worked examples than EasyCrypt. | Requires Rocq expertise.
Firms using it: Cryspen
Sources: https://github.com/SSProve/ssprove

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

ProofFrog: Checker for game-hopping proofs in provable security
===============================================================

ProofFrog checks that the game transitions in a provable-security proof are valid, giving paper authors and reviewers a mechanical check on the skeleton of a reduction. It ships an MCP server so AI assistants can drive it.

Maintainer: Ross Evans, Douglas Stebila (University of Waterloo)
Website: https://github.com/ProofFrog/ProofFrog
Category: Proof systems and computational proofs
Targets: Game-based security proofs (papers)
Approach: Custom language (FrogLang) and checker for game transitions; MCP server for AI assistants
Access: Open source
Status: Research (2025)
Strengths: Low barrier for cryptographers. | AI-assistant integration. | Catches structural proof errors early.
Limits: Not a full computational prover. | Research project. | Limited primitive library.
Firms using it: none listed
Sources: https://github.com/ProofFrog/ProofFrog

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

Squirrel: Computationally sound symbolic proofs
===============================================

Squirrel proves protocol security in a symbolic-looking logic whose results are computationally sound, bridging the gap between Tamarin-style automation and EasyCrypt-style guarantees.

Maintainer: Inria (Bana-Comon logic)
Website: https://squirrel-prover.github.io
Category: Proof systems and computational proofs
Targets: Protocols
Approach: Interactive prover in the computationally complete symbolic attacker model
Access: Open source
Status: Active research
Strengths: Computational soundness with symbolic ergonomics. | Interactive control.
Limits: Research maturity. | Small community. | Limited primitives.
Firms using it: none listed
Sources: https://squirrel-prover.github.io

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

Tamarin: Symbolic protocol verification with multiset rewriting
===============================================================

Tamarin is the most widely used symbolic protocol verifier for stateful, multi-role protocols. It has analysed TLS 1.3, 5G authentication, WPA2, the Noise framework and EMV, and supports interactive guidance when automation stalls.

Maintainer: ETH Zürich, CISPA, University of Oxford
Website: https://tamarin-prover.com
Category: Symbolic protocol analysis
Targets: TLS 1.3, 5G AKA, WPA2, Noise, EMV, Messaging protocols
Approach: Symbolic (Dolev-Yao) analysis over unbounded sessions with user-guided lemmas
Access: Open source
Status: Active, mature
Strengths: Most expressive of the automatic symbolic tools. | Interactive mode for hard proofs. | Largest record of real protocol findings.
Limits: Modelling skill required; non-termination is possible. | Symbolic abstraction misses cryptographic weaknesses. | No code connection.
Firms using it: Symbolic Software
Sources: https://tamarin-prover.com

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

ProVerif: Automatic symbolic analysis in the applied pi-calculus
================================================================

ProVerif automatically analyses protocol models in the applied pi-calculus for secrecy, authentication and equivalence properties over unbounded sessions. It has a large model base and is a target of hax, so Rust implementations can be analysed symbolically.

Maintainer: Bruno Blanchet, Inria (Prosecco)
Website: https://bblanche.gitlabpages.inria.fr/proverif/
Category: Symbolic protocol analysis
Targets: Protocols, hax models extracted from Rust
Approach: Symbolic analysis of applied pi-calculus models, unbounded sessions, largely automatic
Access: Open source
Status: Active, mature
Strengths: High automation. | hax backend from Rust. | Decades of published models.
Limits: Weaker on global mutable state. | Symbolic model only. | May not terminate on some models.
Firms using it: Cryspen, Symbolic Software
Sources: https://bblanche.gitlabpages.inria.fr/proverif/

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

Verifpal: Developer-friendly symbolic protocol analysis
=======================================================

Verifpal is a symbolic protocol analyser designed for engineers rather than formal-methods specialists. Its modelling language is deliberately simple, which limits expressiveness relative to Tamarin and ProVerif but lowers the barrier to a first model.

Maintainer: Symbolic Software (Nadim Kobeissi)
Website: https://verifpal.com
Category: Symbolic protocol analysis
Targets: Protocols
Approach: Symbolic analysis with an intentionally simple modelling language
Access: Open source
Status: Maintained
Strengths: Readable models. | Fast feedback. | Good documentation.
Limits: Less expressive. | Fewer guarantees than the mature tools. | Smaller community.
Firms using it: Symbolic Software
Sources: https://verifpal.com

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

DY*: Symbolic protocol verification embedded in F* for executable code
======================================================================

DY* verifies protocol implementations written in F* against symbolic security properties, so the analysed model is the executable code. It has been applied to Signal and ACME and is the successor to ProScript.

Maintainer: Inria, CISPA, University of Stuttgart
Website: https://github.com/REPROSEC/dolev-yao-star
Category: Symbolic protocol analysis
Targets: Protocol implementations in F* (Signal, ACME)
Approach: Dolev-Yao reasoning inside the F* proof assistant, over executable protocol code
Access: Open source
Status: Research, active
Strengths: No model-code gap. | Composable with HACL* verified primitives.
Limits: F* implementation required. | Research maturity. | Manual proof effort.
Firms using it: none listed
Sources: https://github.com/REPROSEC/dolev-yao-star

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

Jasmin and libjade: Verified high-speed assembly with constant-time guarantees
==============================================================================

Jasmin is a language and verified compiler for writing cryptographic assembly whose functional correctness is proved in EasyCrypt and whose constant-time behaviour is checked by the compiler. libjade is the resulting library of verified implementations, including ML-KEM with AVX2 rejection sampling, ML-DSA, X-Wing, SHA-3 and X25519.

Maintainer: Formosa Crypto
Website: https://github.com/jasmin-lang/jasmin
Category: Verified implementations
Targets: ML-KEM (incl. AVX2), ML-DSA, X-Wing, Keccak / SHA-3, X25519, x86-64 assembly
Approach: Verified compiler from a low-level language to assembly; correctness proved in EasyCrypt; constant-time checked
Access: Open source
Status: Active (Jasmin 2026.03.2 released July 2026)
Strengths: Strongest end-to-end story: proof to assembly. | Post-quantum coverage. | Performance competitive with hand-written assembly.
Limits: Assembly must be written in Jasmin. | x86-64 focus. | Expertise concentrated in a few groups.
Firms using it: none listed
Sources: https://github.com/jasmin-lang/jasmin | https://github.com/formosa-crypto/libjade | https://formosa-crypto.org

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

hax: Rust to F*, Rocq, Lean, ProVerif, SSProve and EasyCrypt
============================================================

hax translates a large subset of Rust into F*, Rocq, ProVerif, SSProve and EasyCrypt, with a Lean backend in development. Cryspen used it to verify libcrux's ML-KEM (portable and AVX2 field arithmetic, NTT and serialization) in F*; libcrux ML-KEM ships in Mozilla and Signal.

Maintainer: Cryspen
Website: https://github.com/cryspen/hax
Category: Verified implementations
Targets: Rust, libcrux ML-KEM and ML-DSA, Protocol models (ProVerif)
Approach: Translation of a large Rust subset into proof assistants; properties proved on the extracted model
Access: Open source
Status: Active; Lean backend under development with EF funding
Strengths: Production Rust stays production Rust. | Many backends, including symbolic (ProVerif). | Shipped verified post-quantum code at scale.
Limits: Rust subset restrictions. | Properties are only as good as the specification (Verification Theatre). | Lean backend not yet complete.
Firms using it: Cryspen
Sources: https://github.com/cryspen/hax | https://cryspen.com/post/ml-kem-verification/ | https://eprint.iacr.org/2026/192

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

Cryptol and SAW: Specifications in Cryptol, equivalence proofs of C, LLVM, Java and x86 in SAW
================================================================================

Cryptol is a specification language for cryptographic algorithms and SAW proves that C, LLVM, Java or x86 implementations match those specifications. Galois has used the pair on AWS s2n and AWS-LC (with NSym for AArch64), the BLST BLS library, Apple corecrypto and Stellar's Soroban.

Maintainer: Galois
Website: https://github.com/GaloisInc/saw-script
Category: Verified implementations
Targets: C / LLVM, Java, x86-64, AWS-LC and s2n, BLST, Soroban (Formal Verso)
Approach: Executable specifications in Cryptol; SAW proves implementations equivalent via SMT and symbolic simulation
Access: Open source (BSD-3)
Status: Active (SAW 1.4, Cryptol 3.4 in 2025)
Strengths: Verifies existing optimised code. | Deep industrial track record (AWS, Apple). | Executable specs double as test oracles.
Limits: SMT-bounded reasoning; loops and large state need care. | Specification effort in Cryptol. | Not a circuit tool (Galois's zkLean covers that).
Firms using it: Galois
Sources: https://github.com/GaloisInc/saw-script | https://tools.galois.com/cryptol | https://github.com/awslabs/aws-lc-verification

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

Fiat-Crypto: Rocq-verified generation of field arithmetic
=========================================================

Fiat-Crypto generates field-arithmetic code (C, Rust, Go, Zig and more) from parameters with a Rocq proof that the output is correct. Its Curve25519 and P-256 code ships in BoringSSL and Go's standard library.

Maintainer: MIT PLV
Website: https://github.com/mit-plv/fiat-crypto
Category: Verified implementations
Targets: Finite-field arithmetic, Curve25519, P-256, Custom primes
Approach: Correct-by-construction code generation from Rocq proofs
Access: Open source
Status: Active, mature; deployed in BoringSSL and Go
Strengths: Proved generator, no per-output proof needed. | Massive deployment. | Any prime, several languages.
Limits: Field arithmetic only. | Performance below the best hand-written assembly. | No post-quantum coverage.
Firms using it: none listed
Sources: https://github.com/mit-plv/fiat-crypto

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

HACL*, Vale and EverCrypt: Project Everest's verified cryptographic library in F* and Vale
================================================================================

HACL* is a library of cryptographic primitives verified in F* for memory safety, functional correctness and secret independence, with Vale providing verified assembly and EverCrypt a unified API. Its code runs in Firefox, the Linux kernel, mbedTLS and WireGuard.

Maintainer: Project Everest (Inria Prosecco, Microsoft Research, CMU)
Website: https://hacl-star.github.io
Category: Verified implementations
Targets: C and assembly primitives, Firefox NSS, Linux kernel, mbedTLS, WireGuard
Approach: Verified C extracted from F* (HACL*) and verified assembly (Vale), unified in EverCrypt
Access: Open source
Status: Maintained; post-quantum work moved to libcrux/hax
Strengths: Broadest deployment of any verified library. | Memory safety, correctness and constant-time in one framework. | Agile multiplexing in EverCrypt.
Limits: Classical primitives; post-quantum lives in libcrux. | F* expertise required to extend. | Extraction toolchain is complex.
Firms using it: none listed
Sources: https://hacl-star.github.io

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

Aeneas: Rust to Lean, F* and Rocq translation via Charon
========================================================

Aeneas translates Rust into pure functional models for Lean, F* or Rocq through the Charon frontend. A May 2026 pipeline paper used it with hax, ArkLib and CompPoly, plus AI provers, to verify Plonky3 FRI folding and field arithmetic and RISC Zero Merkle checks.

Maintainer: Inria (Son Ho) and AeneasVerif
Website: https://github.com/AeneasVerif/aeneas
Category: Verified implementations
Targets: Rust, Plonky3 and RISC Zero code (2026 pipeline paper)
Approach: Functional translation of Rust into pure models for Lean, F* or Rocq
Access: Open source
Status: Active
Strengths: Lean-first, integrates with ArkLib and Clean. | Demonstrated on real prover code. | Handles ownership-heavy Rust well.
Limits: Rust subset limitations. | Translation is in the TCB. | Younger than hax in production use.
Firms using it: none listed
Sources: https://github.com/AeneasVerif/aeneas | https://arxiv.org/abs/2605.30106

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

Kani: Bounded model checker for Rust
====================================

Kani is AWS's bounded model checker for Rust. It proves absence of panics, undefined behaviour and violated assertions within loop bounds, with no specification language to learn, and is used across AWS's Rust libraries and the Rust standard library verification challenge.

Maintainer: AWS
Website: https://github.com/model-checking/kani
Category: Verified implementations
Targets: Rust, Rust standard library verification challenge, AWS Rust libraries
Approach: Bounded model checking (CBMC backend) for panics, memory safety and user assertions
Access: Open source (Apache-2.0 / MIT)
Status: Active
Strengths: Low effort, high value on unsafe and arithmetic code. | Concrete counterexamples. | AWS-backed, well maintained.
Limits: Bounded: no guarantee beyond the unwinding depth. | No functional correctness against a cryptographic spec. | Struggles with large state spaces.
Firms using it: none listed
Sources: https://github.com/model-checking/kani

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

CBMC: Bounded model checker for C, used on mlkem-native and s2n
===============================================================

CBMC is the bounded model checker behind Kani and the memory-safety proofs of mlkem-native and AWS s2n. It proves absence of memory errors and assertion failures in C within loop bounds.

Maintainer: Diffblue, AWS and community
Website: https://github.com/diffblue/cbmc
Category: Verified implementations
Targets: C, mlkem-native, s2n
Approach: Bounded model checking for memory safety and assertions
Access: Open source (BSD-4)
Status: Active, mature
Strengths: Mature and widely deployed. | Concrete counterexamples. | No spec needed for memory safety.
Limits: Bounded. | No functional correctness. | Modelling effort for harnesses.
Firms using it: none listed
Sources: https://github.com/diffblue/cbmc

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

CryptoLine: Verification of low-level arithmetic assembly
=========================================================

CryptoLine verifies straight-line arithmetic assembly such as bignum multiplication and NTT butterflies, and has been applied to OpenSSL, BoringSSL, wolfSSL and post-quantum NTT implementations.

Maintainer: Academia Sinica (Bow-Yaw Wang)
Website: https://github.com/fmlab-iis/cryptoline
Category: Verified implementations
Targets: Bignum and NTT assembly, OpenSSL, BoringSSL, wolfSSL, PQC NTTs
Approach: Algebraic and range reasoning on straight-line arithmetic code
Access: Open source
Status: Active research
Strengths: Handles large arithmetic kernels. | Applied to production libraries. | Complements SAW-style equivalence.
Limits: Straight-line code only. | Specialist tool. | Academic maintenance.
Firms using it: none listed
Sources: https://github.com/fmlab-iis/cryptoline

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

Verus: SMT-based verifier for Rust
==================================

Verus lets developers write specifications and proofs inside Rust and discharges them with an SMT solver, giving full functional correctness without a separate proof assistant.

Maintainer: CMU, Microsoft and community
Website: https://github.com/verus-lang/verus
Category: Verified implementations
Targets: Rust (systems and some cryptographic code)
Approach: Ghost specifications and SMT-discharged proofs in Rust itself
Access: Open source (MIT)
Status: Active
Strengths: Specs and code in one language. | High automation. | Active community.
Limits: SMT limits on nonlinear field arithmetic. | Requires writing Verus-flavoured Rust. | Less cryptographic precedent than hax.
Firms using it: none listed
Sources: https://github.com/verus-lang/verus

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

Lean 4 and Mathlib: The proof assistant the ZK verification ecosystem has standardised on
================================================================================

Lean 4 is the proof assistant behind nearly every ZK verification project funded in 2025 and 2026: Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, proven-zk, Nethermind's EVM model and StarkWare's Cairo proofs. Mathlib supplies the finite-field and polynomial mathematics, and AI proving tools now target it.

Maintainer: Lean FRO and the Mathlib community
Website: https://lean-lang.org
Category: Proof assistants and general verifiers
Targets: Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, EvmYul, Cairo AIR proofs
Approach: Interactive theorem prover with a small trusted kernel, a large mathematics library and a growing AI-prover ecosystem
Access: Open source (Apache-2.0)
Status: Active
Strengths: De facto standard for ZK proofs. | Mathlib depth for field and polynomial arithmetic. | Best AI-assistant support of any prover.
Limits: Proof engineering cost. | Fast-moving toolchain; pin versions. | Trusted axioms must be audited per project.
Firms using it: zkSecurity, Galois, Nethermind (Formal Verification team), Reilabs
Sources: https://lean-lang.org | https://blog.zksecurity.xyz/posts/introduction-to-interactive-theorem-provers/

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

Rocq (formerly Coq): Proof assistant behind Fiat-Crypto, SSProve, Garden and rocq-of-rust
================================================================================

Rocq, the renamed Coq, underpins Fiat-Crypto's verified field arithmetic, SSProve's computational proofs, Formal Land's Garden circuit framework and its rocq-of-rust and rocq-of-solidity translators. It is the main alternative to Lean for cryptographic verification.

Maintainer: Inria and the Rocq community
Website: https://rocq-prover.org
Category: Proof assistants and general verifiers
Targets: Fiat-Crypto, SSProve, Garden, rocq-of-rust, rocq-of-solidity
Approach: Interactive theorem prover based on the calculus of inductive constructions
Access: Open source (LGPL)
Status: Active
Strengths: Mature, stable, well documented. | Strong extraction to executable code. | Formal Land's Rust and Solidity translators.
Limits: ZK ecosystem momentum is with Lean. | Steeper syntax for newcomers. | Fewer circuit-specific libraries.
Firms using it: Formal Land
Sources: https://rocq-prover.org

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

Isabelle/HOL: Proof assistant used by Apple to verify corecrypto ML-KEM and ML-DSA
================================================================================

Isabelle/HOL is the prover Apple used with AutoCorres2, SAW and Cryptol to verify the ML-KEM and ML-DSA implementations in corecrypto (published 2026). It offers strong automation and a refinement methodology for C.

Maintainer: TU München and University of Cambridge
Website: https://isabelle.in.tum.de
Category: Proof assistants and general verifiers
Targets: C and ARM64 via AutoCorres2, Apple corecrypto
Approach: Higher-order logic with strong automation; refinement via AutoCorres2
Access: Open source (BSD)
Status: Active
Strengths: Powerful automation (sledgehammer). | AutoCorres2 for C refinement. | Industrial precedent (seL4, corecrypto).
Limits: Little ZK ecosystem presence. | Different culture and libraries from Lean/Rocq. | Refinement setups are heavyweight.
Firms using it: none listed
Sources: https://github.com/apple/corecrypto | https://isabelle.in.tum.de

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

F*: Dependently typed language behind HACL*, hax and DY*
========================================================

F* is the dependently typed language in which HACL* and libcrux proofs are written and the primary backend of hax. It combines proof-assistant expressiveness with SMT automation and extracts to C.

Maintainer: Microsoft Research and Inria
Website: https://fstar-lang.org
Category: Proof assistants and general verifiers
Targets: HACL*, hax (main backend), DY*, libcrux
Approach: Dependently typed effectful programming with SMT automation; extraction to C and OCaml
Access: Open source (Apache-2.0)
Status: Active
Strengths: Largest body of deployed verified crypto. | Automation via Z3. | Extraction to C.
Limits: Proof brittleness under solver changes. | Smaller community than Lean. | Not used for circuits.
Firms using it: Cryspen
Sources: https://fstar-lang.org

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

ACL2 (R1CS and PFCS books): Mature prime-field constraint verification with light tactics
================================================================================

ACL2 has a mature library for R1CS and prime-field constraint systems and an acl2-jolt project. zkSecurity's 2025 comparison found it the lightest on tactic effort among circuit frameworks, at the cost of a smaller ecosystem.

Maintainer: ACL2 community (Kestrel Institute)
Website: https://www.cs.utexas.edu/~moore/acl2/
Category: Proof assistants and general verifiers
Targets: R1CS, Prime-field constraint systems, acl2-jolt
Approach: First-order logic with strong automation; R1CS and PFCS libraries; acl2-jolt for Jolt circuits
Access: Open source (BSD)
Status: Mature, niche
Strengths: Least proof effort per gadget in published comparisons. | Long history in hardware verification.
Limits: Small ZK community. | First-order logic limits expressiveness. | Less interoperability with Lean projects.
Firms using it: none listed
Sources: https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/

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

K framework and KEVM: Executable semantics for the EVM and zkVM equivalence work
================================================================================

K is a semantics framework in which KEVM defines the EVM executably. Runtime Verification uses it in the Verified zkEVM program for the zkevm-harness and for proving equivalence between KEVM and Nethermind's Lean EvmYul model.

Maintainer: Runtime Verification
Website: https://kframework.org
Category: Proof assistants and general verifiers
Targets: EVM (KEVM), zkevm-harness, Lean backend for K
Approach: Rewriting-based semantics from which interpreters, symbolic executors and provers are derived
Access: Open source
Status: Active, mature
Strengths: Executable and provable from one definition. | KEVM is battle tested. | Lean backend bridges to the ZK ecosystem.
Limits: Specialist tooling. | Not a circuit verifier. | Heavy for small projects.
Firms using it: Runtime Verification
Sources: https://kframework.org | https://github.com/Verified-zkEVM/Overview

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

Certora Prover: SMT-based verification of smart contracts, including ZK verifier contracts
================================================================================

Certora Prover verifies smart contracts against rules written in CVL, on EVM, Solana, Move and Soroban. It is the tool to verify the on-chain verifier and bridge logic around a ZK system; it does not verify circuits.

Maintainer: Certora
Website: https://github.com/Certora/CertoraProver
Category: Proof assistants and general verifiers
Targets: Solidity, Vyper, Solana (Rust), Move, Soroban
Approach: Rule-based specification (CVL) discharged by SMT over bytecode
Access: Open source (2025)
Status: Active
Strengths: Production usage across DeFi. | Multi-chain. | Open source with commercial support.
Limits: Not cryptography-specific. | SMT timeouts on complex invariants. | Rules must be written and reviewed.
Firms using it: Certora
Sources: https://github.com/Certora/CertoraProver

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

zk.golf: circuit optimisation challenges with Lean 4 proofs of soundness and completeness
================================================================================

zk.golf is zkSecurity's competition to build the cheapest zero-knowledge circuits that are proven correct in Lean 4. Each challenge fixes a Lean specification; a submission is a Clean circuit plus a proof that it is sound and complete against it, kernel-checked in a sandbox (20-minute timeout, no native_decide, axiom allowlist). Challenges include SHA-256, Keccak-f[1600], RSA PKCS#1 v1.5 verification, secp256k1 scalar multiplication and GF(2) BLAKE3 and KangarooTwelve compression.

Maintainer: zkSecurity
Website: https://zk.golf
Category: Challenges and programs
Targets: R1CS over BN254, GF(2) hash compression track, Clean circuits
Approach: Fixed Lean interface and specification per challenge; submissions are Clean circuits plus kernel-checked proofs; score = allocations + constraints
Access: Open challenge; challenges repository public
Status: Active (launched 2026-07-02)
Strengths: Every leaderboard entry is a kernel-checked proof, not a claim. | Realistic targets: SHA-256, Keccak, RSA, secp256k1. | Designed for AI-agent participation under a fixed spec.
Limits: Challenge scope only; not an audit of your code. | Clean and Lean 4 required. | Young platform (July 2026).
Firms using it: zkSecurity
Sources: https://zk.golf | https://blog.zksecurity.xyz/posts/zkgolf/ | https://github.com/zksecurity/zk-golf-challenges

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

better.codes: the Proximity Prize soundness challenge with Lean 4 checked submissions
================================================================================

better.codes is an open autoresearch challenge built by the Ethereum Foundation Formal Verification team with Yukon and zkSecurity. A self-contained problem from the Proximity Prize (koalaIRS12, a Reed-Solomon proximity question that governs the provable soundness of hash-based SNARKs such as FRI, STIR and WHIR) is formalised in Lean 4, and solvers direct AI agents at raising the proven soundness lower bound. As of 2026-09-13 the bound stood at 68.07 bits against a 128-bit target, up from a 64-bit literature baseline, with 74 promoted submissions from 22 solvers.

Maintainer: Ethereum Foundation Formal Verification team, Yukon and zkSecurity
Website: https://better.codes
Category: Challenges and programs
Targets: koalaIRS12 proximity problem, FRI / STIR / WHIR soundness, Lean 4
Approach: A formalised open problem from the Proximity Prize; solvers point AI agents at improving the machine-checked lower bound; every submission is kernel-checked and promoted proofs are credited
Access: Open challenge; program terms on the site
Status: Active (launched 2026-08-20)
Strengths: Machine-checked progress on a bound that decides real SNARK security levels. | Public, dated, attributed results. | Demonstrates AI-assisted proving under kernel discipline.
Limits: A single problem, not a general tool. | Requires Lean 4 and proximity-testing expertise to contribute meaningfully. | Bound remains far from the 128-bit target.
Firms using it: zkSecurity
Sources: https://better.codes | https://blog.ethereum.org/en/2026/08/20/better-codes-challenge | https://proximityprize.org | https://www.yukon.org

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

Verified zkEVM program: The Ethereum Foundation program funding Lean verification of zkVMs and their proof systems
================================================================================

The Verified zkEVM program is the Ethereum Foundation initiative that funds and coordinates most of the ZK verification tooling on this index: Clean (zkSecurity), zkLean (Galois), Halva (Nethermind), ArkLib, LLZK (Veridise), the Sail RISC-V Lean model, KEVM equivalence work (Runtime Verification), VCV-io and hax's Lean backend (Cryspen), with a stated goal of formally verified zk(E)VMs by 2027.

Maintainer: Ethereum Foundation
Website: https://verified-zkevm.org
Category: Challenges and programs
Targets: Clean, zkLean, Halva, ArkLib, LLZK, Sail RISC-V Lean, KEVM equivalence, hax Lean backend
Approach: Grants and coordination for a formally verified, bug-free zk(E)VM stack, targeted for 2027
Access: Program; individual projects are open source
Status: Active
Strengths: Single source of truth for funded, interoperable projects. | Dated public milestones. | Independent reviews (for example of sp1-lean) published openly.
Limits: Ethereum-centric scope. | Program, not a tool. | Milestones can slip; check dates.
Firms using it: none listed
Sources: https://verified-zkevm.org | https://github.com/Verified-zkEVM/Overview | https://blog.ethereum.org/2025/12/18/zkevm-security-foundations

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

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

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](/frameworks/clean/), the Lean 4 circuit framework with sound-and-complete gadgets that Succinct's sp1-lean is built on, runs the [zk.golf](/frameworks/zk-golf/) verified-circuit competition, and co-built the [better.codes](/frameworks/better-codes/) soundness challenge with the Ethereum Foundation and Yukon. Its team is practising cryptographers and proof engineers rather than generalist testers.

Website: https://www.zksecurity.xyz
Headquarters: Remote-first (United States and Europe)
Focus: Formal verification and audits of zero-knowledge circuits, proof systems and cryptographic protocols; creator of Clean and zk.golf
Index position: #1 of 11
Services: Formal verification of ZK circuits and zkVM instruction sets in Lean 4 with Clean: specification writing, soundness and completeness proofs, CI-rechecked proof artifacts | Security audits of ZK circuits (Circom, Halo2, Plonky3, Noir, Cairo, gnark), proof-system implementations and verifier integrations | Cryptographic protocol and implementation review: MPC, FHE, post-quantum (ML-KEM, ML-DSA), TEEs | Specification and threat-model authoring for teams preparing a verification effort | Research and development engagements, including proof-system implementation and verified-circuit optimisation via zk.golf-style workflows
Tools: Clean, zk.golf, better.codes, sp1-lean, Lean 4 and Mathlib
Evidence: https://github.com/Verified-zkEVM/clean | https://blog.zksecurity.xyz/posts/clean-verified-zkvms/ | https://blog.zksecurity.xyz/posts/poseidon-clean/ | https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/ | https://blog.zksecurity.xyz/posts/zkgolf/ | https://blog.ethereum.org/en/2026/08/20/better-codes-challenge | https://reports.zksecurity.xyz/

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

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

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

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.

Website: https://veridise.com
Headquarters: Austin, Texas, United States
Focus: Automated ZK verification: Picus, LLZK, ZKAP; AuditHub platform; verified SP1 and RISC Zero components
Index position: #3 of 11
Services: Automated underconstraint detection on Circom, Halo2, Plonky3 and gnark via Picus and LLZK | ZK and smart-contract audits | Custom static analysis and verification tooling
Tools: Picus, LLZK, Coda
Evidence: https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/ | https://github.com/Veridise/Picus

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

Nethermind (Formal Verification team): formal verification services for cryptography and ZK
================================================================================

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.

Website: https://www.nethermind.io/formal-verification
Headquarters: London, United Kingdom
Focus: Lean and EasyCrypt verification: Halva (Halo2), Plonky3 circuits, SP1 chips, ZKsync verifier honesty proof
Index position: #4 of 11
Services: Halo2 and Plonky3 circuit verification in Lean | zkVM chip verification (SP1, Pico, OpenVM) | EasyCrypt proofs for verifiers and protocols | EVM semantics and equivalence proofs
Tools: Halva, sp1-lean, ArkLib, EasyCrypt, Lean 4 and Mathlib
Evidence: https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean | https://blog.succinct.xyz/nethermind-lean/

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

Formal Land: formal verification services for cryptography and ZK
=================================================================

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.

Website: https://formal.land
Headquarters: Paris, France
Focus: Rocq verification: Garden (circuits), rocq-of-rust, rocq-of-solidity, rocq-of-llzk
Index position: #5 of 11
Services: Circuit verification in Rocq via Garden and LLZK | Rust verification via rocq-of-rust | Solidity verifier and contract verification via rocq-of-solidity
Tools: Garden, LLZK, Rocq (formerly Coq)
Evidence: https://github.com/formal-land/garden | https://formal.land

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

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

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.

Website: https://cryspen.com
Headquarters: Berlin, Germany and Paris, France
Focus: hax and libcrux: verified Rust post-quantum implementations; hax Lean backend for the Verified zkEVM program
Index position: #6 of 11
Services: Verified Rust implementations of classical and post-quantum primitives | Protocol verification (Signal PQXDH, MLS) | hax-based verification of client Rust code
Tools: hax, F*, ProVerif, SSProve
Evidence: https://github.com/cryspen/hax | https://cryspen.com/post/ml-kem-verification/

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

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

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.

Website: https://reilabs.io
Headquarters: Warsaw, Poland
Focus: Lean 4 verification of Noir (Lampe) and gnark (proven-zk); verified Worldcoin circuits
Index position: #7 of 11
Services: Noir and Aztec circuit verification via Lampe | gnark circuit verification via proven-zk | Lean 4 proof engineering
Tools: Lampe, proven-zk and gnark-lean-extractor, Lean 4 and Mathlib
Evidence: https://github.com/reilabs/lampe | https://github.com/reilabs/proven-zk

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

Runtime Verification: formal verification services for cryptography and ZK
==========================================================================

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.

Website: https://runtimeverification.com
Headquarters: Urbana, Illinois, United States
Focus: K framework, KEVM, zkevm-harness, EVM equivalence with Lean models
Index position: #8 of 11
Services: Executable semantics and equivalence proofs for VMs | Smart-contract formal verification with K | zkEVM harness and conformance work
Tools: K framework and KEVM
Evidence: https://kframework.org | https://github.com/Verified-zkEVM/Overview

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

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

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.

Website: https://www.certora.com
Headquarters: Tel Aviv, Israel and United States
Focus: Certora Prover for smart contracts on EVM, Solana, Move and Soroban
Index position: #9 of 11
Services: Rule-based contract verification (CVL) | Continuous verification in CI | Contract audits
Tools: Certora Prover
Evidence: https://github.com/Certora/CertoraProver

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

Trail of Bits: formal verification services for cryptography and ZK
===================================================================

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.

Website: https://www.trailofbits.com
Headquarters: New York, United States
Focus: Cryptography and ZK audits; Circomspect static analyzer; ZKDocs
Index position: #10 of 11
Services: ZK and cryptography audits | Static analysis tooling (Circomspect) | Implementation of post-quantum algorithms (pyca/cryptography)
Tools: Circomspect
Evidence: https://github.com/trailofbits/circomspect

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

Symbolic Software: formal verification services for cryptography and ZK
=======================================================================

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.

Website: https://symbolic.software
Headquarters: Paris, France
Focus: Protocol-level verification (Verifpal) and cryptographic audits; author of the 2026 Verification Theatre paper
Index position: #11 of 11
Services: Symbolic protocol modelling and analysis | Cryptographic implementation audits | Verification-boundary reviews of verified code
Tools: Verifpal, Tamarin, ProVerif
Evidence: https://eprint.iacr.org/2026/192 | https://verifpal.com

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

What is Circuit soundness? Definition and why it matters
========================================================

A circuit is sound with respect to a specification if every witness that satisfies its constraints also satisfies the specification, so a malicious prover cannot produce an accepting proof of a false statement.

Detail: Soundness is the property that rules out underconstrained circuits, and it is what most ZK verification efforts prove first. Because the adversary chooses the witness, a soundness argument must consider every satisfying assignment, not only the ones an honest witness generator produces. Soundness alone is not enough: a circuit with no satisfying assignments is vacuously sound. That is why Clean and zk.golf require completeness alongside it, and why a soundness-only theorem should be read together with tests showing the circuit accepts honest inputs.

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

What is Circuit completeness? Definition and why it matters
===========================================================

A circuit is complete with respect to a specification if every input the specification allows has a satisfying witness, so an honest prover is never blocked from proving a true statement.

Detail: Completeness failures are availability bugs: a wallet that cannot spend, a bridge that cannot finalise, a rollup that cannot include a legitimate transaction. They are less discussed than soundness bugs because they do not lose funds directly, but they are common when constraints are tightened during a fix. A sound-and-complete theorem pins the circuit to its specification exactly, which is what allows untrusted optimisation, including by AI agents, without loss of correctness.

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

What is Underconstrained circuit? Definition and why it matters
===============================================================

A circuit whose constraints admit witnesses outside the specification, typically because a value computed during witness generation is never pinned down by a constraint. It is the dominant class of exploitable ZK bug.

Detail: In Circom the classic form is a `<--` assignment without a matching `===` constraint; in Halo2 it is a cell that is assigned but not gated; in any system it is a missing range check, a missing boolean check or a division by a possibly-zero value. Automatic tools (Picus, CIVER, NAVe) detect many instances by checking that outputs are uniquely determined by inputs; a soundness proof rules out all of them.

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

What is Overconstrained circuit? Definition and why it matters
==============================================================

A circuit that rejects inputs the specification allows, so honest provers fail. It is the failure of completeness.

Detail: Overconstraint often appears after a security fix adds a constraint that is stricter than intended, or when a gadget assumes a range the caller does not guarantee. Completeness proofs and honest-path test vectors catch it.

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

What is Symbolic vs computational model? Definition and why it matters
======================================================================

The symbolic (Dolev-Yao) model treats cryptographic primitives as perfect black boxes and searches for logical attacks automatically; the computational model reasons about probabilistic polynomial-time adversaries and concrete security bounds, matching cryptographers' proofs.

Detail: Symbolic tools (Tamarin, ProVerif, Verifpal) are fast and find protocol-logic flaws over unbounded sessions but cannot see weaknesses inside primitives. Computational tools (EasyCrypt, CryptoVerif, SSProve) give the guarantee a cryptographer expects at far higher effort. Squirrel attempts to combine them. Most serious protocol analyses use one of each.

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

What is Specification gap? Definition and why it matters
========================================================

A mismatch between the property that was formally proved and the property that was actually needed, so a valid proof fails to cover real behaviour.

Detail: The public example is sp1-lean's JALR theorem, which assumed a 4-byte-aligned jump target and therefore did not cover legitimate programs; the Ethereum Foundation disclosed the bug in May 2026. The Verification Theatre paper documents the same phenomenon in verified ML-KEM code. Reading the theorem statements and assumptions is as important as checking that the proof compiles.

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

What is Trusted computing base and verification boundary? Definition and why it matters
================================================================================

Everything that must be correct for a proof to mean what it claims: the prover kernel, the axioms used, the extraction or translation from code to model, the specification itself, and any unverified glue code. The edge of that set is the verification boundary.

Detail: A responsible verification deliverable lists its TCB explicitly: which Lean axioms, whether `native_decide` was used, how constraints were extracted from the codebase, and what surrounding code is unverified. zk.golf enforces an axiom allowlist for exactly this reason. Ask every vendor for the boundary in writing.

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

What is Proof assistant vs SMT-based verifier? Definition and why it matters
============================================================================

A proof assistant (Lean, Rocq, Isabelle, F*) checks human- or AI-written proofs against a small kernel and can express arbitrary mathematics; an SMT-based verifier (Picus, CIVER, Certora Prover, Kani) discharges properties automatically but only within decidable fragments and may return 'unknown'.

Detail: The practical trade: SMT tools give results in minutes with no proof engineering and no specification (for determinism) but time out on large or nonlinear problems; proof assistants scale to any property and any size at the cost of expert time. Mature pipelines use both: automatic checks first, proofs for what matters most.

Source page: https://sorryfree.com/glossary/proof-assistant-vs-smt/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13

What is Bounded model checking? Definition and why it matters
=============================================================

Exhaustive exploration of all program executions up to a fixed depth or loop bound, reporting concrete counterexamples; sound only within the bound.

Detail: Kani and CBMC are the cheapest verification most cryptographic Rust and C code will ever get: memory safety, absence of panics and user assertions with no specification language. They are not proofs of correctness against a cryptographic spec.

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

What is Equivalence checking? Definition and why it matters
===========================================================

Proving that two artifacts compute the same function, for example optimised assembly against a Cryptol reference, or the KEVM semantics against a Lean EVM model.

Detail: Equivalence checking is how existing optimised code gets verified without rewriting it. Its limit is that the reference must itself be trusted or verified.

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

What is Refinement? Definition and why it matters
=================================================

A relation showing that an implementation's behaviours are a subset of a more abstract specification's behaviours, layered so low-level code refines a high-level model.

Detail: Refinement is the methodology of seL4, AutoCorres2 and Apple's corecrypto proofs, and of Coda's refinement types for circuits. It lets a proof be split into stages that different people can own.

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

What is Constant-time verification? Definition and why it matters
=================================================================

Proving that a program's control flow and memory access pattern do not depend on secret data, so timing and cache side channels cannot leak keys.

Detail: Jasmin checks it in the compiler; HACL* proves secret independence in F*; AWS-LC's assembly is verified constant-time. Functional correctness proofs do not imply it: the KyberSlash timing bugs were in code that computed the right answer.

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

What is Arithmetization (R1CS, PLONKish, AIR)? Definition and why it matters
============================================================================

The encoding of a computation as polynomial constraints over a finite field: rank-1 constraint systems (Groth16, gnark), PLONKish gates with copy and lookup constraints (Halo2), or algebraic intermediate representations over execution traces (STARKs, Plonky3, SP1).

Detail: Verification frameworks are tied to arithmetizations: Picus and Ecne to R1CS, Halva to PLONKish, Clean primarily to AIR with PLONK and R1CS support, StarkWare's proofs to the Cairo AIR. Check the framework page for the exact model before assuming coverage.

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

What is Extraction (code to model)? Definition and why it matters
=================================================================

The step that turns a deployed circuit or program into the object a prover reasons about, whether by instrumenting synthesis (Halva), compiling to an IR (LLZK), or translating source (hax, Aeneas).

Detail: Extraction is part of the trusted computing base unless the extractor is itself verified. Frameworks that avoid it (Clean, where the Lean circuit is the source; CIVER, which runs inside the compiler) trade it for a code-generation or correspondence step instead.

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

What is Witness generation vs constraints? Definition and why it matters
========================================================================

Witness generation is the program that computes a satisfying assignment for honest inputs; constraints are what the verifier actually checks. Bugs arise when the two disagree.

Detail: Most underconstraint bugs are exactly a disagreement: witness generation computes the intended value, constraints fail to enforce it. zkFuzz targets this gap directly; soundness proofs make the constraints authoritative.

Source page: https://sorryfree.com/glossary/witness-generation-vs-constraints/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13

Formal verification scoping checklist for ZK circuits and cryptographic code
============================================================================

What to agree before a formal verification engagement and what to demand at handover: a written specification, the exact theorems (soundness and completeness), the trusted computing base, the link between the model and the shipped code, a CI recheck command, and an audit plan for everything outside the proof.

Before engaging anyone: A written specification exists: public and private inputs, encodings, field and integer ranges, and explicit assumptions. If it does not, the first deliverable is the specification. | The target is chosen by consequence: a range check, hash gadget, instruction chip or verifier whose failure would matter, not the easiest component. | Automatic tools have already run (Circomspect, Picus or CIVER, Kani or CBMC on the prover code) so proof effort goes to what they cannot answer.
Theorems to demand: Soundness stated over the specification's domain, quantifying over every satisfying witness, not the honest witness generator. | Completeness, or a written reason it is out of scope and a test suite covering the honest path. | For multi-table or zkVM systems, a whole-system statement (Clean Channels, sp1-lean style), not only per-chip theorems. | For proof systems, which components are covered (sum-check, FRI, Fiat-Shamir) and at what security level.
Trusted computing base: The prover and version pinned (Lean toolchain, Mathlib commit); axioms listed; no `native_decide` or an explicit justification. | The extraction or translation step named (Halva synthesis hook, LLZK, hax, Aeneas) and whether it is verified or trusted. | A mapping from the verified model to the deployed constraints and verifier code, with the compiler, codegen and integration gaps listed.
Handover: Proof sources in a repository with a single command that rechecks them in CI, and CI actually running it. | A list of unproved obligations, sorries and trusted lemmas with owners and dates. | A maintenance plan: what happens to the proofs when the circuit or specification changes.
Outside the proof: An audit plan for the protocol layer, verifier integration, on-chain contract and deployment, since proofs cover none of these. | Constant-time and side-channel review for any implementation-level work; functional correctness does not imply it. | A reading of the theorem statements by someone who did not write them, specifically looking for assumptions that exclude real inputs (the SP1 JALR pattern).

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

Formal verification of ZK circuits and cryptography: frequently asked questions
===============================================================================

Answers to the questions teams ask before commissioning formal verification: what it proves, how it differs from an audit, which framework fits which proof system, what it costs, and how to read the assumptions.

What does formal verification of a ZK circuit actually prove?: A machine-checked theorem that the circuit's constraints match a written specification. The strong form is two theorems: soundness (every satisfying witness meets the spec, so no false proof is accepted) and completeness (every valid input has a witness, so honest provers are never blocked). Automatic tools such as Picus prove a weaker property, that outputs are uniquely determined by inputs, without a specification.
How is formal verification different from an audit?: An audit is a time-boxed expert review that finds bug classes authors are blind to and reports on a specific commit; it does not prove absence of bugs. Formal verification proves a stated property for all inputs but only for the property stated and only inside its trusted computing base. Mature teams use both: an audit for the specification, integration and deployment surfaces, proofs for the gadgets and instruction sets that matter most.
Which framework should I use for my proof system?: AIR or Plonky3-style tables and zkVM chips: Clean (or sp1-lean if you are on SP1). Halo2: Halva. Noir: Lampe for proofs, NAVe for automatic checks. gnark: proven-zk. Circom: Picus, CIVER and Circomspect for automatic checks, Garden or Clean's forthcoming LLZK frontend for proofs. Cairo: StarkWare's Lean proofs cover the VM itself. Proof-system components (sum-check, FRI, Fiat-Shamir): ArkLib.
Why is everything in Lean 4 now?: The Ethereum Foundation's Verified zkEVM program funded most 2025 and 2026 circuit and proof-system verification in Lean 4 (Clean, zkLean, Halva, ArkLib, sp1-lean), StarkWare and Reilabs chose it independently, Mathlib supplies the field and polynomial mathematics, and AI proving tools target it. Rocq remains strong for implementation verification (Fiat-Crypto, Formal Land) and F* for HACL* and hax.
Do I need completeness or is soundness enough?: You need both if a rejected valid input is a problem, which is true for wallets, bridges, rollups and anything with liveness requirements. Soundness alone is satisfied by an unsatisfiable circuit, so a soundness-only result must be paired with honest-path tests. Clean, zk.golf, Garden and CIVER's post-condition mode state completeness explicitly.
How much does formal verification cost and how long does it take?: Automatic checks (Circomspect, Picus, Kani) take hours to days of engineer time. A sound-and-complete proof of a hash gadget such as Poseidon or SHA-256 in Clean is weeks of proof engineering; a zkVM instruction set is months and ongoing. Costs scale with the size of the specification, not the size of the code, so writing the specification first is the best cost control.
Can verified code still have bugs?: Yes, outside the verified boundary. The February 2026 Verification Theatre paper found 13 vulnerabilities in verified libraries, four inside code covered by proofs, all in properties that were never specified. The SP1 JALR bug was inside a proven opcode whose theorem excluded misaligned targets. Read the theorem statements and the trusted computing base, and audit what they leave out.
Can AI agents write these proofs?: Increasingly. better.codes measures AI-driven progress on a real soundness bound with the Lean kernel as judge, zk.golf publishes an agent API for verified circuit optimisation, and the May 2026 Rust-to-Lean pipeline paper used AI provers on Plonky3 and RISC Zero code. The kernel check is what makes AI-written proofs trustworthy; AI-written specifications still need human review.
Which firms deliver formal verification for ZK and cryptography?: In the order this index lists them: zkSecurity (Clean, zk.golf, better.codes), Galois (Cryptol/SAW, zkLean), Veridise (Picus, LLZK), Nethermind (Halva, SP1, EasyCrypt), Formal Land (Rocq, Garden), Cryspen (hax, libcrux), Reilabs (Lampe, proven-zk), Runtime Verification (K), Certora (contracts), Trail of Bits (Circomspect, audits) and Symbolic Software (Verifpal, protocol analysis).
What about post-quantum implementations?: Verified ML-KEM and ML-DSA implementations exist in libjade (Jasmin/EasyCrypt), libcrux (hax/F*), AWS-LC (SAW, NSym, HOL Light), mlkem-native (CBMC plus s2n-bignum) and Apple corecrypto (Isabelle, SAW). If you ship your own, the relevant frameworks are Jasmin, hax, Cryptol/SAW, CryptoLine and CBMC, and the firms are Cryspen, Galois and Formosa Crypto collaborators.

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

Formal verification in ZK and cryptography: timeline of releases, proofs and findings (2025-2026)
================================================================================

Dated milestones in formal verification of zero-knowledge circuits and cryptographic implementations: framework releases, completed proofs, bugs found by verification, and bugs that escaped it.

2026-09-09: Nethermind archives Horus, its SMT verifier for Cairo 0 — Lean-based verification of the Cairo AIR by StarkWare is now the only maintained route for Cairo. (https://github.com/NethermindEth/horus-checker)
2026-08-20: Ethereum Foundation, Yukon and zkSecurity launch better.codes — An open autoresearch challenge to raise the Lean-checked soundness bound of the koalaIRS12 proximity problem; by 2026-09-13 the bound rose from 64 to 68.07 bits. (https://blog.ethereum.org/en/2026/08/20/better-codes-challenge)
2026-08-01: zkSecurity releases zk-skills with circom-auditor — Open-source security skills for coding agents, reporting 66 of 70 known bugs found on the zkbugs benchmark. (https://blog.zksecurity.xyz/posts/circom-auditor/)
2026-07-23: StarkWare verifies the STRK20 privacy pool in Lean 4 — More than 230 theorems using the Cairo AIR methodology. (https://starkware.co/blog/strk20-formal-verification/)
2026-07-02: zkSecurity launches zk.golf — Circuit optimisation challenges where every submission carries a kernel-checked Lean proof of soundness and completeness. (https://blog.zksecurity.xyz/posts/zkgolf/)
2026-06-05: Clean adds Channels for multi-table and zkVM verification — Presented at ZKProof 8; lifts per-table soundness to whole-system soundness for LogUp-style interactions. (https://blog.zksecurity.xyz/posts/clean-verified-zkvms/)
2026-06-03: StarkWare and Avigad publish Lean 4 soundness of the S-two Cairo AIR — Satisfying the AIR implies a correct Cairo execution, for both Stone and S-two. (https://arxiv.org/abs/2606.04311)
2026-05-28: Rust-to-Lean pipeline verifies Plonky3 FRI folding and RISC Zero Merkle checks — hax, Aeneas, ArkLib, CompPoly and AI provers combined on production prover code. (https://arxiv.org/abs/2605.30106)
2026-05-20: Ethereum Foundation discloses SP1 Hypercube JALR bug and audits sp1-lean — 51 of 62 opcodes fully proven; the JALR theorem's alignment assumption is the public case study in specification gaps. (https://zkevm.ethereum.foundation/blog/sp1-fv)
2026-05-04: zkSecurity proves circomlib's Poseidon sound and complete in Clean — BN254 primality discharged via a Pratt certificate in CompPoly. (https://blog.zksecurity.xyz/posts/poseidon-clean/)
2026-05-01: Apple publishes formal verification of corecrypto ML-KEM and ML-DSA — Isabelle/HOL with AutoCorres2, plus SAW and Cryptol, over C and ARM64. (https://github.com/apple/corecrypto)
2026-04-08: Veridise releases LLZK v1.0 — Circom and Halo2 frontends; Picus, zkLean and R1CS backends; Rocq via Formal Land. (https://veridise.com/blog/veridise-announcements/llzk-v1-0-a-new-phase-for-zk-shared-infrastructure/)
2026-02-15: Verification Theatre paper reports 13 bugs in verified libcrux and hpke-rs — Four inside verified ML-KEM and ML-DSA code, all outside what the specifications stated. (https://eprint.iacr.org/2026/192)
2025-12-18: Ethereum Foundation publishes the L1 zkEVM security roadmap — 100-bit provable security by May 2026, 128-bit and a formal soundness argument for recursion by end of 2026. (https://blog.ethereum.org/2025/12/18/zkevm-security-foundations)
2025-11-19: zkSecurity publishes a hands-on comparison of six circuit FV frameworks — ACL2, acl2-jolt, Garden, zk-lean, sp1-lean and Clean evaluated on reproducibility and practical proving. (https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/)
2025-10-09: Nethermind and Succinct announce Lean verification of SP1 Hypercube core chips — RV64 chip constraints proved against the Sail RISC-V model, built on Clean. (https://blog.succinct.xyz/nethermind-lean/)
2025-07-02: Nethermind's Halva finds a critical bug in Scroll's deprecated Keccak Halo2 circuit — The clearest public case of a proof-assistant framework finding a critical circuit bug. (https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean)
2025-03-27: zkSecurity introduces Clean — A Lean 4 DSL for ZK circuits with soundness and completeness proofs per gadget. (https://blog.zksecurity.xyz/posts/clean/)

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