Table of Contents
Fetching ...

zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing

Rong Fu, Jia Yee Tan, Wenxin Zhang, Youjin Wang, Ziyu Kong, Zeli Su, Zhaolu Kang, Shuning Zhang, Xianda Li, Kun Liu, Simon Fong

TL;DR

zkCraft introduces a ZK-native fuzzing framework that casts the search for small, vulnerability-inducing edits in zero-knowledge circuits as a single algebraic existence problem encoded by a Row-Vortex polynomial and certified via a Violation IOP. It couples deterministic LLM-guided mutation templates as zero-shot pattern accelerators with a compact, auditable proof that also yields a concrete counterexample trace for developer triage. The framework demonstrates strong detection performance across real Circom circuits, reducing solver interactions while maintaining zero false positives and deploying an end-to-end pipeline that is extensible to other DSLs. Theoretical additions provide formal guarantees on binding, extraction complexity, and relative completeness, while practical backends offer constant-sized proofs within defined parameter envelopes. Overall, zkCraft bridges formal verification and automated debugging to enable scalable, auditable robust ZK circuit development.

Abstract

Zero-knowledge circuits enable privacy-preserving and scalable systems but are difficult to implement correctly due to the tight coupling between witness computation and circuit constraints. We present zkCraft, a practical framework that combines deterministic, R1CS-aware localization with proof-bearing search to detect semantic inconsistencies. zkCraft encodes candidate constraint edits into a single Row-Vortex polynomial and replaces repeated solver queries with a Violation IOP that certifies the existence of edits together with a succinct proof. Deterministic LLM-driven mutation templates bias exploration toward edge cases while preserving auditable algebraic verification. Evaluation on real Circom code shows that proof-bearing localization detects diverse under- and over-constrained faults with low false positives and reduces costly solver interaction. Our approach bridges formal verification and automated debugging, offering a scalable path for robust ZK circuit development.

zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing

TL;DR

zkCraft introduces a ZK-native fuzzing framework that casts the search for small, vulnerability-inducing edits in zero-knowledge circuits as a single algebraic existence problem encoded by a Row-Vortex polynomial and certified via a Violation IOP. It couples deterministic LLM-guided mutation templates as zero-shot pattern accelerators with a compact, auditable proof that also yields a concrete counterexample trace for developer triage. The framework demonstrates strong detection performance across real Circom circuits, reducing solver interactions while maintaining zero false positives and deploying an end-to-end pipeline that is extensible to other DSLs. Theoretical additions provide formal guarantees on binding, extraction complexity, and relative completeness, while practical backends offer constant-sized proofs within defined parameter envelopes. Overall, zkCraft bridges formal verification and automated debugging to enable scalable, auditable robust ZK circuit development.

Abstract

Zero-knowledge circuits enable privacy-preserving and scalable systems but are difficult to implement correctly due to the tight coupling between witness computation and circuit constraints. We present zkCraft, a practical framework that combines deterministic, R1CS-aware localization with proof-bearing search to detect semantic inconsistencies. zkCraft encodes candidate constraint edits into a single Row-Vortex polynomial and replaces repeated solver queries with a Violation IOP that certifies the existence of edits together with a succinct proof. Deterministic LLM-driven mutation templates bias exploration toward edge cases while preserving auditable algebraic verification. Evaluation on real Circom code shows that proof-bearing localization detects diverse under- and over-constrained faults with low false positives and reduces costly solver interaction. Our approach bridges formal verification and automated debugging, offering a scalable path for robust ZK circuit development.
Paper Structure (69 sections, 6 theorems, 76 equations, 12 figures, 9 tables, 2 algorithms)

This paper contains 69 sections, 6 theorems, 76 equations, 12 figures, 9 tables, 2 algorithms.

Key Result

Theorem 6.1

Let $\mathsf{PC}$ be a polynomial commitment scheme that is computationally binding on coefficient vectors. Suppose the evaluator uses the block-Vandermonde map $M$ of Eqs. eq:M-block–eq:det-M with pairwise distinct nodes and with field size satisfying Eq. eq:field-size-condition. If an adversary pr

Figures (12)

  • Figure 1: Overview of the zkCraft framework for ZK-native fuzzing and mutation. The pipeline begins at the Input Layer, where a Circom program is decomposed into R1CS matrices. In Stage 1 (The Slicer), a Sparse Fingerprint Scanner computes diagnostic scores to prune the constraint space into a manageable Candidate Pool$\mathcal{R}_{\mathrm{cand}}$. This process is accelerated by the LLM Oracles, which provide zero-shot Mutation Templates and learn vulnerability patterns to bias the search. In Stage 2 (ZK-Native Engine), candidate edits are bundled into the Row-Vortex Commitment$R(X,Y)$. A Violation IOP (utilizing algebraic Sum-Check identities) then searches for a witness that satisfies the edited constraints while diverging from the original output. The resulting Succinct Proof$\pi$ serves as a Proof-as-Counterexample, from which the Witness Extraction machinery reconstructs the concrete trace to confirm the vulnerability via TCCT.
  • Figure 2: zkCraft versus baseline tools. The horizontal axis uses a logarithmic scale from one second to two hours. Curves show cumulative unique true positives averaged over five seeds and shaded bands indicate one standard deviation. A gold marker at 100 seconds highlights early convergence.
  • Figure 3: Ablation results. Bars represent the log10 of the slowdown factor relative to the default configuration. The red line reports the number of bugs not discovered within 24 hours when a single module is removed. A horizontal threshold marks a 100 times slowdown.
  • Figure 4: zkCraft convergence under four mutation/population settings. Time (log scale) on the horizontal axis; cumulative true positives on the vertical. Gold dashed line marks 100-second convergence; shaded areas show one standard deviation.
  • Figure 5: Row-Vortex commitment schematic. The three panels illustrate candidate row selection, construction of the bivariate polynomial, and the Violation IOP that yields a succinct proof. The top annotation summarizes the replacement of many SMT calls by a single commitment.
  • ...and 7 more figures

Theorems & Definitions (11)

  • Theorem 6.1: Binding reduction for Row-Vortex commitment
  • proof
  • Theorem 6.2: Explicit knowledge-error bound
  • Lemma 6.3: Indicator polynomial non-vanishing
  • proof
  • Theorem 6.4: Knowledge-error explicit bound
  • proof
  • Proposition 6.5: Practical IOP cost
  • proof
  • Theorem 6.6: Relative Completeness
  • ...and 1 more