Resources: https://eprint.iacr.org/2024/514.pdf , https://eprint.iacr.org/2023/190.pdf , https://0xparc.org/blog/ecne

Introduction

This document defines a systematic checklist for auditing Circom circuits in Nomos. Circom compiles programs into two artifacts: witness-generation code and an arithmetic constraint system (R1CS/QAP). Security of the resulting zero-knowledge proof system depends entirely on whether the constraints faithfully encode the intended relation. If they do not, a malicious prover may generate valid proofs for false statements.

Overview

The checklist is organized into ten focus areas, reflecting the most frequent and impactful classes of vulnerabilities:

1. Spec ↔ Constraints: Ensure every rule in the specification is enforced at the constraint level; avoid relying only on witness assignments.
2. Under-/Un-constrained & Nondeterminism: Detect signals that are assigned but never constrained, or whose ranges are left unchecked.
3. Public Inputs: Confirm that all public signals are bound to constraints and influence circuit state.
4. Bit-length & Range: Validate that integers, IDs, and limbs respect explicit width bounds.
5. Field-Semantic Mismatches: Check for unintended modular wraparound where integer semantics are intended.
6. Sharp Edges (IsZero, division, conditionals): Verify both branches are constrained and edge cases (division by zero, multiple witnesses) are handled.
7. Crypto Primitives & Domain Separation: Ensure gadgets are used with correct parameters and that transcripts are domain-separated.
8. Template/Component Contracts: Audit that gadgets with caller obligations (e.g., .out constraints) are used safely.
9. Prover/Verifier Integration: Verify ordering of public inputs and transcript consistency with verifier code.
10. Negative & Fuzz Tests: Design tests that deliberately break constraints to ensure robustness against under-constraint.

Each section contains concrete checks, rationale, and optional search patterns for automation.

Two perennial failure modes:

• Misusing assignment vs. constraint operators. In Circom, <-- assigns a value to a signal in witness code, while <==/=== constrains it in R1CS. Using <-- where a constraint is needed yields under-constrained circuits and forgeries.
• Under-/over-constraining.
  • Under-constrained: some signals/ranges aren’t enforced → multiple valid witnesses / forged proofs (e.g., Dark Forest RangeProof missing bit-length checks; Tornado-style nullifier double-spend if nondeterminism exists).
  • Over-constrained: extra/optimizer-introduced assertions make valid inputs fail (e.g., early Poseidon instance marking a line “custom/zero”). That’s a completeness bug.

Why public inputs and “assigned-but-not-constrained” are dangerous.