Formal Verification of R1CS Project

Team

• Eric McCarthy (PI)
• Alessandro Coglio
• Eric Smith

Goals

The goal of the Formal Verification of R1CS project is to lift R1CS circuits (Rank 1 Constraint Systems)[1] into logic and to prove them equivalent to specifications written in the ACL2 theorem prover.

Status

We have extended our Axe toolkit to support “lifting” R1CS circuits into a higher-level logical representation suitable for reasoning and proof. We have also used Axe to prove the main correctness theorems for R1CS circuits with thousands of variables and thousands of constraints. We are working on scaling Axe to even larger circuits.

We write our specifications in the ACL2 theorem prover. We have recently written formal specifications for many small R1CS “gadgets,” for elliptic curve arithmetic and curve conversions, and for the MiMC, Blake2s, and Blake-256 hash functions. We are working on specifying Pedersen hashes.

The main R1CS circuits that we are currently formally verifying are those used by Semaphore. We have formally verified many small gadgets and some larger ones such as Montgomery curve arithmetic, birational equivalence conversions between Montgomery and Twisted Edwards curves, and MiMC hash in Feistel mode.

Inquiries

If you are interested in having your R1CS circuits/gadgets formally verified, please contact us!

Footnotes

[1] For a succinct definition of R1CS, see section 2.1 of Aurora: Transparent Succinct Arguments for R1CS. For a more conversational introduction in context, see Gates to R1CS in Quadratic Arithmetic Programs: from Zero to Hero.

Publications

Formal Verification of Zero-Knowledge Circuits
Alessandro Coglio, Eric McCarthy, Eric Smith
November 2023
18th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023)
{Description of our work to date on formally verifying zero-knowledge circuits, explaining how the approach has evolved based on its application to different use cases.}