Pith. sign in

REVIEW 3 major objections 7 minor 97 references

ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges

T0 review · 3 major / 7 minor · reviewed 2026-07-30 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Automated ZKP security tools catch under half of real bugs on isolated circuits and under a fifth on full projects.

desk verdict Solid empirical SoK: the isolated-to-project detection drop and the zkVM FV gap map are real contributions; adjudication and Circom-only scope are disclosed limits, not collapse points. read the letter →

arxiv 2607.23752 v1 pith:OX6Z4ETY submitted 2026-07-26 cs.CR

Arman Kolozyan , Tom Sorger , Alexander Hicks , Stefanos Chaliasos This is my paper · ORCID
classification cs.CR
keywords zero-knowledgeproofssecuritytoolingCircomformalverificationzkVMunderconstrainedcircuitspractitionersurveybugdetection
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Zero-knowledge proof systems now secure large sums of money and sensitive identity data, yet subtle bugs in circuits or surrounding code can let attackers forge proofs. This paper maps the security tools and formal-verification efforts built to catch those bugs, then measures how well the tools actually work. On 70 real Circom vulnerabilities, at least one of six open-source tools finds 45.7 percent of the bugs when the vulnerable fragment is isolated, but only 19.6 percent when the same bug sits inside its full project. Formal verification mostly proves constraint soundness and leaves witness generators, proof backends, and verifiers largely unchecked. A survey of 48 practitioners shows that development and auditing stay human-led, that large language models are already common, and that teams want clearer guarantees and lower integration cost. The central message is that today’s tooling is useful for local underconstraint checks but does not yet give system-level assurance, so integration with real workflows must improve.

What carries the argument

A dual-mode evaluation harness that runs the same 70 real Circom bugs once as isolated vulnerable fragments and once inside their original project codebases, scoring true-positive detection under a fixed timeout, paired with a systematic classification of formal-verification efforts by goal, model-construction method, and trusted computing base.

What would settle it

Re-run the six tools on an expanded set that includes non-Circom DSLs and zkVM guest programs, count both true and false positives on full projects, and check whether cumulative detection stays near 20 percent or rises substantially.

Watch

Extended reading notes

Core claim

Across 70 real-world Circom vulnerabilities, at least one of six automated open-source tools detects 45.7 percent of bugs in isolated wrappers but only 19.6 percent on full project codebases, leaving important classes such as circuit-design issues and many semantic mismatches unaddressed; formal-verification work likewise concentrates on constraint-correctness soundness while witness generators, lookup arguments, proof backends, and verifiers remain largely unverified.

Load-bearing premise

That true-positive detection on this Circom bug set, with manual judgment when a tool does not name the exact ground-truth location, is a fair proxy for real-world tool effectiveness even without false-positive rates or non-Circom languages.

Editorial extensions

If this is right

  • Developers should treat current automated tools as focused fragment checkers, not whole-project oracles.
  • Tool builders need language-agnostic or multi-DSL support beyond Circom and must expand past nondeterminism.
  • Formal-verification roadmaps should move from isolated constraint-soundness proofs to CI-friendly end-to-end claims with explicit trusted bases.
  • Practitioners will keep relying on human review and LLMs until integration cost and report clarity improve.
  • Reusable, versioned specifications can serve testing, fuzzing, static analysis, and proof assistants at once.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The sharp isolated-to-project drop suggests that scalability and environment fragility, not just missing detectors, are first-order barriers to adoption.
  • Because practitioners already use LLMs heavily yet distrust them on circuit- and proof-system bugs, the near-term path is verified acceleration: models propose artifacts that independent checkers and humans ratify.
  • If autoprecompiles proliferate, verification effort must shift from hand-checking each circuit to validating the generators that produce them.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 7 minor

Summary. The paper presents a four-part empirical study of ZKP security tooling: (RQ1) a systematization of circuit-analysis tools by target, technique, and vulnerability coverage; (RQ2) a quantitative evaluation of six open-source, non-interactive Circom tools against an extended dataset of 70 real-world vulnerabilities, run in isolated wrappers and on full project codebases; (RQ3) a systematic analysis of formal-verification efforts across the zkVM stack, organized around explicit verification goals (CC-S/CC-C, WC, PS, VC, PC), model-creation approaches, and trusted-computing-base accounting; and (RQ4/RQ5) a survey of 48 practitioners on tool adoption, barriers, and perceived gaps. Headline results: at least one tool detects 45.7% of bugs in isolated mode but only 19.6% in project mode; FV efforts concentrate on constraint-correctness soundness while witness generators, lookup/permutation arguments, proof backends, and verifiers remain largely unverified; workflows are human-led with mainstream LLM use.

Significance. If the results hold, this is a useful and timely reference point for the ZKP security community. Three strengths deserve explicit credit. First, the evaluation uses real-world vulnerabilities from audits and disclosures rather than tool-tailored benchmarks, extends the Chaliasos et al. Circom dataset from 29 to 70 bugs, and the dual isolated/project design yields a genuinely informative finding (the 45.7%→19.6% drop) that tool papers' own evaluations obscure. Second, the reproducibility posture is strong: the extended dataset, harness, raw tool outputs, and anonymized survey data are all public, which lets others audit the detection labels directly. Third, Section VI is, to my knowledge, the first systematic treatment of zkVM formal verification with a precise decomposition of verification goals and an explicit TCB analysis (including the often under-reported point that theorem statements and solver encodings are themselves part of the TCB); this section alone is a valuable contribution. The survey is smaller in novelty but consistent with prior practitioner studies and usefully quantifies the LLM-adoption picture.

