pith. sign in

arxiv: 2602.00667 · v4 · submitted 2026-01-31 · 💻 cs.CR · cs.SE

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

Rong Fu , Jia Yee Tan , Youjin Wang , Ziyu Kong , Zeli Su , Zhaolu Kang , Shuning Zhang , Xianda Li
show 2 more authors
Kun Liu Simon Fong
This is my paper

Pith reviewed 2026-05-16 09:00 UTC · model grok-4.3

classification 💻 cs.CR cs.SE
keywords zero-knowledge circuitsfuzzingLLMCircomR1CSconstraint verificationIOP
0
0 comments X

The pith

zkCraft uses LLM-guided mutations and a Violation IOP to detect under- and over-constrained faults in ZK circuits while cutting solver queries.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces zkCraft as a framework for finding semantic inconsistencies in zero-knowledge circuits by combining deterministic R1CS-aware localization with proof-bearing search. Candidate constraint edits are encoded into a single Row-Vortex polynomial, and a Violation IOP certifies their existence with a succinct proof instead of repeated solver calls. Deterministic LLM-driven mutation templates steer exploration toward edge cases while keeping the algebraic verification auditable. Evaluation on real Circom code shows the method detects diverse under- and over-constrained faults with low false positives.

Core claim

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, while deterministic LLM-driven mutation templates bias exploration toward edge cases and preserve auditable algebraic verification.

What carries the argument

Violation IOP that certifies the existence of constraint edits with a succinct proof, replacing repeated solver queries.

If this is right

  • Detects diverse under- and over-constrained faults in real Circom code
  • Maintains low false positives in localization
  • Reduces costly solver interaction
  • Bridges formal verification and automated debugging for scalable ZK development

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The solver reduction could make fuzzing practical for circuits large enough to cause current tools to time out
  • The same encoding-plus-IOP pattern might apply to constraint systems beyond R1CS

Load-bearing premise

LLM-driven mutation templates reliably bias search toward genuine edge-case faults without systematically missing critical inconsistencies or generating edits the algebraic verifier cannot classify.

What would settle it

An experiment on a known under-constrained Circom circuit where the LLM templates produce no exposing edit and the Violation IOP therefore reports no fault.

Figures

Figures reproduced from arXiv: 2602.00667 by Jia Yee Tan, Kun Liu, Rong Fu, Shuning Zhang, Simon Fong, Xianda Li, Youjin Wang, Zeli Su, Zhaolu Kang, Ziyu Kong.

