Paper 2023/1278
Compositional Formal Verification of Zero-Knowledge Circuits
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)
- 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
-
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} }