Formal verification of zero knowledge gadgets

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 ( 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
Some specifications:


Hello, I think formal verification of cryptography is very important. How does your work compare to the Fiat-Crypto project and in particular to their recent work entitled “High-assurance field inversion for pairing-friendly primes” (paper, presentation)?

The work we are doing for Tezos is post-hoc verification of R1CS code. The Fiat-Crypto work is synthesis of C code. The C code will be part of the codebase used to generate zero-knowledge proofs that someone ran the R1CS code correctly on their secret inputs, but does not address correctness of the R1CS code.