Formal methods for zero knowledge circuits with Isil Dillig | a16z crypto research talks

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
More from the a16z crypto team
Subscribe to our 'web3 weekly newsletter': a16zcrypto.substack.com
Listen to our 'web3 with a16z' podcast: a16zcrypto.com/web3-with-a16z-podcast/
Read more of our work: a16zcrypto.com