A16Z hosts Isil Dillig: Formal Methods for Zero-Knowledge Systems

Veridise
Veridise
Published in
7 min readJan 7, 2025

Isil Dillig, President and Co-founder of Veridise, took the stage at an a16z crypto event to deliver a comprehensive presentation on Formal Methods for Zero-Knowledge Circuits.

Her talk dives deep into the world of ZK systems, exploring common vulnerabilities, the inner workings of Veridise’s cutting-edge ZK security tools, and our recent academic research aimed at strengthening the security of these systems.

This presentation is an essential watch for professionals in the ZK space, security analysts and any blockchain enthusiast curious about the intersection of formal methods and zero-knowledge security. Isil offers an expert overview on ZK circuit vulnerabilities and engages in discussions with the a16z crypto audience. For those short on time, this blog post distills the key highlights from her talk.

Full presentation:

Zero-knowledge proofs have become foundational in blockchain space

Zero-knowledge (ZK) proofs have become foundational in the blockchain space, enabling applications such as scalable ZK rollups, privacy-preserving transactions, and secure online voting.

Despite their transformative potential, implementing ZK proofs correctly remains a significant challenge. Over the years, vulnerabilities in ZK circuits have led to major hacks in popular protocols.

Veridise’s analysis of over 100 recent security audits reveals that ZK circuits are particularly prone to critical vulnerabilities, with twice the likelihood of severe bugs compared to smart contracts. This highlights the urgent need for increase security work in the ZK space.

The challenge of under-constrained ZK circuits

A prevalent issue in ZK circuits is under-constrained circuits, where missing constraints allows for multiple outputs from the same input, compromising circuit determinism and integrity.

Isil referenced a pivotal study by Stefanos Chaliasos et al., which found that 95% of known ZK circuit bugs stem from under-constrained circuits. By lucky coincidence, one of the study’s authors, Jens Ernstberger, was present in the audience and shared additional insights at the 12:25 mark.

Over-constrained bugs in ZK circuits, while problematic, are much rarer and easier to detect during development phase, as they prevent valid solutions from being produced.

Formal methods to the rescue

Isil continues by explaining how Veridise has developed state-of-the-art formal methods tools to verify critical properties of ZK circuits. She provides a chronological overview of Veridise’s research journey, highlighting initial approaches that seemed promising but ultimately proved ineffective, paving the way for more comprehensive solutions that were developed later on.

Strawman solution: Encode circuit as an SMT formula and query satisfiability

Isil introduces a strawman solution to the problem of under-constrained circuits: leveraging Satisfiability Modulo Theories (SMT) solvers. SMT solvers are favored by practitioners in formal methods, and was something the Veridise team experimented with in the beginning. However, Isil quickly acknowledges the limitations of this approach for real-world ZK circuits.

Despite being a logical first step, this method is impractical for real-world applications. ZK circuits in real-world scenarios are too complex, as they involve numerous constraints, intermediate signals, and nonlinearities, all of which complicate the encoding process.

When circuits are encoded as SMT formulas and fed into solvers, the systems often struggle to process them, even with extended computation time. This sets the stage for discussing alternative strategies to address under-constrained circuits.

A working technique: Combining static analysis with SMT solvers (Picus)

Isil then outlines Veridise’s breakthrough: a hybrid technique that combines static analysis with SMT solvers. This approach involves an interactive loop between the two components, which exchange information via a shared knowledge base. The knowledge base maintains two critical types of information: range data for all signals and a record of signals proven to be deterministic.

The process starts with static analysis, which is lightweight and cost-efficient. Static analysis aims to infer signal ranges and identify deterministic variables. If the output variables align with the deterministic variables in the knowledge base, the circuit is deemed properly constrained. However, if static analysis stalls, the task is escalated to the SMT solver.

The SMT solver builds on the findings from static analysis, either proving additional signals deterministic or identifying non-deterministic outputs that point at potential bugs in the circuit. This iterative process of going back and forth between the SMT solver and the static analyzer continues until no further progress is possible. In cases where neither verification succeeds nor a bug is identified, the process may return an “unknown” result, often due to SMT solver timeouts.

