Language-Agnostic Detection of Bugs in Zero-Knowledge Proof Programs

A summary of a talk on a new language-agnostic approach using abstract interpretation to find critical vulnerabilities in Zero-Knowledge Proof (ZKP) programs by modeling and detecting mismatches between prover computations and verifier constraints.

May 7, 2026 4 min read

Language-Agnostic Detection of Bugs in Zero-Knowledge Proof Programs — source: https://www.youtube.com/watch?v=pW8yJiXRzXc

Zero-Knowledge Proof (ZKP) programs present a unique development challenge: developers must write code for both the prover (the computation) and the verifier (the constraints). The prover performs complex operations to generate a proof, while the verifier, for performance reasons, is restricted to a simpler set of operations (addition, multiplication, equality) to check the proof. This decoupling between computation and verification is a primary source of critical vulnerabilities.

The Core Problem: Computation-Constraint Mismatches

A fundamental issue arises when the verifier’s constraints do not fully capture the logic of the prover’s computations. A classic example is integer division:

Computation (Prover): The prover calculates out = a / b. This computation has an implicit precondition: b cannot be zero. An honest prover’s program would crash if it attempted to divide by zero.
Constraint (Verifier): To check this using its limited operations, the verifier enforces the constraint out * b == a.

A malicious actor can exploit this mismatch. They can ignore the prover’s computation entirely and forge a proof with a=0, b=0, and out=5. The verifier’s check (5 * 0 == 0) passes, thus accepting a fraudulent proof that corresponds to an impossible computation (division by zero).

To mitigate this, developers must manually add a constraint to ensure b is non-zero. However, to optimize performance and avoid redundant checks, ZKP libraries often place these requirements as assumptions or documentation (e.g., “signal tags”) on their functions. These assumptions are not enforced by the compiler, and developers frequently forget to add the corresponding constraints, leading to vulnerabilities.

Limitations of Existing Bug Detection Tools

Prior work on ZKP bug detection has several key limitations:

Language-Specific: Most tools are tightly coupled to a single ZKP language, such as Circom.
Constraint-Focused: They primarily analyze the verifier’s constraints in isolation, checking for properties like non-determinism. They do not analyze the prover’s computations, making it impossible to detect semantic mismatches where the verifier correctly verifies the wrong thing.
Narrow Scope: They target a limited class of bugs and often overlook vulnerabilities like arithmetic overflows or division by zero.
Scalability Bottlenecks: Many rely on SMT solvers, which are slow and struggle with the non-linear equations common in ZKP constraints, often leading to timeouts on large programs.

A New Formal Model and Detection Tool

To address these limitations, a new approach was proposed, centered around a formal model and a practical, language-agnostic tool.

The Domain Consistency Model (DCM)

The core contribution is the Domain Consistency Model (DCM), which formalizes the relationship between the prover’s computations and the verifier’s constraints. The model defines a program as correct if the set of possible values an honest prover can produce is consistent with the set of values the verifier accepts. Any value set that is accepted by the verifier but cannot be produced by the prover represents a potential vulnerability. This model allows for the formalization of a new taxonomy of vulnerabilities based on these computation-constraint mismatches.

CCC-Check: An Efficient, Language-Agnostic Detector

Implementing the DCM by iterating through all possible values is computationally infeasible. The solution is CCC-Check, a bug detection tool based on abstract interpretation, a static analysis technique that approximates program behavior for efficiency.

Approximating the Computation Side: CCC-Check leverages the developer-provided specifications (signal tags and assumptions) as a summary of the expected behavior and preconditions for an honest prover.
Approximating the Constraint Side: It uses a set of inference rules to analyze the verifier’s constraints and approximate the possible range of values each variable can hold. For example, a constraint like x * (x - 2) == 0 implies that the verifier will only accept values of 0 or 2 for x. This pattern-matching approach is significantly faster than SMT solving, especially for non-linear equations.

To achieve language-agnostic support, CCC-Check operates on a shared compiler Intermediate Representation (IR). This allows it to analyze any ZKP language (like Circom or Noir) that can be compiled to this IR, making the tool future-proof as the ecosystem evolves.

Evaluation and Real-World Impact

CCC-Check’s effectiveness was validated through extensive evaluation:

Performance: When compared against an SMT-based tool on 35 benchmark programs, CCC-Check was, on average, two orders of magnitude faster while maintaining comparable precision.
Real-World Vulnerabilities: The tool was used to analyze six widely-adopted, open-source ZKP projects from entities like Microsoft and TikTok. This analysis uncovered 15 previously unknown vulnerabilities.
Impact: Of these 15 bugs, 13 have since been patched by the project maintainers. Notably, 12 of these vulnerabilities could not have been captured by existing models because they were semantic mismatches that required analyzing both the prover’s computation and the verifier’s constraints.