Compositional Formal Verification of Zero-Knowledge Circuits

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

Paper 2023/1278 Original: eprint.iacr.org/2023/1278 ↗

Compositional Formal Verification of Zero-Knowledge Circuits

Alessandro Coglio

Eric McCarthy

Eric Smith

Collin Chin

Pranav Gaddamadugu

Michel Dellepere

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.
History: 2023-08-24: last updated; 2023-08-24: published
Short URL: https://ia.cr/2023/1278
License: https://creativecommons.org/licenses/by/4.0/

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}
}