major comments (3)
  1. [§III-B (Execution and Metrics), §V] The headline 45.7%/19.6% figures rest on the 'detected' label, whose assignment procedure is under-specified. Several evaluated tools (Picus, Ecne, CIVER in automatic mode) emit a global underconstraint/nondeterminism verdict, possibly with a candidate witness or signal set, rather than a line-level diagnosis. The manual step that credits such a verdict as a TP has no stated adjudication rule (e.g., required overlap between flagged signals and the annotated vulnerable location), no blinding, and no inter-rater agreement statistic. Because false positives are deliberately not measured, a verbose tool is never penalized, and the manual matching step is exactly where verbosity could convert into credited detections. Two mitigating factors: (i) raw outputs and annotations are public, so the labels are auditable; (ii) any inflation here biases detection rates upward, i.e., against the paper's
  2. [§V (Overall effectiveness; Isolated versus project analysis), Abstract] The 45.7% (n=70) vs 19.6% (n=56) comparison uses different denominators: 14 projects fail to compile in project mode, and those failures are plausibly correlated with bug detectability (stale/deprecated codebases). The paired analysis later in the section — among the 56 bugs compiling in both modes, 31 missed in both, 6 detected in both, 14 detected only in isolated mode — is the cleaner basis for the isolated-vs-project claim and implies an isolated-mode rate of 20/56 ≈ 35.7% on the comparable subset, not 45.7%. The abstract and RQ2 key findings lead with the cross-denominator comparison. This does not reverse the conclusion (a substantial drop remains), but the headline should either use the paired subset or explicitly flag the denominator change.
  3. [§V (Detection by root cause, Table IV), Abstract] The 0/6 detection rate for 'circuit-design issue' bugs (and 0–1/3 for specification misimplementations) is presented as part of the empirical finding that 'important vulnerability classes [are] left unaddressed,' but Table III already establishes that no evaluated tool claims support for these classes — the result is substantially by construction rather than an empirical discovery. The RQ1 coverage analysis is fine on its own; the issue is the framing in the abstract and §V takeaways, where a definitional zero is folded into the measured-effectiveness narrative. The paper should either separate 'tools fail on classes they target' from 'classes no tool targets' in the RQ2 presentation, or temper the abstract phrasing.
minor comments (7)
  1. [§III-B, §V (Operational limitations)] The 600s timeout on a fixed VM (8 vCPUs / 32 GB) is a free parameter of the measurement: timeout counts as non-detection, so the TP rates are partly a function of this budget. CIVER alone has 14 timeouts in isolated mode. A brief sensitivity statement (e.g., how many timeouts produce partial output, or what happens at 2× budget) would help readers calibrate.
  2. [§V (Operational limitations)] The claim that ECNE and CIRCOMSPECT are 'substantially noisier' is the only false-positive statement in the paper and is anecdotal ('our use of the tools on real codebases revealed'). Since FP rates are explicitly out of scope, either give a rough count from the harness logs or soften the sentence.
  3. [§VII, Table I, Table VI, Fig. 4] Auditor percentages throughout §VII rest on n=12 (e.g., '83% of auditors' is 10 respondents; Table VI's covered/hard cells are similarly small). Percentages without denominators invite over-reading; please report n per question, especially since all questions were optional.
  4. [§III-C, §VIII (Threats to validity)] Respondent recruitment via personal channels to 200 practitioners at high-profile organizations introduces self-selection and familiarity biases; the threats-to-validity paragraph mentions representativeness but not that personal-channel recruitment may skew toward tool-friendly respondents. One sentence would suffice.
  5. [§VI, Table V] Table V is dense and valuable, but the 'Model' column mixes citations with approach labels in a way that requires flipping back to §VI-B; consider adding the E/T/M/CbC letter codes to the table for readability.
  6. [§V (Isolated versus project analysis)] The paired-mode counts in §V (31/6/14) sum to 51, not 56; please account for the remaining 5 (presumably error/timeout in at least one mode) explicitly.
  7. [Fig. 2] Fig. 2 is hard to parse in the text-only form; per-tool numbers would benefit from a small table in addition to the stacked bars.

Circularity Check

1 steps flagged · score 1.0 of 10

Empirical measurement paper; no derivation-by-construction. Minor self-citation supplies the starting bug corpus but does not force the detection rates or conclusions.

  1. self citation load bearing [Section III-B Dataset; also RQ1 vulnerability mapping to [7], [15]]
    "We extend the dataset introduced by Chaliasos et al. [7], which contains real-world ZKP circuit vulnerabilities. [...] We extend the Circom dataset from 29 to 70 bugs by adding high-severity vulnerabilities from audit reports and public disclosures. [...] Vulnerability coverage was mapped to existing ZKP bug taxonomies [7], [15]"

    The seed corpus and root-cause taxonomy come from prior work with author overlap (Chaliasos). This is ordinary self-citation of a starting dataset, not load-bearing circularity: the paper adds 41 new bugs from external audits/disclosures, evaluates tools the prior work did not evaluate at this scale, and the headline rates (45.7%/19.6%, per-class zeros) are new measurements that are not forced by the citation. Flagged only as minor self-citation of inputs.

full rationale

This is a systematization, tool-evaluation, formal-verification survey, and practitioner-survey paper. Its central quantitative claims (45.7% isolated / 19.6% project true-positive detection across 70/56 Circom bugs; concentration of FV on constraint soundness; LLM adoption and trait rankings from 48 practitioners) are measurements against external artifacts: public tools, an extended audit/disclosure bug set, published FV efforts, and survey responses. Detection labels are assigned by comparing tool output to ground-truth annotations from the extended Chaliasos et al. corpus, not by defining effectiveness in terms of the tools' own scores. Self-citations to overlapping authors' prior taxonomy/dataset work ([7], [15]) supply the starting corpus and vulnerability classes, but the paper extends the set from 29 to 70 bugs, re-runs tools in a new harness, and reports independent outcomes (including large miss rates and class-level zeros). That is ordinary incremental empirical work, not circularity. Manual adjudication when a tool does not name the ground-truth location is a measurement-validity concern (asymmetric TP credit, no FP rates), not a self-definitional or fitted-input loop. No uniqueness theorem, ansatz, or renamed known result is load-bearing. Score 1 for non-load-bearing self-citation of the seed dataset only.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

Load-bearing premises are methodological choices standard to empirical security-tool studies, not fitted physical constants or new ontological entities. The central effectiveness claim rests on the representativeness of the Circom bug corpus, the correctness of manual TP adjudication, the 600s timeout and hardware envelope, and the non-interactive/no-spec tool configuration. FV conclusions rest on the authors’ classification of public materials for closed and open efforts. Survey conclusions rest on self-selected experienced practitioners reached through personal networks.

free parameters (2)
  • tool_timeout_seconds = 600
    Fixed 600-second per-run cutoff on the evaluation VM; directly affects timeout vs detected/missed counts especially for SMT-heavy tools in project mode.
  • evaluation_vm_resources = 8 vCPU / 32 GB / 2.4 GHz
    8 vCPUs, 32 GB RAM, AMD EPYC-Milan 2.4 GHz define the operational envelope in which errors and timeouts are measured.
assumptions (5)
  • domain assumption True-positive detection against ground-truth audit/disclosure locations (with dual manual review when reports are indirect) is a valid primary effectiveness metric even without false-positive rates.
    Stated in Section III-B; FP analysis deferred to future work while headline rates are still used to judge practical value.
  • domain assumption Circom is a sufficiently representative DSL for quantitative claims about automated ZKP security tooling effectiveness today.
    Justified in III-B by tool concentration and deployment maturity; limits external validity to newer DSLs and zkVMs acknowledged in threats.
  • domain assumption Public papers, docs, and code suffice to classify closed-source tools and FV efforts by target, technique, scope, and TCB.
    Corpus rule in III-A; misclassification risk if public material is incomplete.
  • domain assumption Standard survey methodology (pilots, optional items, inductive coding of free text) yields interpretable adoption and gap signals from a convenience sample of high-impact practitioners.
    Section III-C; 200 contacted, 48 responses via personal channels.
  • domain assumption Existing ZKP bug taxonomies (Chaliasos et al., Kolozyan et al.) are adequate axes for mapping tool vulnerability coverage.
    Used throughout Sections IV–V and Table III/IV.

how reviews work

0 comments
Cite this review

Pith. "Pith review of ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges." pith.science (2026). https://pith.science/paper/OX6Z4ETY

@misc{pith2026260723752,
  author       = {Pith},
  title        = {Pith review of: ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OX6Z4ETY}},
  note         = {Machine review of arXiv:2607.23752}
}
read the original abstract

