{"id":"1fc6c5b0-92e5-4e2d-a711-c59b00d3ad4b","arxiv_id":"2607.23752","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"low","formal_verification":"none","parameter_count":2,"one_line_summary":"Six Circom-focused ZKP tools detect 45.7% of 70 real bugs in isolation but only 19.6% on full codebases; formal verification is mostly constraint-soundness, and practitioners still run human-led workflows with heavy LLM use.","lead":"ZKP security tools catch under half of real bugs on isolated circuits and under a fifth on full projects, while formal verification mostly covers constraint soundness. The study maps tool gaps and practitioner needs for systems that secure large blockchains and identity apps.","discovery_kind":"extension","skeptic_critique":{"model":"moonshotai/kimi-k3","headline":"\"Detected\" is credited even when a tool never names the ground-truth location; for tools emitting a global underconstraint verdict, manual adjudication may credit detection without the tool actually localizing or characterizing the bug — inflating the 45.7%/19.6% rates.","rationale":"I agree with the reader that the external-validity limits (Circom-only, 600s timeout, no FP rates, survey selection) are disclosed and non-fatal. But the reader's weakest_assumption treats \"true-positive detection ... is a sufficient proxy\" at the dataset level, whereas the more specific and more checkable soft spot is one level down: the labeling mechanism itself. Section III-B's manual adjudication when \"a tool reports a vulnerability but does not directly identify the ground-truth location\" is the point where TP credit could be granted loosely, and it interacts with the deliberate absence of FP measurement — a noisy tool faces no penalty, and matching its global alarm to an annotated bug is a judgment call with no reported inter-rater reliability or published decision rule. This is not an accusation of sloppiness; the authors preserved raw outputs precisely to allow re-checking, which is why my proposed test is cheap and decisive. The denominator mismatch (45.7% over 70 vs 19.6% over 56) is a real presentation issue but does not change the direction, since the paired 20/56 vs 11/56 still shows a large drop — so it alone would not move the verdict. The FV-concentration claim (constraint soundness mature; witness generators, lookups, backends, verifiers largely unverified) is a classification claim backed by Table V and specific citations, and I found no load-bearing problem there. Net: the concern is a measurement-precision question on the headline rates, resolvable from the artifact; the qualitative contributions (effectiveness collapse in project mode, coverage concentration, FV gaps, practitioner findings) survive even a moderately stricter adjudication. The reader's ACCEPT with HIGH confidence therefore stands; I would not condition acceptance, but the artifact-based re-adjudication is the single check most worth running before citing the exact percentages.","tokens_in":23794,"tokens_out":2967,"duration_ms":79996,"concrete_test":"Using the public artifact's preserved raw outputs: (1) re-adjudicate the 83 isolated-mode and 14 project-mode TPs under a strict criterion — the tool's flagged signal/location must fall on the vulnerable component named in the ground-truth annotation (e.g., same template/function), with one rater blinded to ground truth and inter-rater agreement reported; (2) recompute union detection on the 56-bug intersection only; (3) for the 41 newly added bugs, record whether the bug was originally discovered with tool assistance. If strict adjudication removes more than ~20% of TPs or several dataset bugs were tool-discovered, the 45.7%/19.6% headline needs recalibration; if TPs survive, the claim is solid.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The headline effectiveness numbers rest on the \"detected\" label. Section III-B states that when a tool reports a vulnerability \"but does not directly identify the ground-truth location, two authors manually inspect the raw output and compare it with the dataset annotation before assigning the final label.\" This is the weakest joint in the measurement. Several evaluated tools (Picus, Ecne, CIVER in automatic mode) output essentially a global property — \"this circuit is underconstrained/nondeterministic\" — possibly with a candidate witness or signal set, not a line-level diagnosis. For a bug whose ground truth is a nondeterminism/underconstraint flaw, crediting TP requires only that the tool's global alarm be judged to \"correspond\" to the annotated bug, a judgment made by the authors without reported inter-rater agreement, blinding, or a published adjudication rule (e.g., required proximity of flagged signals to the ground-truth location). 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. The risk is asymmetric across bug classes: classes the tools nominally target get generous matching, while \"circuit-design issues\" (0/6 detected) are partly unaddressed by construction — tools were never designed to find them — so the \"important classes left unaddressed\" finding is half-empirical, half-definitional. A secondary measurement wrinkle: the 45.7% (n=70) and 19.6% (n=56) are computed on different sets, and the 14 non-compiling projects are enriched for isolated-mode-detectable bugs (32 detected of 70 vs 20 of the 56 intersection). The paired numbers (20/56 vs 11/56) still show the drop, so the direction is safe, but the headline rates as printed compare non-identical cohorts. Finally, provenance of the 41 newly added audit/disclosure bugs is not disclosed; if any were originally found using the evaluated tools or their techniques, the TP-r","agreement_with_reader":"partial"},"referee_report":{"model":"moonshotai/kimi-k3","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.","tokens_in":24084,"tokens_out":2843,"duration_ms":76968,"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":[{"comment":"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","section":"§III-B (Execution and Metrics), §V"},{"comment":"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.","section":"§V (Overall effectiveness; Isolated versus project analysis), Abstract"},{"comment":"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.","section":"§V (Detection by root cause, Table IV), Abstract"}],"minor_comments":[{"comment":"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.","section":"§III-B, §V (Operational limitations)"},{"comment":"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.","section":"§V (Operational limitations)"},{"comment":"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.","section":"§VII, Table I, Table VI, Fig. 4"},{"comment":"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.","section":"§III-C, §VIII (Threats to validity)"},{"comment":"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.","section":"§VI, Table V"},{"comment":"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.","section":"§V (Isolated versus project analysis)"},{"comment":"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.","section":"Fig. 2"}],"recommendation":"minor_revision","confidential_remarks":"Two authors are affiliated with zkSecurity/the Ethereum Foundation and the dataset extends prior work by a co-author (Chaliasos et al.); the self-citation pattern is appropriate and disclosed, and EF funding is acknowledged. The qualitative judgments in §VI reflect authors who are themselves participants in the ecosystem being assessed — the section reads as expert-informed rather than neutral, which I consider a feature for this kind of systematization, but the editor may want to note it. Nothing here rises to a concern about integrity."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The useful core is simple. On an extended 70-bug Circom set, six open-source tools hit 45.7% in isolated wrappers and 19.6% on full projects; the FV section is the first clean stack-wide map showing constraint-soundness concentration and large unverified layers (witness gen, lookups, backends, verifiers); the 48-person survey puts numbers on human-led workflows and LLM use. That package is new relative to prior bug taxonomies.\n\nWhat they did well: dual classification with tie-break, a harness that keeps raw outputs, explicit isolated vs project modes, root-cause tables, and an artifact link. The paired drop on the 56-bug intersection still holds, so the direction is safe even if the printed 45.7/19.6 compare slightly different cohorts. The FV framing (CC-S/CC-C, WC, PS, VC, TCB by modeling choice) is clearer than most blog-and-paper scatter in this area. Survey instruments were piloted; threats are written down.\n\nSoft spots, in proportion. The stress-test on “detected” is fair but not fatal: when a tool only screams global underconstraint, two authors manually match to ground truth with no reported kappa or blinding. That can inflate TPs for the classes tools already target, and FPs are deliberately unmeasured. Still a true-positive capability study, not a precision study—they say so. Quantitative eval is Circom-only; newer DSLs/zkVMs appear only in the landscape and FV map. Survey is convenience-sampled from high-profile orgs (24% of 200). None of that erases the measurements.\n\nMath/data/citations look ordinary and honest: external bug reports, public tools, extended prior dataset, no circular scoring. Self-cites to the taxonomy/dataset are load-bearing prior work, not padding.\n\nWho it is for: anyone building or buying ZKP tooling, allocating audit budget, or choosing a zkVM verification target. Worth a serious referee. I would bring it to reading group and cite the detection drop and FV gap table. Send to peer review.","headline":"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.","tokens_in":25128,"tokens_out":539,"would_cite":true,"duration_ms":12624,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Automated ZKP security tools catch under half of real bugs on isolated circuits and under a fifth on full projects.","keywords":["zero-knowledge proofs","security tooling","Circom","formal verification","zkVM","underconstrained circuits","practitioner survey","bug detection"],"falsifier":"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.","tokens_in":24874,"feed_emoji":"🔐","tokens_out":826,"duration_ms":17443,"temperature":0.7,"pith_summary":"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.","feed_headline":"ZKP tools catch 46% of isolated bugs, 20% in real projects","feed_subtitle":"Six open-source checkers miss most full-codebase flaws; formal proofs stay narrow","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["ZKP tools catch 46% of isolated bugs, only 20% in full codebases","Six ZKP checkers find 45.7% bugs alone, 19.6% in real projects","ZKP security tools miss most full-codebase flaws in 70-bug test","Formal ZKP verification stays narrow; tools leave key bug classes open","Circom tools detect under half of isolated bugs, far less in projects"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["ZKP tools catch 46% of isolated bugs, only 20% in full codebases","Six ZKP checkers find 45.7% bugs alone, 19.6% in real projects","ZKP security tools miss most full-codebase flaws in 70-bug test","Formal ZKP verification stays narrow; tools leave key bug classes open","Circom tools detect under half of isolated bugs, far less in projects"]},"model":"grok-4.5","effort":"low","cost_usd":0.003535,"raw_usage":{"total_tokens":1221,"prompt_tokens":839,"num_sources_used":0,"completion_tokens":93,"cost_in_usd_ticks":35348000,"prompt_tokens_details":{"text_tokens":839,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":289,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":839,"tokens_out":93,"duration_ms":6534,"temperature":1.0,"reasoning_tokens":289,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T13:33:05.433686+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"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.","supporting_citations":[],"review_version":1}