# Quantstamp: Linting Halo2 Circuits

- Channel: [Ethereum Denver](https://streameth.org/ethereum-denver)
- Date: 2023-10-07
- Duration: 17:44
- Watch: https://streameth.org/watch/yt-66gtzO-G1IA
- YouTube: https://www.youtube.com/watch?v=66gtzO-G1IA

## Description

Various tools (Ecne, Picus) exist for sanity checking various ZK proof system circuits. However, this work is limited to R1CS analysis and is therefore not suitable for use with proof systems with Plonkish arithmetic. We describe a modification to the Halo2 proof codebase that enables constraints for Halo2 gates to be sanity checked. We outline a proof of concept where real (erroneous) circuits are found to be under-constrained in the sense that they have two satisfying assignments. These satisfying assignments are found via an SMT solver connected directly to the Halo2 codebase. This is the first work we are aware of that applies lightweight formal methods to the Halo2 codebase. We conclude by outlining future directions for the project.

 with 
Jan Gorzny
Fatemeh Heidari
Mohsen Ahmadvand
Mohammad Jahanara
Jeffrey Kam
Matthias Hall-Andersen