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