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将候选约束修改编码为单个行涡旋多项式，并以一个违规交互式可验证证明取代重复的求解器查询，该证明在提供简洁证明的同时确认修改的存在。确定性的LLM驱动变异模板将探索偏向于边界情况，同时保持可审计的代数验证。在真实Circom代码上的评估表明，承载证明的定位能够以较低误报率检测多种欠约束与过约束故障，并减少昂贵的求解器交互。我们的方法桥接了形式化验证与自动化调试，为稳健的零知识电路开发提供了一条可扩展的路径。