[Resource Topic] 2023/1278: Compositional Formal Verification of Zero-Knowledge Circuits

Welcome to the resource topic for 2023/1278

Compositional Formal Verification of Zero-Knowledge Circuits

Authors: Alessandro Coglio, Eric McCarthy, Eric Smith, Collin Chin, Pranav Gaddamadugu, Michel Dellepere


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.

ePrint: https://eprint.iacr.org/2023/1278

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .