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

TL;DR

zkCraft is a framework that uses LLM-guided mutation templates and proof-bearing search to improve the detection of semantic faults in zero-knowledge circuits, enhancing robustness and scalability.

Contribution

It introduces a novel combination of deterministic LLM-driven mutation templates with proof-bearing localization for ZK circuit debugging.

Findings

Detects diverse under- and over-constrained faults with low false positives

Reduces costly solver interactions in fault detection

Bridges formal verification and automated debugging for ZK circuits

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.