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.
