Paper 2023/1278

Compositional Formal Verification of Zero-Knowledge Circuits

Alessandro Coglio, Aleo Systems, Inc., Kestrel Institute
Eric McCarthy, Aleo Systems, Inc., Kestrel Institute
Eric Smith, Kestrel Institute
Collin Chin, Aleo Systems, Inc.
Pranav Gaddamadugu, Aleo Systems, Inc.
Michel Dellepere, Aleo Systems, Inc.
Abstract

We provide a preliminary report of our ongoing work in formally defining and verifying, in a compositional way, the R1CS gadgets generated by Aleo's snarkVM. The approach is applicable to other systems that generate gadgets in a similar manner, and that may use non-R1CS representations.

Metadata
Available format(s)
PDF
Category
Applications
Publication info
Preprint.
Keywords
zero-knowledge circuitsformal verificationtheorem provingR1CS constraints
Contact author(s)
acoglio @ aleo org
ericm @ aleo org
eric smith @ kestrel edu
collin @ aleo org
pranav @ aleo org
mdellepere @ aleo org
History
2023-08-28: approved
2023-08-24: received
See all versions
Short URL
https://ia.cr/2023/1278
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/1278,
      author = {Alessandro Coglio and Eric McCarthy and Eric Smith and Collin Chin and Pranav Gaddamadugu and Michel Dellepere},
      title = {Compositional Formal Verification of Zero-Knowledge Circuits},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/1278},
      year = {2023},
      url = {https://eprint.iacr.org/2023/1278}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.