Compositional Formal Verification of Zero-Knowledge Circuits

Alessandro Coglio; Eric McCarthy; Eric Smith; Collin Chin; Pranav Gaddamadugu; Michel Dellepere

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 circuits formal verification theorem proving R1CS 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: 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},
      note = {\url{https://eprint.iacr.org/2023/1278}},
      url = {https://eprint.iacr.org/2023/1278}
}