Coda
Direct answerCoda 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 (2026-09-13)
- Research (2023), not actively developed
What Coda does
Coda is historically important: it showed that functional correctness of circomlib-style gadgets is provable with modest effort. Its ideas live on in Veridise's tooling and in the Lean frameworks.
Where it is strong
- Clear methodology paper.
- Found real bugs.
- Refinement types keep specs close to code.
Limits and caveats
- Requires rewriting circuits in Coda.
- No active maintenance.
- Coq only.
When to choose it
Read the paper for the methodology; use Clean, Garden or zkLean for new work.
Who works with Coda
Top-listed for circuit verification work: zkSecurity
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
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, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Ecne, NAVe, Verified Cairo AIR (Stone and S-two).