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.

翻译：[translated abstract in Chinese] 零知识电路能够实现隐私保护与可扩展系统，但由于证人计算与电路约束之间的紧密耦合，正确实现存在困难。我们提出zkCraft这一实用框架，该框架结合确定性、R1CS感知的局部化技术与带有证明的搜索技术，用于检测语义不一致性问题。zkCraft将候选约束编辑编码为单个Row-Vortex多项式，并用违规交互式预言证明替代重复的求解器查询，该证明可验证编辑的存在性并附带简洁证明。确定性的由大语言模型驱动的变异模板将探索导向边缘情况，同时保持可审计的代数验证。在真实Circom代码上的评估表明，基于证明的局部化技术能够以低误报率检测多种欠约束与过约束故障，并显著减少昂贵的求解器交互。我们的方法弥合了形式化验证与自动化调试之间的鸿沟，为鲁棒零知识电路开发提供了可扩展路径。