← → Print all
03 — Auditing · Assurance guide

Automated underconstraint detection

Static analysis / SMT

In one paragraph

Automated underconstraint detection: Static analysis / SMT. Layer: Circuit. Characteristic finds: Non-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositions. Blind to: Application semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgets. Coverage claim: Per-property, where the solver terminates. Cost profile: Very low once wired in. Choose it when: Mandatory pre-audit hygiene for any Circom or R1CS codebase, and a permanent CI gate — so the paid engagement is not spent on findings a linter would have caught.

By MarketComp Updated v1.3 About the authors Changelog
Layer
Circuit
Characteristic finds
Non-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositions
Blind to
Application semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgets
Coverage claim
Per-property, where the solver terminates
Cost profile
Very low once wired in
Assurance matrix · see the row in context

What it is

Tools that reason about the constraint system directly and either prove that outputs are unique given inputs, or produce two distinct witnesses satisfying the constraints for the same public input. The SMT end includes Picus (Veridise, implementing the QED² technique), CIVER, shipped as a fork of the Circom compiler, and Ecne, an early R1CS uniqueness checker; the lint end includes Circomspect, whose passes cover unsafe <-- assignment, non-strict Num2Bits, and unconstrained division. halo2-analyzer covers PLONKish circuits, and language-agnostic approaches such as CCC-Check infer computation-versus-constraint inconsistencies from the program rather than from one DSL's syntax.

Strengths and tradeoffs

Strengths
  • Near-zero marginal cost once in CI; catches regressions on every commit
  • Returns concrete counterexample witnesses, directly actionable as tests
  • SMT-based tools can prove absence of the bug class for a given template
  • Linting has essentially no adoption barrier
Tradeoffs
  • Coverage skewed heavily to Circom and R1CS; AIR support exists (Picus has been applied to SP1's Plonky3 chips) but is younger, and Noir and other PLONKish frontends are thinner still
  • 'Unknown' is a common result on hash and bigint gadgets — solver timeouts force manual splitting
  • Models only under- and over-constraint; blind to replay, key management and transcript design
  • A 'safe' verdict is scoped to the property checked and is routinely over-read as 'correct'
  • Maintenance is uneven and the headline open-source tools have seen little movement since 2024, with some vendors moving active development into hosted products — apply the same recency test you would apply to a framework before depending on one

Choose it whenMandatory pre-audit hygiene for any Circom or R1CS codebase, and a permanent CI gate — so the paid engagement is not spent on findings a linter would have caught.

Failure modes that involve it
Direct answers that mention it
Maintained implementations

Not recorded for this entry.

Maturity: Production-used, unevenly maintained · License: Mixed (MIT / GPL-3.0) · github.com ↗

How to decide
Other assurance guides in §03
ZK security consultanciesManual circuit and constraint reviewFormal verification of ZK circuitsDifferential and fuzz testingCryptographic review of the protocol and proof systemVerifier and integration reviewAudit contestsBug bountiesLLM-assisted review

Sources cited on this page · 5

  1. Automated detection of underconstrained circuits (QED², PLDI 2023)paper
  2. Picus — automated verification of the uniqueness property for ZKP circuits (Veridise)tool
  3. Ecne — early automated uniqueness checking for R1CStool
  4. Automated analysis of Halo2 circuitspaper
  5. Automated soundness and completeness vetting of Polygon zkEVM (USENIX Security '25)paper

All 48 sources for §03 are listed on the section page →

Cite this page 
MarketComp (2026). Automated underconstraint detection. The ZK Field Manual (Version 1.3). MarketComp. https://zkpick.com/audit/automated-underconstraint-detection/
@misc{zkfieldmanual-automated-underconstraint-detection,
  title        = {Automated underconstraint detection — The ZK Field Manual},
  author       = {MarketComp},
  year         = {2026},
  version      = {1.3},
  howpublished = {\url{https://zkpick.com/audit/automated-underconstraint-detection/}},
  note         = {Accessed: YYYY-MM-DD}
}