As you likely know, zero knowledge proofs are coming to Tezos.

Here are some links:

But how can you be sure that the R1CS gadgets are correct? R1CS gadgets serve to define zero-knowledge computations, but they can be hard to audit and it is easy to make mistakes.

At Kestrel Institute (www.kestrel.edu) we are working on formal verification of R1CS gadgets, in order to help bring formally verified zero knowledge proofs to Tezos.

To formally verify R1CS gadgets we (1) write a specification in the theorem prover, (2) lift the R1CS into logic, and (3) connect the two with a mechanized formal proof of functional equivalence. The proof effectively tests the gadget with every possible input.

We are using the ACL2 theorem prover (ACL2 Version 8.3), which is based on a subset of Common Lisp for which a formal logic is defined. This means programs can be both executed and reasoned about in the same language, which can also express high-level declarative specifications.

If you would like to check out the work please see

R1CS:

`https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=R1CS____R1CS`

Some specifications:

`https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ZCASH____ZCASH`