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