# Formal Verification of R1CS Project

## Team

## Goals

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

We will extend our Axe toolkit to support "lifting" R1CS circuits into a higher-level logical representation suitable for reasoning and proof. We will write specifications in the ACL2 theorem prover. To connect the two, we will use the Axe equivalence checker.

The first few R1CS "gadgets" that we will formally verify are those that are used by roll_up.

For example, R1CS that implement the following algorithms:

- MiMC hash
- Pedersen hash
- Blake2 hash
- EdDSA (Edwards-curve Digital Signature Algorithm)
- Sparse Merkle Tree operations

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

[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.