1 of 17

Push-Button Verification for

Yu Feng

ZK Circuits

2 of 17

Roadmap

Overview

Ongoing & Next Steps

Common Bug Detection for ZK Circuits

01

02

03

Spectrum of Formal Methods

Motivations, Challenges

Push-button Verification

3 of 17

Overview

4 of 17

Spectrum of Formal Methods

Testing

Bounded Model Checking, Symbolic Execution

Formal Verification

Guarantee

Human Efforts

Pros: Highest Guarantee

Cons: More Human/Expert Efforts

Pros: Less Human Efforts

Cons: Less Guarantee

5 of 17

An Architecture View of ZK Circuits

Smart

Contracts

Application Circuits

Core ZK Libraries & Building Blocks

6 of 17

7 of 17

ZK Circuit Verification: Current Roadmap

  • Coda: https://github.com/Veridise/Coda
  • - Formal verification using interactive theorem proving (i.e., Coq)
  • - Provide the highest guarantee, but requires manual/expert efforts

​

​

  • Picus: https://github.com/Veridise/Picus
  • - Push-button verification for common issues in ZK circuits

Coda

Core Library Circuits

(Verified Components)

Developer

Application Circuits

Picus

(Fully Verified)

Properties

Smart

Contracts

Application Circuits

Core ZK Libraries & Building Blocks

8 of 17

Common Bug Detection for�ZK Circuits

9 of 17

Uniqueness Property

  •  

ref: https://0xparc.org/blog/ecne

10 of 17

Push-button Verification

Translating a program and its property into constraints that can be reasoned about by off-the-shelf solver

​

​

​

​

​

​

​

​

Symbolic Compilation

Constraint Solver

Program

Property

Constraints

Solution

https://github.com/alex-ozdemir/CVC4/blob/ff/src/theory/ff

foo (int a) {

y = 1;

if (a > 0) y = 10;

assert y > 4

}

 

SMT formula

- Large circuits

- Non-linear ops

- Finite fields

…

​

​

​

11 of 17

Push-button Solver for ZK Circuits

  •  

https://en.wikipedia.org/wiki/DPLL_algorithm

Circuit

Solver

Finite Field Solver

SAT Solver

12 of 17

Automatic Circuit Invariant Synthesis

Some properties are difficult to prove without invariants

​

  • in[1] != 0
  • in2[0] != in1[0]
  • in[0] != 0 && in[1] != 1
  • …

13 of 17

Modular Verification for Large Circuits

Gadget

Summary

14 of 17

Evaluation

Compared Against Ecne (https://github.com/franklynwang/EcneProject)

65 (98%)

49 (74%)

15 of 17

Plans & Next Steps

16 of 17

Ongoing & Next Steps

​

  • - Specification language for ZK circuits (e.g., Orbis spec)
  • - Circuits in Halo2/Plonky/etc.
  • - Modular Incremental Solver for Large Circuits
  • - Contribute to Finite-Field solvers

Smart

Contracts

Application Circuits

Core ZK Libraries & Building Blocks

17 of 17

THANKS

Coda: https://github.com/Veridise/Coda

- Formal verification using interactive theorem proving (i.e., Coq)

- Provide the highest guarantee, but requires manual/expert efforts

​

​

Picus: https://github.com/Veridise/Picus

- Push-button verification for common issues in ZK circuits

​

​

Medjai: https://github.com/Veridise/Medjai

- Push-button verification for Cairo contracts

​

Smart

Contracts

Application Circuits

Core ZK Libraries & Building Blocks