Zero-knowledge proofs (ZKPs) have become a core technology for privacy and verifiable computing. They are used to secure blockchains that handle billions of dollars and identity applications dealing with sensitive personal data. However, ZKP systems are complex, and subtle implementation errors can completely break their guarantees, letting attackers forge money or false proofs of identity. Researchers and practitioners have therefore developed a growing set of bug detection and formal verification methods to secure these systems. Yet their real-world effectiveness and adoption remain unclear. In this paper, we aim to shed light on the state of ZKP security tooling. We first systematize the landscape of these tools and observe that most target Circom, leaving newer DSLs and zkVMs with limited support. We then evaluate six tools across 70 real-world vulnerabilities and find that while the tools detect 45.7% of bugs on isolated targets, their effectiveness drops to 19.6% on full codebases, with important vulnerability classes left unaddressed. We also present the first systematic analysis of formal verification efforts, revealing that current work focuses primarily on constraint correctness and identifying key gaps and risks. Finally, we survey 48 practitioners, showing that development and security remain human-led, LLMs are widely used, and practitioners prioritize tools with clearer guarantees and lower integration effort. Overall, our results highlight the need for better integration of security tooling with the development and auditing process, and we provide actionable insights for researchers and practitioners.

Figures

Figures reproduced from arXiv: 2607.23752 by the authors.

