ZKP学习笔记

ZK-Learning MOOC课程笔记

Lecture 15: Secure ZK Circuits via Formal Methods (Guest Lecturer: Yu Feng (UCSB & Veridise))

15.3 Formal Methods in ZK (Part II)

  • Formally prove that a circuit is NOT underconstrained
  • Existing Strategies
    • Static Analysis of Constraints (SA): false positive
    • SMT Solver: hard to scale for large circuit
  • Picus
    • Static Analysis Phase
    • SMT Phase
  • Future Directions