---
title: "Automated underconstraint detection"
description: "Automated underconstraint detection: Static analysis / SMT. Layer: Circuit. Characteristic finds: Non-unique outputs for a fixed input, unconstrained…"
type: "option"
url: "https://zkpick.com/audit/automated-underconstraint-detection/"
section: "03 Auditing a ZK protocol"
authors:
  - "MarketComp"
publisher: "MarketComp"
version: "1.3"
updated: "2026-09-12"
license: "CC-BY-4.0"
json: "https://zkpick.com/data/audit/automated-underconstraint-detection.json"
---

*By MarketComp. Updated 2026-09-12. Version 1.3. CC BY 4.0.*

# Automated underconstraint detection — *Static analysis / SMT*

> 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.

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**

- 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 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.

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

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-automated-underconstraint-detection)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Automated underconstraint detection | Circuit | Non-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositions | Application semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgets | Per-property, where the solver terminates | Very low once wired in |