The goal of the Formal Verification of R1CS project is to lift R1CS circuits (Rank 1 Constraint Systems) into logic and to prove them equivalent to specifications written in the ACL2 theorem prover.
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
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.
If you are interested in having your R1CS circuits/gadgets formally verified,
please contact us!
 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.