Paper 2023/1051

Automated Analysis of Halo2 Circuits

Fatemeh Heidari Soureshjani, Polytechnique Montréal, Quantstamp, Inc.
Mathias Hall-Andersen, Aarhus University
MohammadMahdi Jahanara, Quantstamp, Inc.
Jeffrey Kam, Quantstamp, Inc.
Jan Gorzny, Quantstamp, Inc.
Mohsen Ahmadvand, Quantstamp, Inc.

Zero-knowledge proof systems are becoming increasingly prevalent and being widely used to secure decentralized financial systems and protect the privacy of users. Given the sensitivity of these applications, zero-knowledge proof systems are a natural target for formal verification methods. We describe methods for checking one such proof system: Halo2. We use abstract interpretation and an SMT solver to check various properties of Halo2 circuits. Using abstract interpretation, we can detect unused gates, unconstrained cells, and unused columns. Using an SMT solver, we can detect under-constrained (in the sense that for the same public input they have two efficiently computable satisfying assignments) circuits. This is the first work we are aware of that applies lightweight formal methods to PLONKish arithmetization and Halo2 circuits.

Available format(s)
Publication info
Published elsewhere. Satisfiability Modulo Theories 2023 (SMT 2023)
Zero-Knowledge ProofsHalo2Formal MethodsAbstract InterpretationSMT
Contact author(s)
fatemeh heidari-soureshjani @ polymtl ca
mathias @ hall-andersen dk
mohammad @ quantstamp com
jeffrey @ quantstamp com
j gorzny @ gmail com
mohsen @ quantstamp com
2023-07-05: approved
2023-07-05: received
See all versions
Short URL
Creative Commons Attribution


      author = {Fatemeh Heidari Soureshjani and Mathias Hall-Andersen and MohammadMahdi Jahanara and Jeffrey Kam and Jan Gorzny and Mohsen Ahmadvand},
      title = {Automated Analysis of Halo2 Circuits},
      howpublished = {Cryptology ePrint Archive, Paper 2023/1051},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.