Figure 1
Figure 1. Two ways to develop a ZKP application. A ZK-DSL (a) [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Per-tool outcomes in Isolated and Project modes. TABLE IV: Cumulative detection by ground-truth root cause. Root cause Isolated Project Missing input constraints 10/22 (45.5%) 3/18 (16.7%) Logic-to-constraint translation 9/18 (50.0%) 3/13 (23.1%) Unsafe circuit reuse 4/10 (40.0%) 2/7 (28.6%) Assigned but unconstrained 6/6 (100.0%) 2/5 (40.0%) Circuit design issue 0/6 (0.0%) 0/6 (0.0%) Arithmetic field issues 2/4 (50… view at source ↗
Figure 3
Figure 3. The zkVM verification stack: a specification band (reference models) over an implementation band (what runs), linked by compiler and extraction steps. Each artifact is labeled with its verification goal and its relevance to soundness/completeness. TABLE V: Verification efforts across the zkVM stack up to date. Verification goal refers to the goals defined in Section VI-A, with the targeted constraints in brackets fo… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Practitioner survey overview. TABLE VI: Practitioners’ views of vul￾nerabilities and tools (including LLMs). Hard: hard to detect manually. Covered: adequately covered by tools. Class Hard Covered Underconstrained circuits 72% 70% Arithmetic issues 44% 78% Semantic mis…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

97 extracted references · 6 linked inside Pith

  1. [1]

    The knowledge complexity of interactive proof-systems (extended abstract),

    S. Goldwasser, S. Micali, and C. Rackoff, “The knowledge complexity of interactive proof-systems (extended abstract),” inProceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA, R. Sedgewick, Ed. ACM, 1985, pp. 291–304

    1985

  2. [2]

    Zerocash: Decentralized anonymous payments from bitcoin,

    E. Ben-Sasson, A. Chiesa, C. Garman, M. Green, I. Miers, E. Tromer, and M. Virza, “Zerocash: Decentralized anonymous payments from bitcoin,” in2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18-21, 2014. IEEE Computer Society, 2014, pp. 459–474

    2014

  3. [3]

    zklogin: Privacy-preserving blockchain authentication with existing credentials,

    F. Baldimtsi, K. K. Chalkias, Y . Ji, J. Lindstrøm, D. Maram, B. Riva, A. Roy, M. Sedaghat, and J. Wang, “zklogin: Privacy-preserving blockchain authentication with existing credentials,” inProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communi- cations Security, CCS 2024, Salt Lake City, UT, USA, October 14-18, 2024, B. Luo, X. Liao, J....

    2024

  4. [4]

    Analyzing and benchmarking zk-rollups,

    S. Chaliasos, I. Reif, A. Torralba-Agell, J. Ernstberger, A. Kattis, and B. Livshits, “Analyzing and benchmarking zk-rollups,” in6th Conference on Advances in Financial Technologies, AFT 2024, Vienna, Austria, September 23-25, 2024, ser. LIPIcs, R. B ¨ohme and L. Kiffer, Eds., vol

    2024

  5. [5]

    A survey of zero-knowledge proof based verifiable machine learning,

    Z. Peng, T. Wang, C. Zhao, G. Liao, Z. Lin, Y . Liu, B. Cao, L. Shi, Q. Yang, and S. Zhang, “A survey of zero-knowledge proof based verifiable machine learning,”CoRR, vol. abs/2502.18535, 2025

    arXiv 2025

  6. [6]

    On the size of pairing-based non-interactive arguments,

    J. Groth, “On the size of pairing-based non-interactive arguments,” in Advances in Cryptology - EUROCRYPT 2016 - 35th Annual Interna- tional Conference on the Theory and Applications of Cryptographic Techniques, Vienna, Austria, May 8-12, 2016, Proceedings, Part II, ser. Lecture Notes in Computer Science, M. Fischlin and J. Coron, Eds., vol

    2016

  7. [7]

    Sok: What don’t we know? understanding security vulnerabilities in snarks,

    S. Chaliasos, J. Ernstberger, D. Theodore, D. Wong, M. Jahanara, and B. Livshits, “Sok: What don’t we know? understanding security vulnerabilities in snarks,” in33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024, D. Balzarotti and W. Xu, Eds. USENIX Association, 2024

    2024

  8. [8]

    The orchard counterfeiting vulnerability—and next steps,

    Z. Wilcox, J. McGee, and T. Hornby, “The orchard counterfeiting vulnerability—and next steps,” https://forum.zcashcommunity.com/t /the-orchard-counterfeiting-vulnerability-and-next-steps/56015, Jun. 2026, accessed 2026-06-21

    2026

Show all 97 references
  1. [9]

    Attacker drains $2.1M from deprecated Aztec Connect in exploit,

    GNcrypto, “Attacker drains $2.1M from deprecated Aztec Connect in exploit,” https://www.gncrypto.news/news/attacker-drains-2-1m-depre cated-aztec-connect-exploit/, 2026, accessed: 2026-06-18

    2026

  2. [10]

    ZKsync OS bug bounty program,

    Matter Labs, “ZKsync OS bug bounty program,” https://immunefi.com/ bug-bounty/zksync-os/information/, 2026, accessed: 2026-06-18

    2026

  3. [11]

    Circomspect,

    Trail of Bits, “Circomspect,” https://github.com/trailofbits/circomspect, 2024, accessed: 2026-06-18

    2024

  4. [12]

    Practical security analysis of zero-knowledge proof circuits,

    H. Wen, J. Stephens, Y . Chen, K. Ferles, S. Pailoor, K. Charbonnet, I. Dillig, and Y . Feng, “Practical security analysis of zero-knowledge proof circuits,” in33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024, D. Balzarotti and W....

    2024

  5. [13]

    Automated analysis of halo2 circuits,

    F. H. Soureshjani, M. Hall-Andersen, M. Jahanara, J. Kam, J. Gorzny, and M. Ahmadvand, “Automated analysis of halo2 circuits,” inPro- ceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on A...

    2023

  6. [14]

    Pilspector,

    Thibaut Schaeffer, “Pilspector,” https://github.com/Schaeff/pilspector/, 2023

    2023

  7. [15]

    Language-Agnostic Detection of Computation- Constraint Inconsistencies in ZKP Programs Via Value Inference,

    A. Kolozyan, B. Vandenbogaerde, J. Swalens, L. Hoste, S. Chaliasos, and C. De Roover, “Language-Agnostic Detection of Computation- Constraint Inconsistencies in ZKP Programs Via Value Inference,” in 2026 IEEE Symposium on Security and Privacy (SP). Los Alamitos, CA, USA: IEEE ...

    2026

  8. [16]

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

    S. Pailoor, Y . Chen, F. Wang, C. Rodr ´ıguez-N´u˜nez, J. V . Geffen, J. Morton, M. Chu, B. Gu, Y . Feng, and I. Dillig, “Automated detection of under-constrained circuits in zero-knowledge proofs,”Proc. ACM Program. Lang., vol. 7, no. PLDI, pp. 1510–1532, 2023

    2023

  9. [17]

    Certifying zero-knowledge circuits with refine- ment types,

    J. Liu, I. Kretz, H. Liu, B. Tan, J. Wang, Y . Sun, L. Pearson, A. Miltner, I. Dillig, and Y . Feng, “Certifying zero-knowledge circuits with refine- ment types,” inIEEE Symposium on Security and Privacy, SP 2024, San Francisco, CA, USA, May 19-23, 2024. IEEE, 2024, pp. 1741–1759

    2024

  10. [18]

    AC4: algebraic computation checker for circuit constraints in zero-knowledge proofs,

    Q. Yang, B. Liang, H. Chen, and G. Li, “AC4: algebraic computation checker for circuit constraints in zero-knowledge proofs,”Formal As- pects Comput., vol. 38, no. 1, pp. 11:1–11:20, 2026

    2026

  11. [19]

    Automated verification of consis- tency in zero-knowledge proof circuits,

    J. Stephens, S. Pailoor, and I. Dillig, “Automated verification of consis- tency in zero-knowledge proof circuits,” inComputer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23- 25, 2025, Proceedings, Part I, ser. Lecture Notes in Computer ...

    2025

  12. [20]

    zkFuzz: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits ,

    H. Takahashi, J. Kim, S. Jana, and J. Yang, “ zkFuzz: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits ,” in2026 IEEE Symposium on Security and Privacy (SP). Los Alamitos, CA, USA: IEEE Computer Society, May 2026, pp. 3055–3074

    2026

  13. [21]

    Towards fuzzing zero- knowledge proof circuits (short paper),

    S. Chaliasos, I. Al-Fath, and A. F. Donaldson, “Towards fuzzing zero- knowledge proof circuits (short paper),” inProceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA Companion 2025, Clarion Hotel Trondheim, Trondheim, Norway, June...

    2025

  14. [22]

    Formal verification of SP1 Hypercube,

    Succinct Labs, “Formal verification of SP1 Hypercube,” 2025. [Online]. Available: https://blog.succinct.xyz/nethermind-lean/

    2025

  15. [23]

    Announcing formal verification of OpenVM RV32IM constraints in Lean,

    OpenVM, “Announcing formal verification of OpenVM RV32IM constraints in Lean,” 2026, accessed: 2026-06-18. [Online]. Available: https://blog.openvm.dev/fv

    2026

  16. [24]

    Verifying jolt zkvm lookup semantics,

    C. Kwan, Q. Dao, and J. Thaler, “Verifying jolt zkvm lookup semantics,” inFinancial Cryptography and Data Security - 29th International Conference, FC 2025, Miyakojima, Japan, April 14-18, 2025, Revised Selected Papers, Part I, ser. Lecture Notes in Computer Science, C. Garman...

    2025

  17. [25]

    Advanced formal verification of zero-knowledge proof blockchains,

    CertiK, “Advanced formal verification of zero-knowledge proof blockchains,” 2024, accessed: 2026-06-18. [Online]. Available: https: //www.certik.com/resources/blog/advanced-formal-verification-of-zer o-knowledge-proof-blockchains

    2024

  18. [26]

    Formally verifying zero-knowledge circuits: Introducing CertiPlonk,

    Nethermind, “Formally verifying zero-knowledge circuits: Introducing CertiPlonk,” 2025, accessed: 2026-06-18. [Online]. Available: https: //www.nethermind.io/blog/formally-verifying-zero-knowledge-circuit s-introducing-certiplonk

    2025

  19. [27]

    Circom: A circuit description language for building zero- knowledge applications,

    M. Bell ´es-Mu˜noz, M. Isabel, J. L. Mu ˜noz-Tapia, A. Rubio, and J. B. Mel´e, “Circom: A circuit description language for building zero- knowledge applications,”IEEE Trans. Dependable Secur. Comput., vol. 20, no. 6, pp. 4733–4751, 2023

    2023

  20. [28]

    Succinct non- interactive zero knowledge for a von neumann architecture,

    E. Ben-Sasson, A. Chiesa, E. Tromer, and M. Virza, “Succinct non- interactive zero knowledge for a von neumann architecture,” inPro- ceedings of the 23rd USENIX Security Symposium, San Diego, CA, USA, August 20-22, 2014, K. Fu and J. Jung, Eds. USENIX Association, 2014, pp. 781–796

    2014

  21. [29]

    Precompiles,

    RISC Zero, “Precompiles,” https://dev.risczero.com/api/zkvm/precompi les, 2026, accessed: 2026-06-18

    2026

  22. [30]

    Sok: Understanding zkvm: From research to practice,

    G. Yang, Y . Yang, Y . Cheng, H. Tang, B. Zhang, and K. Ren, “Sok: Understanding zkvm: From research to practice,” inProceedings of the ACM Asia Conference on Computer and Communications Security, ASIA CCS 2026, Bangalore, India, June 1-5, 2026, M. Agrawal, I. Molloy, V . Pand...

    2026

  23. [31]

    Jolt: Snarks for virtual machines via lookups,

    A. Arun, S. T. V . Setty, and J. Thaler, “Jolt: Snarks for virtual machines via lookups,” inAdvances in Cryptology - EUROCRYPT 2024 - 43rd Annual International Conference on the Theory and Applications of Cryptographic Techniques, Zurich, Switzerland, May 26-30, 2024, Proceedi...

    2024

  24. [32]

    Personal opinion surveys,

    B. A. Kitchenham and S. L. Pfleeger, “Personal opinion surveys,” in Guide to Advanced Empirical Software Engineering, F. Shull, J. Singer, and D. I. K. Sjøberg, Eds. Springer, 2008, pp. 63–92

    2008

  25. [33]

    What developers want and need from program analysis: an empirical study,

    M. Christakis and C. Bird, “What developers want and need from program analysis: an empirical study,” inProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineer- ing, ASE 2016, Singapore, September 3-7, 2016, D. Lo, S. Apel, and S. Khurshid, Eds...

    2016

  26. [34]

    Smart contract and defi security tools: Do they meet the needs of practitioners?

    S. Chaliasos, M. A. Charalambous, L. Zhou, R. Galanopoulou, A. Ger- vais, D. Mitropoulos, and B. Livshits, “Smart contract and defi security tools: Do they meet the needs of practitioners?” inProceedings of the 46th IEEE/ACM International Conference on Software Engineering, IC...

    2024

  27. [35]

    Conscs: Effective and efficient verification of circom circuits,

    J. Jiang, X. Peng, J. Chu, and X. Luo, “Conscs: Effective and efficient verification of circom circuits,” in47th IEEE/ACM International Confer- ence on Software Engineering, ICSE 2025, Ottawa, ON, Canada, April 26 - May 6, 2025. IEEE, 2025, pp. 616–628

    2025

  28. [36]

    Scalable verification of zero-knowledge protocols,

    M. Isabel, C. Rodr ´ıguez-N´u˜nez, and A. Rubio, “Scalable verification of zero-knowledge protocols,” inIEEE Symposium on Security and Privacy, SP 2024, San Francisco, CA, USA, May 19-23, 2024. IEEE, 2024, pp. 1794–1812

    2024

  29. [37]

    Ecneproject,

    Franklyn Wang, “Ecneproject,” https://github.com/franklynwang/Ecne Project, 2022

    2022

  30. [38]

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

    A. Ozdemir, F. Brown, and R. S. Wahby, “Circ: Compiler infrastructure for proof systems, software verification, and more,” in43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 2022, pp. 2248–2266

    2022

  31. [39]

    LLZK: An MLIR-based intermediate representation for zero- knowledge circuit languages,

    Veridise, “LLZK: An MLIR-based intermediate representation for zero- knowledge circuit languages,” https://github.com/project-llzk/llzk-lib, 2026

    2026

  32. [40]

    SMT solving over finite field arithmetic,

    T. Hader, D. Kaufmann, and L. Kov ´acs, “SMT solving over finite field arithmetic,” inLPAR 2023: Proceedings of 24th International Confer- ence on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023, ser. EPiC Series in Computing,...

    2023

  33. [41]

    Split gr ¨obner bases for satisfiability modulo finite fields,

    A. Ozdemir, S. Pailoor, A. Bassa, K. Ferles, C. W. Barrett, and I. Dillig, “Split gr ¨obner bases for satisfiability modulo finite fields,” inComputer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, ser...

    2024

  34. [42]

    An SMT-LIB theory of finite fields,

    T. Hader and A. Ozdemir, “An SMT-LIB theory of finite fields,” in Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024, ...

    2024

  35. [43]

    Satisfiability modulo finite fields,

    A. Ozdemir, G. Kremer, C. Tinelli, and C. W. Barrett, “Satisfiability modulo finite fields,” inComputer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, ser. Lecture Notes in Computer Science, C. Enea and A. L...

    2023

  36. [44]

    Mcsat-based finite field reasoning in the yices2 SMT solver (short paper),

    T. Hader, D. Kaufmann, A. Irfan, S. Graham-Lengrand, and L. Kov ´acs, “Mcsat-based finite field reasoning in the yices2 SMT solver (short paper),” inAutomated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, ser. ...

    2024

  37. [45]

    An effective orchestral approach to satisfiability modulo prime fields,

    M. Isabel, E. Rodr ´ıguez-Carbonell, C. Rodr´ıguez-N´u˜nez, and A. Rubio, “An effective orchestral approach to satisfiability modulo prime fields,” CoRR, vol. abs/2604.26709, 2026

    2026 arXiv

  38. [46]

    Automating bitvector and finite field equivalence proofs in lean,

    E. Pertseva, V . Robert, C. W. Barrett, and J. Parker, “Automating bitvector and finite field equivalence proofs in lean,”CoRR, vol. abs/2605.15163, 2026

    2026 arXiv

  39. [47]

    Formal verification of the Keccak precompile from Plonky3,

    Formal Land, “Formal verification of the Keccak precompile from Plonky3,” 2026, accessed: 2026-06-18. [Online]. Available: https://formal.land/blog/2026/01/14/formal-verification-keccak-plonky3

    2026

  40. [48]

    We verified the verifier: a first for zero-knowledge proof systems,

    Nethermind, “We verified the verifier: a first for zero-knowledge proof systems,” 2025, accessed: 2026-06-18. [Online]. Available: https://www.nethermind.io/blog/we-verified-the-verifier-a-first-for-zer o-knowledge-proof-systems

    2025

  41. [49]

    Verified zkEVM project,

    Ethereum Foundation, “Verified zkEVM project,” 2025, accessed: 2026-06-18. [Online]. Available: https://verified-zkevm.org

    2025

  42. [50]

    zkVM standards for Ethereum,

    Ethereum Foundation (eth-act), “zkVM standards for Ethereum,” https: //github.com/eth-act/zkvm-standards, 2026

    2026

  43. [51]

    Verifying SP1 circuit determinism with Picus: A collaboration between Veridise and Succinct,

    Veridise, “Verifying SP1 circuit determinism with Picus: A collaboration between Veridise and Succinct,” https://veridise.com/blog/audit-insight s/verifying-sp1-circuit-determinism-with-picus-a-collaboration-betwe en-veridise-and-succinct/, 2025

    2025

  44. [52]

    RISC Zero’s ZK-VM security: How Veridise enabled provable & continuous ZK security,

    ——, “RISC Zero’s ZK-VM security: How Veridise enabled provable & continuous ZK security,” 2025, accessed: 2026-06-18. [Online]. Available: https://veridise.com/blog/audit-insights/risc-zeros-zk-vm-sec urity-how-veridise-enabled-risc-zero-to-achieve-provable-continuous-z k-security/

    2025

  45. [53]

    Formal verification of the s-two AIR,

    J. Avigad, A. Ganor, L. Goldberg, D. Levit, O. Nir, Y . Seginer, and A. Titelman, “Formal verification of the s-two AIR,”CoRR, vol. abs/2606.04311, 2026

    2026 arXiv

  46. [54]

    Formal verification of Halo2 circuits in Lean,

    Nethermind, “Formal verification of Halo2 circuits in Lean,” 2025, accessed: 2026-06-18. [Online]. Available: https://www.nethermind.io/ blog/formal-verification-of-halo2-circuits-in-lean

    2025

  47. [55]

    Releasing OpenVM 2.0 to production,

    Y . Sun, “Releasing OpenVM 2.0 to production,” https://www.axiom.xy z/blog/openvm-2-production, 2026

    2026

  48. [56]

    VCVio: Verified cryptography in lean via oracle effects and handlers,

    D. Tuma, Q. Dao, J. Waters, A. Hicks, and N. Hopper, “VCVio: Verified cryptography in lean via oracle effects and handlers,” Cryptology ePrint Archive, Paper 2026/899, 2026

    2026

  49. [57]

    Introducing Clean, a formal verification DSL for ZK circuits in Lean4,

    G. Dell’Immagine, “Introducing Clean, a formal verification DSL for ZK circuits in Lean4,” https://blog.zksecurity.xyz/posts/clean/, 2025

    2025

  50. [58]

    Consistency verification for zero-knowledge virtual machine on circuit-irrelevant representation,

    J. Ke, B. Liang, and G. Li, “Consistency verification for zero-knowledge virtual machine on circuit-irrelevant representation,”IACR Cryptol. ePrint Arch., vol. 2025, p. 2204, 2025

    2025

  51. [59]

    Clean: Lean circuit dsl,

    G. Mitscha-Baude, “Clean: Lean circuit dsl,” https://github.com/Verifie d-zkEVM/clean, 2026

    2026

  52. [60]

    Charon: An analysis framework for rust,

    S. Ho, G. Boisseau, L. Franceschino, Y . Prak, A. Fromherz, and J. Protzenko, “Charon: An analysis framework for rust,” inComputer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part IV, ser. Lecture Notes in Compu...

    2025

  53. [61]

    Aeneas: Rust verification by functional transla- tion,

    S. Ho and J. Protzenko, “Aeneas: Rust verification by functional transla- tion,”Proc. ACM Program. Lang., vol. 6, no. ICFP, pp. 711–741, 2022

    2022

  54. [62]

    hax: Verifying security-critical rust software using multiple provers,

    K. Bhargavan, M. Buyse, L. Franceschino, L. L. Hansen, F. Kiefer, J. Schneider-Bensch, and B. Spitters, “hax: Verifying security-critical rust software using multiple provers,” inVerified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, Pr...

    2024

  55. [63]

    Verus: Verifying rust programs using linear ghost types,

    A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y . Zhou, J. Howell, B. Parno, and C. Hawblitzel, “Verus: Verifying rust programs using linear ghost types,”Proc. ACM Program. Lang., vol. 7, no. OOPSLA1, pp. 286–315, 2023

    2023

  56. [64]

    zkvm-verus: Ethereum foundation verus evaluation,

    CertiK, “zkvm-verus: Ethereum foundation verus evaluation,” https://gi thub.com/CertiKProject/zkvm-verus, 2026

    2026

  57. [65]

    Simple high-level code for cryptographic arithmetic - with proofs, without compromises,

    A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala, “Simple high-level code for cryptographic arithmetic - with proofs, without compromises,” in2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19-23, 2019. IEEE, 2019, pp. 1202–1219

    2019

  58. [66]

    The trusted computing base of the compcert verified compiler,

    D. Monniaux and S. Boulm ´e, “The trusted computing base of the compcert verified compiler,” inProgramming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, ...

    2022

  59. [67]

    Getting the bugs out of snarks: The road ahead,

    J. Thaler, “Getting the bugs out of snarks: The road ahead,” 2024, accessed: 2026-06-18. [Online]. Available: https://a16zcrypto.com/pos ts/article/getting-bugs-out-of-snarks/

    2024

  60. [68]

    Accelerating Ethereum with autoprecompiles,

    powdr Labs, “Accelerating Ethereum with autoprecompiles,” https://ww w.powdr.org/blog/accelerating-ethereum-with-autoprecompiles, 2025, accessed: 2026-06-18

    2025

  61. [69]

    ArkLib: Formally verified arguments of knowledge,

    Verified-zkEVM, “ArkLib: Formally verified arguments of knowledge,”

  62. [70]

    Algebraic methods for interactive proof systems,

    C. Lund, L. Fortnow, H. J. Karloff, and N. Nisan, “Algebraic methods for interactive proof systems,”J. ACM, vol. 39, no. 4, pp. 859–868, 1992

    1992

  63. [71]

    Fast reed- solomon interactive oracle proofs of proximity,

    E. Ben-Sasson, I. Bentov, Y . Horesh, and M. Riabzev, “Fast reed- solomon interactive oracle proofs of proximity,” in45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, Prague, Czech Republic, July 9-13, 2018, ser. LIPIcs, I. Chatzigiannakis, C. ...

    2018

  64. [72]

    WHIR: reed-solomon proximity testing with super-fast verification,

    G. Arnon, A. Chiesa, G. Fenzi, and E. Yogev, “WHIR: reed-solomon proximity testing with super-fast verification,” inAdvances in Cryptology - EUROCRYPT 2025 - 44th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Madrid, Spain, May 4-8...

    2025

  65. [73]

    A fiat-shamir transformation from duplex sponges,

    A. Chiesa and M. Orr `u, “A fiat-shamir transformation from duplex sponges,” inTheory of Cryptography - 23rd International Conference, TCC 2025, Aarhus, Denmark, December 1-5, 2025, Proceedings, Part I, ser. Lecture Notes in Computer Science, B. Applebaum and H. R. Lin, Eds., ...

    2025

  66. [74]

    Multivariate lookups based on logarithmic derivatives,

    U. Hab ¨ock, “Multivariate lookups based on logarithmic derivatives,” IACR Cryptol. ePrint Arch., vol. 2022, p. 1530, 2022

    2022

  67. [75]

    Twist and shout: Faster memory checking arguments via one-hot addressing and increments,

    S. T. V . Setty and J. Thaler, “Twist and shout: Faster memory checking arguments via one-hot addressing and increments,”IACR Cryptol. ePrint Arch., vol. 2025, p. 105, 2025

    2025

  68. [76]

    On formal verification and a bug in SP1 Hypercube,

    C. Gunton, “On formal verification and a bug in SP1 Hypercube,” 2026, accessed: 2026-06-18. [Online]. Available: https://zkevm.ethere um.foundation/blog/sp1-fv

    2026

  69. [77]

    Verification theatre: False assurance in formally verified cryptographic libraries,

    N. Kobeissi, “Verification theatre: False assurance in formally verified cryptographic libraries,” Cryptology ePrint Archive, Paper 2026/192, 2026

    2026

  70. [78]

    Validity threats in empirical software engineering research - an initial survey,

    R. Feldt and A. Magazinius, “Validity threats in empirical software engineering research - an initial survey,” inProceedings of the 22nd International Conference on Software Engineering & Knowledge Engi- neering (SEKE’2010), Redwood City, San Francisco Bay, CA, USA, July 1 - J...

    2010

  71. [79]

    Zero- knowledge proof vulnerability analysis and security auditing,

    X. Tang, L. Shi, X. Wang, K. Charbonnet, S. Tang, and S. Sun, “Zero- knowledge proof vulnerability analysis and security auditing,”IACR Cryptol. ePrint Arch., vol. 2024, p. 514, 2024

    2024

  72. [80]

    Formal verification of zero- knowledge circuits,

    A. Coglio, E. McCarthy, and E. W. Smith, “Formal verification of zero- knowledge circuits,” inProceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023, ser. EPTCS, A. Coglio and S. Swords, ...

    2023

  73. [81]

    Leo: A programming language for formally verified, zero-knowledge applications,

    C. Chin, H. Wu, R. Chu, A. Coglio, E. McCarthy, and E. Smith, “Leo: A programming language for formally verified, zero-knowledge applications,”IACR Cryptol. ePrint Arch., vol. 2021, p. 651, 2021

    2021

  74. [82]

    Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs,

    A. Ozdemir, R. S. Wahby, F. Brown, and C. W. Barrett, “Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs,”Formal Methods Syst. Des., vol. 67, no. 2, pp. 161–188, 2025

    2025

  75. [83]

    Revisiting the nova proof system on a cycle of curves,

    W. D. Nguyen, D. Boneh, and S. T. V . Setty, “Revisiting the nova proof system on a cycle of curves,” in5th Conference on Advances in Financial Technologies, AFT 2023, Princeton, NJ, USA, October 23- 25, 2023, ser. LIPIcs, J. Bonneau and S. M. Weinberg, Eds., vol. 282. Schloss...

    2023

  76. [84]

    How to prove false statements: Practical attacks on fiat-shamir,

    D. Khovratovich, R. D. Rothblum, and L. Soukhanov, “How to prove false statements: Practical attacks on fiat-shamir,” inAdvances in Cryptology - CRYPTO 2025 - 45th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2025, Proceedings, Part VI, ser...

    2025

  77. [85]

    MTZK: testing and exploring bugs in zero-knowledge (ZK) compilers,

    D. Xiao, Z. Liu, Y . Peng, and S. Wang, “MTZK: testing and exploring bugs in zero-knowledge (ZK) compilers,” in32nd Annual Network and Distributed System Security Symposium, NDSS 2025, San Diego, California, USA, February 24-28, 2025. The Internet Society, 2025

    2025

  78. [86]

    Fuzzing processing pipelines for zero-knowledge circuits,

    C. Hochrainer, A. Isychev, V . W ¨ustholz, and M. Christakis, “Fuzzing processing pipelines for zero-knowledge circuits,” inProceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, CCS 2025, Taipei, Taiwan, October 13-17, 2025, C. Huang, J. Chen, ...

    2025

  79. [87]

    Towards a formal foundation for blockchain ZK rollups,

    S. Chaliasos, D. Firsov, and B. Livshits, “Towards a formal foundation for blockchain ZK rollups,” inProceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, CCS 2025, Taipei, Taiwan, October 13-17, 2025, C. Huang, J. Chen, S. Shieh, D. Lie, and V...

    2025

  80. [88]

    A practical rollup escape hatch design,

    F. G. Figueira, M. Derka, C. L. Chiu, and J. Gorzny, “A practical rollup escape hatch design,” in2025 IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2025, Pisa, Italy, June 2-6,

    2025

  81. [89]

    Unaligned incentives: Pricing attacks against blockchain rollups,

    S. Chaliasos, C. Swann, S. Pilehchiha, N. Mohnblatt, B. Livshits, and A. Kattis, “Unaligned incentives: Pricing attacks against blockchain rollups,”CoRR, vol. abs/2509.17126, 2025

    2025

  82. [90]

    Automated soundness and completeness vetting of polygon zkevm,

    X. Peng, Z. Sun, K. Zhao, Z. Ma, Z. Li, J. Jiang, X. Luo, and Y . Zhang, “Automated soundness and completeness vetting of polygon zkevm,” in 34th USENIX Security Symposium, USENIX Security 2025, Seattle, WA, USA, August 13-15, 2025, L. Bauer and G. Pellegrino, Eds. USENIX Asso...

    2025

  83. [91]

    Arguzz: Testing zkvms for soundness and completeness bugs,

    C. Hochrainer, V . W ¨ustholz, and M. Christakis, “Arguzz: Testing zkvms for soundness and completeness bugs,”CoRR, vol. abs/2509.10819, 2025

    2025 arXiv

  84. [92]

    A survey on ethereum systems security: Vulnerabilities, attacks, and defenses,

    H. Chen, M. Pendleton, L. Njilla, and S. Xu, “A survey on ethereum systems security: Vulnerabilities, attacks, and defenses,”ACM Comput. Surv., vol. 53, no. 3, pp. 67:1–67:43, 2021

    2021

  85. [93]

    Towards safer smart contracts: A survey of languages and verification methods,

    D. Harz and W. J. Knottenbelt, “Towards safer smart contracts: A survey of languages and verification methods,”CoRR, vol. abs/1809.09805, 2018

    2018 arXiv

  86. [94]

    Ethereum smart contract analysis tools: A systematic review,

    S. S. Kushwaha, S. Joshi, D. Singh, M. Kaur, and H. Lee, “Ethereum smart contract analysis tools: A systematic review,”IEEE Access, vol. 10, pp. 57 037–57 062, 2022

    2022

  87. [316]

    6:1–6:24

    Schloss Dagstuhl - Leibniz-Zentrum f ¨ur Informatik, 2024, pp. 6:1–6:24

    2024

  88. [2025]

    Available: https://github.com/Verified-zkEVM/ArkLib

    [Online]. Available: https://github.com/Verified-zkEVM/ArkLib

  89. [9666]

    Springer, 2016, pp. 305–326

    2016

Pith tools

Reviewed July 30, 2026 · model on record in the stance chip above.