Paper 2023/547

Certifying Zero-Knowledge Circuits with Refinement Types

Junrui Liu, University of California, Santa Barbara
Ian Kretz, The University of Texas at Austin
Hanzhi Liu, University of California, Santa Barbara, Veridise Inc.
Bryan Tan, Veridise Inc.
Jonathan Wang, Axiom
Yi Sun, Axiom
Luke Pearson, Polychain Capital
Anders Miltner, Simon Fraser University
Işıl Dillig, The University of Texas at Austin, Veridise Inc.
Yu Feng, University of California, Santa Barbara, Veridise Inc.

Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application through a rich refinement type system. One of the key challenges in formally verifying ZK applications is that they require reasoning about polynomial equations over large prime fields that go beyond the capabilities of automated theorem provers. Coda mitigates this challenge by generating a set of Coq lemmas that can be proven in an interactive manner with the help of a tactic library. We have used Coda to re-implement 79 arithmetic circuits from widely-used Circom libraries and applications. Our evaluation shows that Coda makes it possible to specify important and formally verify correctness properties of these circuits. Our evaluation also revealed 6 previously-unknown vulnerabilities in the original Circom projects.

Available format(s)
Publication info
zero knowledgeverification
Contact author(s)
junrui @ cs ucsb edu
kretz @ cs utexas edu
hanzhi @ ucsb edu
bryan @ veridise com
jonathanpwang @ protonmail com
yi sun @ post harvard edu
luke @ polychain capital
miltner @ cs sfu ca
isil @ cs utexas edu
yufeng @ cs ucsb edu
2023-08-30: last of 2 revisions
2023-04-18: received
See all versions
Short URL
Creative Commons Attribution


      author = {Junrui Liu and Ian Kretz and Hanzhi Liu and Bryan Tan and Jonathan Wang and Yi Sun and Luke Pearson and Anders Miltner and Işıl Dillig and Yu Feng},
      title = {Certifying Zero-Knowledge Circuits with Refinement Types},
      howpublished = {Cryptology ePrint Archive, Paper 2023/547},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.