There are a number of compilers and tools for generating R1CS programs for use in zero-knowledge proofs. These tools are generally not formally verified, nor do they generate formal proofs, and it is unsettling to depend on the resulting R1CS for high-value or sensitive transactions. R1CS can be difficult to understand by a human. Additionally, people can write programs directly in R1CS, and those programs are also in need of formal verification.
We have built an initial formal model of R1CS in the ACL2 theorem prover, and we have formalized a small number of R1CS gadgets. We have also developed prototype technology for lifting R1CS programs into a logical representation in ACL2. This enables people to prove things about the programs, such as functional correctness with respect to a specification written in ACL2.
The underlying technology is based on the ACL2 theorem prover and the Axe verification toolkit, which we have been using and developing for a number of years to verify Java bytecode implementations of cryptographic primitives and other code.
We would like to improve this technology to handle more R1CS patterns, and to scale the technology so that it can verify larger R1CS programs such as SHA-256, elliptic curve arithmetic, and others.
Along the way, we will develop a standalone tool that can statically check most real-world R1CS programs for: unsatisfiability; unconstrained output variables; non-circuit-derived constructs; and constructs that introduce nondeterminism. Note that this tool will be sound but not complete; the tool will report "unknown" for some inputs.
Besides the important work of verifying that R1CS circuits correctly implement specified functionality, and the standalone checker mentioned above, this work will enable future tools such as:
Equivalence checking, where an R1CS programmer can try out an optimization idea and get a quick answer on whether the optimized circuit is equivalent.
Automatic optimizer, a tool that applies verified optimization rules to make an equivalent circuit that is smaller. This would be based on our existing high-performance rewriter.