# 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)