Formal methods for zero knowledge circuits

Zero knowledge circuits facilitate the construction of zero-knowledge proofs (ZKPs) by describing computations as finite field equations. However, logical errors in these circuits can lead to significant security vulnerabilities in software that uses ZKPs. Isil Dillig (UT-Austin) makes a case for applying formal methods to zero knowledge circuits and describes two of recent projects in this space. She describes a new technique for verifying an important property of ZK circuits as well as a new decision procedure for the theory of (prime-order) finite fields.

About the presenter

Isil is a Professor of Computer Science at UT Austin where she leads the UToPiA research group and a co-founder of Veridise, a blockchain security start-up. Her research interests are primarily in programming languages and formal methods, focusing mostly on program synthesis and software verification. Her research has won various distinguished paper awards, including at POPL, PLDI, OOPSLA, and others. About a16z crypto research a16z crypto research is a multidisciplinary lab that works closely with our portfolio companies and others toward solving the important problems in the space, and toward advancing the science and technology of the next generation of the internet.

More about us:

a16z.com/2022/04/21/announcing-a16z-crypto-research