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.
- Maintainer
- Formal Land
- Website
- https://github.com/formal-land/garden
- Repository
- https://github.com/formal-land/garden
- Category
- ZK circuit verification
- Targets
- CircomPlonky3LLZK
- Approach
- Rocq (Coq) proofs of determinism, functional correctness and completeness
- Access
- Open source
- Status (2026-09-13)
- Active
What Garden does
Garden is the Rocq counterpart to the Lean frameworks: the same properties, a different prover and a team that also maintains rocq-of-rust and rocq-of-solidity, so a client can verify the circuit, the Rust prover code and the Solidity verifier in one ecosystem.
Where it is strong
- States completeness explicitly.
- Same ecosystem as rocq-of-rust and rocq-of-solidity.
- LLZK backend gives it Halo2 reach.
Limits and caveats
- 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.
When to choose it
Choose Garden when your team or partner is Rocq-native or when you want Rust and Solidity verified alongside the circuit.
Who works with Garden
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile Website ↗
Related frameworks in ZK circuit verification
Clean, sp1-lean, zkLean, Halva, Picus, LLZK, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).