Training for Constraining: How to Prevent Circuit-Level Bugs
Vulnerabilities from underconstrained circuits remain a live concern. At least four significant underconstrained-circuit bugs surfaced in 2026: Zcash's Orchard pool (a missing Halo2 copy constraint), OpenVM's pairing check (CVE-2026-46669), Scroll's ecPairing precompile, and three criticals in ZKsync Airbender, caught by formal verification. Unit testing is insufficient to catch underconstrained circuits, as true witnesses always pass verification.
In this introductory workshop we first introduce arithmetic circuits and how they are used in modern SNARK-based systems. Then we will discuss real examples of underconstrained circuits, and what a false proof means in context. Participants will see an example of an underconstrained circuit and how to identify it by inspection. Then we'll demonstrate on an example circuit how methods of fuzzing and formal verification can find a missing constraint, and discuss how AI tools may assist in the search for circuit-level vulnerabilities.
Speakers: Levi Katyal Sledd, Vijay Singh
Track: Security
