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，一个结合了确定性、R1CS感知定位与承载证明搜索的实用框架，用于检测语义不一致性。zkCraft将候选约束编辑编码为单个Row-Vortex多项式，并以一个Violation IOP取代重复的求解器查询，该IOP能够同时证明编辑的存在性并生成简洁证明。确定性的LLM驱动变异模板将探索偏向于边界情况，同时保留可审计的代数验证。在真实Circom代码上的评估表明，承载证明的定位能够以较低的误报率检测多种欠约束与过约束故障，并减少昂贵的求解器交互。我们的方法架起了形式化验证与自动化调试之间的桥梁，为鲁棒的零知识电路开发提供了一条可扩展的路径。