Figure 1
Figure 1. Figure 1: Overview of the zkCraft framework for ZK-native fuzzing and mutation. The pipeline begins at the Input Layer, where a Circom program is decomposed into R1CS matrices. In Stage 1 (The Slicer), a Sparse Fingerprint Scanner computes diagnostic scores to prune the constraint space into a manageable Candidate Pool Rcand. This process is accelerated by the LLM Oracles, which provide zero-shot Mutation Templates … view at source ↗
Figure 2
Figure 2. Figure 2: zkCraft versus baseline tools. The horizontal axis uses a logarithmic scale from one second to two hours. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Ablation results. Bars represent the log10 of the slowdown factor relative to the default configuration. The [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: zkCraft convergence under four mutation/population settings. Time (log scale) on the horizontal axis; [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Row-Vortex commitment schematic. The three panels illustrate candidate row selection, construction of the [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Proof size vs. constraint count (top) and prover time (bottom), both on log-scaled axes. Dashed line shows [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Representative confirmed vulnerabilities and corresponding counterexamples. Left panels show compact [PITH_FULL_IMAGE:figures/full_fig_p007_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Strategy comparison as a radar plot. Axes report early discovery at two short checkpoints, final discovery at [PITH_FULL_IMAGE:figures/full_fig_p008_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Hyperparameter sensitivity heatmap. The horizontal axis is mutation strength and the vertical axis is [PITH_FULL_IMAGE:figures/full_fig_p009_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Sensitivity of zkCraft to key hyperparameters across four settings. Each panel varies one parameter with others fixed; curves show cumulative true positives over time (log scale), averaged across five seeds. A gold dashed line at 100 seconds marks the early-convergence regime. remaining succinct. The prover additionally holds a candidate witness w ′ that, together with (δ, c), is intended to satisfy the e… view at source ↗
Figure 11
Figure 11. Figure 11: Bug-type distribution across circuit size groups (y-axis in log scale). Columns enumerate semantic fault [PITH_FULL_IMAGE:figures/full_fig_p017_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Proof size and prover generation time for KZG, FRI, and IPA at multiple folding depths. The horizontal axis [PITH_FULL_IMAGE:figures/full_fig_p029_12.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents zkCraft, a framework for fuzzing zero-knowledge circuits that uses prompt-guided LLMs as zero-shot mutation oracles to generate R1CS-aware edits, encodes them via a Row-Vortex polynomial, and replaces repeated solver calls with a Violation IOP that produces succinct proofs of constraint violations. The central claim is that this combination enables detection of under- and over-constrained faults in real Circom code with low false positives while reducing solver interaction.

Significance. If the quantitative claims hold, the integration of deterministic LLM mutation templates with algebraic IOP machinery could provide a practical bridge between automated testing and formal ZK verification, lowering the cost of finding semantic inconsistencies in production circuits and improving robustness of privacy-preserving systems.

major comments (2)
  1. [Evaluation] Evaluation section: the assertion that 'proof-bearing localization detects diverse under- and over-constrained faults with low false positives' is not supported by any reported detection rates, false-positive counts, precision/recall figures, or ablation against random-edit baselines on the Circom benchmark set; without these numbers the central claim that the approach reduces costly solver interaction cannot be assessed.
  2. [§3.2] §3.2 (Violation IOP construction): the reduction from repeated solver queries to a single succinct proof is presented as a direct consequence of the Row-Vortex encoding, yet no concrete bound on proof size or verification time relative to a standard R1CS solver is supplied, leaving the claimed efficiency gain unquantified.
minor comments (2)
  1. [§3.1] The notation for the Row-Vortex polynomial is introduced without an explicit equation or degree bound; adding a displayed equation (e.g., Eq. (3)) would clarify how candidate edits are aggregated.
  2. [§4] The prompt templates used for the LLM mutation oracle are described at a high level; including the exact zero-shot prompt text in an appendix would improve reproducibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We appreciate the referee's thorough review and valuable suggestions for improving our paper. We have carefully considered the major comments and revised the manuscript to address them by enhancing the evaluation with quantitative metrics and providing explicit efficiency bounds in the theoretical section.

read point-by-point responses

  1. Referee: [Evaluation] Evaluation section: the assertion that 'proof-bearing localization detects diverse under- and over-constrained faults with low false positives' is not supported by any reported detection rates, false-positive counts, precision/recall figures, or ablation against random-edit baselines on the Circom benchmark set; without these numbers the central claim that the approach reduces costly solver interaction cannot be assessed.

    Authors: We agree that the current evaluation lacks the specific quantitative figures needed to fully substantiate the claims. In the revised manuscript, we have added a comprehensive set of metrics from our experiments, including detection rates, false-positive counts, precision and recall, as well as an ablation study comparing LLM-guided mutations against random-edit baselines on the Circom benchmark set. These additions directly support the reduction in solver queries and will be presented in an updated Evaluation section with new tables and figures. revision: yes

  2. Referee: [§3.2] §3.2 (Violation IOP construction): the reduction from repeated solver queries to a single succinct proof is presented as a direct consequence of the Row-Vortex encoding, yet no concrete bound on proof size or verification time relative to a standard R1CS solver is supplied, leaving the claimed efficiency gain unquantified.

    Authors: We acknowledge that explicit bounds were not provided in the original submission. We have now derived and included concrete bounds in the revised §3.2: the Row-Vortex-based Violation IOP produces a succinct proof whose size is logarithmic in the number of constraints, with verification time also logarithmic, in contrast to the linear cost of each R1CS solver invocation. This analysis quantifies the efficiency improvement and has been added to the manuscript. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation relies on external R1CS/IOP primitives and LLM as independent oracle

full rationale

The paper presents zkCraft as a framework that applies deterministic LLM mutation templates to generate candidate edits, then encodes them into Row-Vortex polynomials for verification via a Violation IOP. Both the algebraic machinery (R1CS, IOP) and the LLM prompting strategy are treated as external inputs whose correctness is not derived from the paper's own fitted quantities or self-citations. No equations reduce the claimed detection rates or solver reductions to a tautological fit; the evaluation on Circom code is presented as an empirical outcome rather than a self-defining prediction. The central claims therefore remain non-circular.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

Abstract-only review yields minimal ledger entries; the central claim rests on the assumption that R1CS faithfully captures circuit semantics and that the newly introduced Row-Vortex and Violation IOP constructs function as described.

axioms (1)
  • domain assumption R1CS constraints accurately model the intended witness computation
    Invoked when the localization step treats constraint edits as directly comparable to circuit behavior.
invented entities (2)
  • Row-Vortex polynomial no independent evidence
    purpose: Encodes candidate constraint edits into a single polynomial for efficient checking
    New encoding construct introduced to replace repeated solver queries.
  • Violation IOP no independent evidence
    purpose: Provides a succinct proof that certifies the existence of faulty edits
    New interactive oracle proof component presented as the replacement for solver interaction.

pith-pipeline@v0.9.0 · 5466 in / 1374 out tokens · 47312 ms · 2026-05-16T09:00:30.738388+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

66 extracted references · 66 canonical work pages · 2 internal anchors

  1. [1]

    Automated detection of under-constrained circuits in zero-knowledge proofs

    Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, and I¸ sıl Dillig. Automated detection of under-constrained circuits in zero-knowledge proofs. Proceedings of the ACM on Programming Languages, 7(PLDI):1510–1532, 2023. 19 zkCraft

    work page 2023

  2. [2]

    Practical security analysis of {Zero-Knowledge} proof circuits

    Hongbo Wen, Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Isil Dillig, and Yu Feng. Practical security analysis of {Zero-Knowledge} proof circuits. In33rd USENIX Security Symposium (USENIX Security 24), pages 1471–1487, 2024

    work page 2024

  3. [3]

    Cheesecloth: Zero-knowledge proofs of real-world vulnerabilities.ACM Transactions on Privacy and Security, 28(4):1–35, 2025

    Santiago Cuéllar Gempeler, Bill Harris, James Parker, Stuart Pernsteiner, Ian Sweet, and Eran Tromer. Cheesecloth: Zero-knowledge proofs of real-world vulnerabilities.ACM Transactions on Privacy and Security, 28(4):1–35, 2025

    work page 2025

  4. [4]

    MTZK: Testing and Exploring Bugs in Zero-Knowledge (ZK) Compilers

    Dongwei Xiao, Zhibo Liu, Yiteng Peng, and Shuai Wang. Mtzk: Testing and exploring bugs in zero-knowledge (zk) compilers. InNDSS, 2025

    work page 2025

  5. [5]

    Zero-knowledge iops approaching witness length

    Noga Ron-Zewi and Mor Weiss. Zero-knowledge iops approaching witness length. InAnnual International Cryptology Conference, pages 105–137. Springer, 2024

    work page 2024

  6. [6]

    {ZKSMT}: A {VM} for proving {SMT} theorems in zero knowledge

    Daniel Luick, John C Kolesar, Timos Antonopoulos, William R Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, and Ning Luo. {ZKSMT}: A {VM} for proving {SMT} theorems in zero knowledge. In33rd USENIX Security Symposium (USENIX Security 24), pages 3837–3845, 2024

    work page 2024

  7. [7]

    Leo: A programming language for formally verified, zero-knowledge applications.Cryptology ePrint Archive, 2021

    Collin Chin, Howard Wu, Raymond Chu, Alessandro Coglio, Eric McCarthy, and Eric Smith. Leo: A programming language for formally verified, zero-knowledge applications.Cryptology ePrint Archive, 2021

    work page 2021

  8. [8]

    Zcls: A lifecycle strategy for efficient zk-rollup circuit optimization in circom.IEEE Access, 13: 202840–202863, 2025

    Khoa Tan V o, Minh Ngo, Thu Nguyen, Thu-Thuy Ta, Mong-Thy Nguyen Thi, Hong-Tri Nguyen, and Tu-Anh Nguyen-Hoang. Zcls: A lifecycle strategy for efficient zk-rollup circuit optimization in circom.IEEE Access, 13: 202840–202863, 2025

    work page 2025

  9. [9]

    Clap: a semantic-preserving optimizing edsl for plonkish proof systems.arXiv preprint arXiv:2405.12115, 2024

    Marco Stronati, Denis Firsov, Antonio Locascio, and Benjamin Livshits. Clap: a semantic-preserving optimizing edsl for plonkish proof systems.arXiv preprint arXiv:2405.12115, 2024

    work page arXiv 2024

  10. [10]

    Zk-prover: Proving programming verification in non- interactive zero-knowledge proofs

    Haoyu Wei, Jingyu Ke, Ruibang Liu, and Guoqiang Li. Zk-prover: Proving programming verification in non- interactive zero-knowledge proofs. InInternational Conference on Formal Engineering Methods, pages 209–227. Springer, 2025

    work page 2025

  11. [11]

    Automated verification of consistency in zero-knowledge proof circuits

    Jon Stephens, Shankara Pailoor, and Isil Dillig. Automated verification of consistency in zero-knowledge proof circuits. InInternational Conference on Computer Aided Verification, pages 315–338. Springer, 2025

    work page 2025

  12. [12]

    Scalable verification of zero-knowledge protocols

    Miguel Isabel, Clara Rodriguez-Nunez, and Albert Rubio. Scalable verification of zero-knowledge protocols. In 2024 IEEE Symposium on Security and Privacy (SP), pages 1794–1812. IEEE, 2024

    work page 2024

  13. [13]

    Fast{RS- IOP} multivariate polynomial commitments and verifiable secret sharing

    Zongyang Zhang, Weihan Li, Yanpei Guo, Kexin Shi, Sherman SM Chow, Ximeng Liu, and Jin Dong. Fast{RS- IOP} multivariate polynomial commitments and verifiable secret sharing. In33rd USENIX Security Symposium (USENIX Security 24), pages 3187–3204, 2024

    work page 2024

  14. [14]

    Ligerolight: Optimized iop-based zero-knowledge argument for blockchain scalability.IEEE Transactions on Dependable and Secure Computing, 21(4):3656–3670, 2023

    Zongyang Zhang, Weihan Li, Ximeng Liu, Xin Chen, and Qihang Peng. Ligerolight: Optimized iop-based zero-knowledge argument for blockchain scalability.IEEE Transactions on Dependable and Secure Computing, 21(4):3656–3670, 2023

    work page 2023

  15. [15]

    Large language model guided protocol fuzzing

    Ruijie Meng, Martin Mirchev, Marcel Böhme, and Abhik Roychoudhury. Large language model guided protocol fuzzing. InProceedings of the 31st Annual Network and Distributed System Security Symposium (NDSS), volume 2024, 2024

    work page 2024

  16. [16]

    How effective are they? exploring large language model based fuzz driver generation

    Cen Zhang, Yaowen Zheng, Mingqiang Bai, Yeting Li, Wei Ma, Xiaofei Xie, Yuekang Li, Limin Sun, and Yang Liu. How effective are they? exploring large language model based fuzz driver generation. InProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 1223–1235, 2024

    work page 2024

  17. [17]

    Semantic-aware fuzzing: An empirical framework for llm-guided, reasoning-driven input mutation.arXiv preprint arXiv:2509.19533, 2025

    Mengdi Lu, Steven Ding, Furkan Alaca, and Philippe Charland. Semantic-aware fuzzing: An empirical framework for llm-guided, reasoning-driven input mutation.arXiv preprint arXiv:2509.19533, 2025

    work page arXiv 2025

  18. [18]

    Large language models for unit testing: A systematic literature review.arXiv preprint arXiv:2506.15227, 2025

    Quanjun Zhang, Chunrong Fang, Siqi Gu, Ye Shang, Zhenyu Chen, and Liang Xiao. Large language models for unit testing: A systematic literature review.arXiv preprint arXiv:2506.15227, 2025

    work page arXiv 2025

  19. [19]

    Zero-shot detection of llm-generated code via approximated task conditioning

    Maor Ashkenazi, Ofir Brenner, Tal Furman Shohet, and Eran Treister. Zero-shot detection of llm-generated code via approximated task conditioning. InJoint European Conference on Machine Learning and Knowledge Discovery in Databases, pages 187–204. Springer, 2025. 20 zkCraft

    work page 2025

  20. [20]

    Mutation-based consistency testing for evaluating the code understanding capability of llms

    Ziyu Li and Donghwan Shin. Mutation-based consistency testing for evaluating the code understanding capability of llms. InProceedings of the IEEE/ACM 3rd International Conference on AI Engineering-Software Engineering for AI, pages 150–159, 2024

    work page 2024

  21. [21]

    zkllm: Zero knowledge proofs for large language models

    Haochen Sun, Jason Li, and Hongyang Zhang. zkllm: Zero knowledge proofs for large language models. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, pages 4405–4419, 2024

    work page 2024

  22. [22]

    Evaluating compiler optimiza- tion impacts on zkvm performance.arXiv preprint arXiv:2508.17518, 2025

    Thomas Gassmann, Stefanos Chaliasos, Thodoris Sotiropoulos, and Zhendong Su. Evaluating compiler optimiza- tion impacts on zkvm performance.arXiv preprint arXiv:2508.17518, 2025

    work page arXiv 2025

  23. [23]

    Towards source mapping for zero-knowledge smart contracts: Design and preliminary evaluation

    Pei Xu, Yulei Sui, and Mark Staples. Towards source mapping for zero-knowledge smart contracts: Design and preliminary evaluation. InProceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 200–209, 2025

    work page 2025

  24. [24]

    Blocka2a: Towards secure and verifiable agent-to- agent interoperability.arXiv preprint arXiv:2508.01332, 2025

    Zhenhua Zou, Zhuotao Liu, Lepeng Zhao, and Qiuyang Zhan. Blocka2a: Towards secure and verifiable agent-to- agent interoperability.arXiv preprint arXiv:2508.01332, 2025

    work page arXiv 2025

  25. [25]

    zkpytorch: A hierarchical optimized compiler for zero-knowledge machine learning.Cryptology ePrint Archive, 2025

    Tiancheng Xie, Tao Lu, Zhiyong Fang, Siqi Wang, Zhenfei Zhang, Yongzheng Jia, Dawn Song, and Jiaheng Zhang. zkpytorch: A hierarchical optimized compiler for zero-knowledge machine learning.Cryptology ePrint Archive, 2025

    work page 2025

  26. [26]

    famulet: Finding finalization failure bugs in polygon zkrollup

    Zihao Li, Xinghao Peng, Zheyuan He, Xiapu Luo, and Ting Chen. famulet: Finding finalization failure bugs in polygon zkrollup. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, pages 971–985, 2024

    work page 2024

  27. [27]

    Fuzzing processing pipelines for zero-knowledge circuits

    Christoph Hochrainer, Anastasia Isychev, Valentin Wüstholz, and Maria Christakis. Fuzzing processing pipelines for zero-knowledge circuits. InProceedings of the 2025 ACM SIGSAC Conference on Computer and Communica- tions Security, pages 783–797, 2025

    work page 2025

  28. [28]

    Towards Fuzzing Zero-Knowledge Proof Circuits (Short Paper)

    Stefanos Chaliasos, Imam Al-Fath, and Alastair Donaldson. Towards fuzzing zero-knowledge proof circuits (short paper). InProceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 98–104, 2025

    work page 2025

  29. [29]

    Automated soundness and completeness vetting of polygon {zkEVM}

    Xinghao Peng, Zhiyuan Sun, Kunsong Zhao, Zuchao Ma, Zihao Li, Jinan Jiang, Xiapu Luo, and Yinqian Zhang. Automated soundness and completeness vetting of polygon {zkEVM}. In34th USENIX Security Symposium (USENIX Security 25), pages 4093–4108, 2025

    work page 2025

  30. [30]

    Arguzz: Testing zkvms for soundness and completeness bugs.arXiv preprint arXiv:2509.10819, 2025

    Christoph Hochrainer, Valentin Wüstholz, and Maria Christakis. Arguzz: Testing zkvms for soundness and completeness bugs.arXiv preprint arXiv:2509.10819, 2025

    work page arXiv 2025

  31. [31]

    zk-bench: A toolset for comparative evaluation and performance benchmarking of snarks

    Jens Ernstberger, Stefanos Chaliasos, George Kadianakis, Sebastian Steinhorst, Philipp Jovanovic, Arthur Ger- vais, Benjamin Livshits, and Michele Orrù. zk-bench: A toolset for comparative evaluation and performance benchmarking of snarks. InInternational Conference on Security and Cryptography for Networks, pages 46–72. Springer, 2024

    work page 2024

  32. [32]

    Conscs: Effective and efficient verification of circom circuits

    Jinan Jiang, Xinghao Peng, Jinzhao Chu, and Xiapu Luo. Conscs: Effective and efficient verification of circom circuits. In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 737–737. IEEE Computer Society, 2025

    work page 2025

  33. [33]

    Whitefox: White-box compiler fuzzing empowered by large language models.Proceedings of the ACM on Programming Languages, 8(OOPSLA2):709–735, 2024

    Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, and Lingming Zhang. Whitefox: White-box compiler fuzzing empowered by large language models.Proceedings of the ACM on Programming Languages, 8(OOPSLA2):709–735, 2024

    work page 2024

  34. [34]

    Boosting symbolic execution via constraint solving time prediction (experience paper)

    Sicheng Luo, Hui Xu, Yanxiang Bi, Xin Wang, and Yangfan Zhou. Boosting symbolic execution via constraint solving time prediction (experience paper). InProceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 336–347, 2021

    work page 2021

  35. [35]

    Synthesize solving strategy for symbolic execution

    Zhenbang Chen, Zehua Chen, Ziqi Shuai, Guofeng Zhang, Weiyu Pan, Yufeng Zhang, and Ji Wang. Synthesize solving strategy for symbolic execution. InProceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 348–360, 2021

    work page 2021

  36. [36]

    Llm- guided formal verification coupled with mutation testing

    Muhammad Hassan, Sallar Ahmadi-Pour, Khushboo Qayyum, Chandan Kumar Jha, and Rolf Drechsler. Llm- guided formal verification coupled with mutation testing. In2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1–2. IEEE, 2024. 21 zkCraft

    work page 2024

  37. [37]

    Mutation-guided llm-based test generation at meta

    Mark Harman, Jillian Ritchey, Inna Harper, Shubho Sengupta, Ke Mao, Abhishek Gulati, Christopher Foster, and Hervé Robert. Mutation-guided llm-based test generation at meta. InProceedings of the 33rd ACM International Conference on the Foundations of Software Engineering, pages 180–191, 2025

    work page 2025

  38. [38]

    Mutation testing via iterative large language model-driven scientific debugging

    Philipp Straubinger, Marvin Kreis, Stephan Lukasczyk, and Gordon Fraser. Mutation testing via iterative large language model-driven scientific debugging. In2025 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pages 358–367. IEEE, 2025

    work page 2025

  39. [39]

    From evaluation to enhancement: Large language models for zero-knowledge proof code generation.arXiv preprint arXiv:2509.11708, 2025

    Zhantong Xue, Pingchuan Ma, Zhaoyu Wang, and Shuai Wang. From evaluation to enhancement: Large language models for zero-knowledge proof code generation.arXiv preprint arXiv:2509.11708, 2025

    work page arXiv 2025

  40. [40]

    Large language model powered symbolic execution.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3148–3176, 2025

    Yihe Li, Ruijie Meng, and Gregory J Duck. Large language model powered symbolic execution.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3148–3176, 2025

    work page 2025

  41. [41]

    Enhancing symbolic execution with machine-checked safety proofs

    David Trabish and Shachar Itzhaky. Enhancing symbolic execution with machine-checked safety proofs. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 294–308, 2026

    work page 2026

  42. [42]

    Formalizing soundness proofs of linear {PCP}{SNARKs}

    Bolton Bailey and Andrew Miller. Formalizing soundness proofs of linear {PCP}{SNARKs}. In33rd USENIX Security Symposium (USENIX Security 24), pages 1489–1506, 2024

    work page 2024

  43. [43]

    Machine-checked zkp for np relations: Formally verified security proofs and implementations of mpc-in-the-head

    José Bacelar Almeida, Manuel Barbosa, Manuel L Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, and Vitor Pereira. Machine-checked zkp for np relations: Formally verified security proofs and implementations of mpc-in-the-head. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, pages 2587–2600, 2021

    work page 2021

  44. [44]

    Zilch: A framework for deploying transparent zero-knowledge proofs.IEEE Transactions on Information Forensics and Security, 16:3269–3284, 2021

    Dimitris Mouris and Nektarios Georgios Tsoutsos. Zilch: A framework for deploying transparent zero-knowledge proofs.IEEE Transactions on Information Forensics and Security, 16:3269–3284, 2021

    work page 2021

  45. [45]

    Circom: A circuit description language for building zero-knowledge applications.IEEE Transactions on Dependable and Secure Computing, 20(6):4733–4751, 2022

    Marta Bellés-Muñoz, Miguel Isabel, Jose Luis Muñoz-Tapia, Albert Rubio, and Jordi Baylina. Circom: A circuit description language for building zero-knowledge applications.IEEE Transactions on Dependable and Secure Computing, 20(6):4733–4751, 2022

    work page 2022

  46. [46]

    Efficient representation of numerical optimization problems for {SNARKs}

    Sebastian Angel, Andrew J Blumberg, Eleftherios Ioannidis, and Jess Woods. Efficient representation of numerical optimization problems for {SNARKs}. In31st USENIX Security Symposium (USENIX Security 22), pages 4273–4290, 2022

    work page 2022

  47. [47]

    Gzkp: A gpu accelerated zero-knowledge proof system

    Weiliang Ma, Qian Xiong, Xuanhua Shi, Xiaosong Ma, Hai Jin, Haozhao Kuang, Mingyu Gao, Ye Zhang, Haichen Shen, and Weifang Hu. Gzkp: A gpu accelerated zero-knowledge proof system. InProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, pages 340–353, 2023

    work page 2023

  48. [48]

    if-zkp: Intel fpga-based acceleration of zero knowledge proofs

    Shahzad Ahmad Butt, Benjamin Reynolds, Veeraraghavan Ramamurthy, Xiao Xiao, Pohrong Chu, Setareh Sharifian, Sergey Gribok, and Bogdan Pasca. if-zkp: Intel fpga-based acceleration of zero knowledge proofs. arXiv preprint arXiv:2412.12481, 2024

    work page arXiv 2024

  49. [49]

    Accelerating zero-knowledge proofs through hardware-algorithm co-design

    Nikola Samardzic, Simon Langowski, Srinivas Devadas, and Daniel Sanchez. Accelerating zero-knowledge proofs through hardware-algorithm co-design. In2024 57th IEEE/ACM International Symposium on Microarchitecture (MICRO), pages 366–379. IEEE, 2024

    work page 2024

  50. [50]

    Tabby: A synthesis-aided compiler for high-performance zero-knowledge proof circuits.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):1671–1697, 2025

    Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Luke Pearson, Yanju Chen, and Yu Feng. Tabby: A synthesis-aided compiler for high-performance zero-knowledge proof circuits.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):1671–1697, 2025

    work page 2025

  51. [51]

    Circ: Compiler infrastructure for proof systems, software verification, and more

    Alex Ozdemir, Fraser Brown, and Riad S Wahby. Circ: Compiler infrastructure for proof systems, software verification, and more. In2022 IEEE Symposium on Security and Privacy (SP), pages 2248–2266. IEEE, 2022

    work page 2022

  52. [52]

    Certifying zero-knowledge circuits with refinement types

    Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, I¸ sıl Dillig, and Yu Feng. Certifying zero-knowledge circuits with refinement types. In2024 IEEE Symposium on Security and Privacy (SP), pages 1741–1759. IEEE, 2024

    work page 2024

  53. [53]

    Zero-knowledge proof-based verifiable decentralized machine learning in communication network: A comprehensive survey.IEEE Communications Surveys & Tutorials, 2025

    Zhibo Xing, Zijian Zhang, Ziang Zhang, Zhen Li, Meng Li, Jiamou Liu, Zongyang Zhang, Yi Zhao, Qi Sun, Liehuang Zhu, et al. Zero-knowledge proof-based verifiable decentralized machine learning in communication network: A comprehensive survey.IEEE Communications Surveys & Tutorials, 2025. 22 zkCraft

    work page 2025

  54. [54]

    A zero-knowledge proof-enabled blockchain- based academic record verification system.Sensors, 25(11):3450, 2025

    Juan Alamrio Berrios Moya, John Ayoade, and Md Ashraf Uddin. A zero-knowledge proof-enabled blockchain- based academic record verification system.Sensors, 25(11):3450, 2025

    work page 2025

  55. [55]

    Zk-gene: A zero-knowledge proof framework for secure genetic marker verification

    Sarthak Gangurde, Ashwini Jadhav, Vijay Gatkal, and Mansi More. Zk-gene: A zero-knowledge proof framework for secure genetic marker verification. In2025 Global Conference in Emerging Technology (GINOTECH), pages 1–5. IEEE, 2025

    work page 2025

  56. [56]

    A Survey on the Applications of Zero-Knowledge Proofs

    Ryan Lavin, Xuekai Liu, Hardhik Mohanty, Logan Norman, Giovanni Zaarour, and Bhaskar Krishnamachari. A survey on the applications of zero-knowledge proofs.arXiv preprint arXiv:2408.00243, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  57. [57]

    Sok: Understanding zk-snarks: The gap between research and practice.arXiv preprint arXiv:2502.02387, 2025

    Junkai Liang, Daqi Hu, Pengfei Wu, Yunbo Yang, Qingni Shen, and Zhonghai Wu. Sok: Understanding zk-snarks: The gap between research and practice.arXiv preprint arXiv:2502.02387, 2025

    work page arXiv 2025

  58. [58]

    Securing smart manufacturing by integrating anomaly detection with zero-knowledge proofs

    Abdu Salam, Mohammad Abrar, Farhan Amin, Faizan Ullah, Izaz Ahmad Khan, Bader Fahad Alkhamees, and Hussain AlSalman. Securing smart manufacturing by integrating anomaly detection with zero-knowledge proofs. IEEE Access, 12:36346–36360, 2024

    work page 2024

  59. [59]

    Mecat: Memory-safe smart contracts in arm trustzone.IEEE Access, 12:56110–56119, 2024

    Seonghwan Park, Hayoung Kang, Sanghun Han, Jonghee M Youn, and Donghyun Kwon. Mecat: Memory-safe smart contracts in arm trustzone.IEEE Access, 12:56110–56119, 2024

    work page 2024

  60. [60]

    Zk-senselm: Veri- fiable large-model wireless sensing with selective abstention and zero-knowledge attestation.arXiv preprint arXiv:2510.25677, 2025

    Hasan Akgul, Mari Eplik, Javier Rojas, Aina Binti Abdullah, and Pieter van der Merwe. Zk-senselm: Veri- fiable large-model wireless sensing with selective abstention and zero-knowledge attestation.arXiv preprint arXiv:2510.25677, 2025

    work page arXiv 2025

  61. [61]

    Qcrmut: Quantum circuit random mutant generator tool.arXiv preprint arXiv:2410.01415, 2024

    Sinhué García Gil, Luis Llana Díaz, and José Ignacio Requeno Jarabo. Qcrmut: Quantum circuit random mutant generator tool.arXiv preprint arXiv:2410.01415, 2024

    work page arXiv 2024

  62. [62]

    Parallel equivalence checking of stabilizer quantum circuits on gpus

    Muhammad Osama, Dimitrios Thanos, and Alfons Laarman. Parallel equivalence checking of stabilizer quantum circuits on gpus. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 109–128. Springer, 2025

    work page 2025

  63. [63]

    zkfuzz: Foundation and framework for effective fuzzing of zero-knowledge circuits.arXiv preprint arXiv:2504.11961, 2025

    Hideaki Takahashi, Jihwan Kim, Suman Jana, and Junfeng Yang. zkfuzz: Foundation and framework for effective fuzzing of zero-knowledge circuits.arXiv preprint arXiv:2504.11961, 2025

    work page internal anchor Pith review arXiv 2025

  64. [64]

    Non-interactive zero-knowledge and its applications

    Manuel Blum, Paul Feldman, and Silvio Micali. Non-interactive zero-knowledge and its applications. InProviding sound foundations for cryptography: on the work of Shafi Goldwasser and Silvio Micali, pages 329–349. 2019

    work page 2019

  65. [65]

    Snarkprobe: An automated security analysis framework for zksnark implementations

    Yongming Fan, Yuquan Xu, and Christina Garman. Snarkprobe: An automated security analysis framework for zksnark implementations. InInternational Conference on Applied Cryptography and Network Security, pages 340–372. Springer, 2024

    work page 2024

  66. [66]

    Ac4: Algebraic computation checker for circuit constraints in zkps.arXiv preprint arXiv:2403.15676, 2024

    Hao Chen, Guoqiang Li, Minyu Chen, Ruibang Liu, and Sinka Gao. Ac4: Algebraic computation checker for circuit constraints in zkps.arXiv preprint arXiv:2403.15676, 2024. 6 Theoretical Additions 6.1 Binding property and block-Vandermonde construction We formalize the linear mapping that relates the Row-V ortex coefficient vector to the pair(δ, c) and state ...

    work page arXiv 2024