By leveraging the complementary strengths of static analysis and SMT solvers, this technique significantly enhances the efficiency and reliability of detecting under-constrained circuits. The interplay between the two methods ensures that partial results from one phase directly support the other, creating a powerful and effective solution for ZK circuit verification.

Empirical evidence with Circom-lib

To evaluate the combined approach of using an SMT solver and a static analyzer, a large-scale study was conducted using a benchmark suite sourced from Circom-lib, the standard library for the Circom language. The study analyzed 163 circuits, each averaging 4,396 constraints and 24 output signals.

The results were both promising and insightful: the method successfully provided definitive results for 70% of the circuits, categorizing them as either verified or under-constrained. However, the remaining 30% faced unresolved issues due to solver timeouts, highlighting the limitations of current SMT solvers when dealing with complex systems, despite the help from the static analyzer.

Given Circom-lib’s widespread adoption, it was unsurprising that the majority of circuits were verified. Out of 163 circuits, 101 were confirmed as verified, while 8 were identified as under-constrained. Importantly, these assessments were precise, with no false positives reported. Conversations with Circom-lib developers revealed that while some findings were intentional design choices, some findings indeed corresponded to critical bugs. We covered these in our previous blog post: “Circom-Pairing: A Million-Dollar ZK Bug Caught Early”.

SMT solvers to the next level: Split Gröbner Bases for Finite Fields

As noted, 30% of the circuits remained unsolved due to solver timeouts, even when using a state-of-the-art SMT solver for finite fields. This raised a pivotal question: could a better decision procedure be created, one specifically designed to handle the practical queries posed by ZK circuits?

The answer came in the form of Veridise’s CAV 2024 paper, co-authored by Veridise team members (Shankara Pailoor, Alp Bassa, Kostas Ferles, Işil Dillig, Alex Ozdemir) and Stanford researchers (Alex Ozdemir, Clark Barrett).

This paper introduced a new and more effective solver built on the concept of Split Gröbner Bases. This innovative approach tackles the computational bottlenecks of verifying ZK circuits by dividing constraints into smaller, more manageable subsets. By isolating linear components and bit-sum constraints from nonlinear ones, the method not only simplifies the verification process but also makes it significantly more scalable.

A key feature of this approach is a propagation module, which iteratively exchanges information between submodules. This process helps create a split Gröbner basis that, while less comprehensive than a full Gröbner basis, is far more efficient to compute. The results were impressive: this method outperformed previous SMT solvers and hybrid approaches, solving three times as many determinism queries within the same timeout period.

For a deeper dive into the details, see our blog post: Veridise’s Zero-Knowledge Research: Split Gröbner Bases for Satisfiability Modulo Finite Fields.

Closing thoughts and future directions

Formal methods are set to become a cornerstone in ensuring the correctness and security of ZK circuits. Veridise’s research represents a significant leap forward in this emerging field, offering practical tools to tackle some of the most critical challenges in ZK security.

Isil concluded her talk with a call for collaboration and highlighted three promising areas for future exploration: developing a verification-friendly intermediate representation (IR) for ZK circuits, designing finite field solvers that go beyond determinism queries, and advancing automated techniques to verify equivalence between ZK circuits and their intended computations.

While Veridise’s prior research primarily targeted the Circom language, Isil hinted at exciting developments in the ZK infrastructure space, addressing audience curiosity. Stay tuned — more details will be revealed early next year!

Isil closed the talk by thanking Shankara Pailoor, Alex Ozdemir, and Alp Bassa, the key contributors to the ZK research presented.

Presentation slides (PDF) download

Author:
Mikko Ikola, VP of Marketing at Veridise

Want to learn more about Veridise?

Twitter | LinkedIn | Github | Request Audit

--

--

Veridise
Veridise

Published in Veridise

Our mission in to harden blockchain security with formal methods. We write about blockchain security, zero-knowledge proofs, and our bug discoveries.

Veridise
Veridise

Written by Veridise

Hardening blockchain security with formal methods. We write about blockchain & zero-knowledge proof security. Contact us for industry-leading security audits.

No responses yet