{"id":"783cb152-d61a-4ec6-b6c5-5db7b50d9934","arxiv_id":"2509.10819","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"ARGUZZ combines product-program metamorphic testing with prover fault injection and found three soundness and eight completeness bugs in six zkVMs.","lead":"ARGUZZ is a new fuzzer that tests zero-knowledge virtual machines by running pairs of semantically equivalent programs inside the VM and injecting faults that mimic a malicious prover. It found eleven real bugs in six production zkVMs, including a critical $50,000 soundness bug in RISC Zero.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The metamorphic oracle is not proven semantics-preserving: the 'one-div' rule can rewrite constant 1 to r/r with r=0, causing a Rust panic that ARGUZZ would misreport as a zkVM completeness bug.","rationale":"The reader's weakest_assumption identifies exactly the load-bearing point. The central claim is that ARGUZZ found eleven real zkVM bugs; for the eight completeness bugs, the only oracle is the product-program crash or mismatch, which presupposes that the paired programs are semantically equivalent. Appendix A contains a rule that plainly violates this for $r = 0, and possibly others for signed arithmetic, so the oracle is not established. This is a genuine correctness risk for the tool, not merely a missing artifact. However, the paper has strong independent support for the soundness-bug findings: vendor bounties, fix PRs, and a refinding experiment that reproduced all three soundness bugs. The completeness bugs also have associated developer fixes, so the empirical findings are likely mostly real; the concern is about the reliability of the detection method and whether all eight are zkVM bugs rather than generator-induced crashes. Since the authors do not release ARGUZZ or verify the rule set, a conditional verdict is appropriate. I agree with the reader's CONDITIONAL recommendation and would not change it.","tokens_in":23277,"tokens_out":6523,"duration_ms":61864,"concrete_test":"Run ARGUZZ's rewrite engine on every rule in Appendix A with exhaustive small-width inputs (e.g., all u16 and i16 values, including 0) by compiling original and transformed Rust functions and comparing behavior, including panics and overflow. For 'one-div', instantiate with $r = 0 and confirm the mismatch. Then re-run the completeness-bug campaigns (bugs 2, 4, 5, 7–11) with 'one-div' disabled or with $r constrained to nonzero; if all eight bugs are still reproduced, the oracle flaw does not invalidate the reported findings, but if any disappear, the completeness-bug count is inflated by a generator artifact.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Appendix A's rewrite rule 'one-div' (1 → $r / $r) is applied without any side condition excluding $r = 0. Under Rust semantics, integer division by zero panics, so the transformed Rust function is not semantically equivalent to the original constant 1. Because Step 6 classifies any crash of the product program on the unmodified VM as a completeness bug ('The merged program crashes during execution on the original VM, indicating a completeness bug'), an instantiation with $r = 0 makes ARGUZZ's own oracle produce the crash, which is not a zkVM bug. The same appendix contains other rules whose equivalence depends on generated types; for example, 'and-to-rem' and 'rem-to-and' are not equivalent for signed Rust integers, since '%' preserves the dividend's sign while '&' does not. Since the eight reported completeness bugs form the largest part of the empirical contribution, the semantic preservation of the transformation set is load-bearing. The paper asserts these transformations are 'semantics-preserving' but provides no proof, no exhaustive check, and no constraint on $r for 'one-div'.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents ARGUZZ, a fuzzer for zero-knowledge VMs (zkVMs) that combines a product-program variant of metamorphic testing with fault injection. It generates semantically equivalent Rust program pairs, merges them into a single program with a known output, and runs the merged program inside six real-world zkVMs (RISC Zero, Nexus, Jolt, SP1, OpenVM, Pico). Fault injection into the VM's execution stage mimics a malicious prover to expose overly weak constraints. The paper reports eleven previously unknown bugs across three zkVMs — three soundness bugs and eight completeness bugs — including a RISC Zero soundness bug that earned a $50,000 bounty. Controlled experiments evaluate bug refinding, instruction-coverage gains from an inline-assembly extension, a fairer fault-injection scheduler, and the impact of instruction-modification injection.","tokens_in":23488,"tokens_out":6469,"duration_ms":56938,"significance":"If the results hold, ARGUZZ would be a valuable, first-of-its-kind tool for systematically testing zkVMs, an area of critical and growing importance for blockchain and cryptographic infrastructure. The empirical contribution is notable: the reported bugs were confirmed and fixed by the respective development teams, and the RISC Zero soundness bug survived prior audits. The product-program encoding of the metamorphic oracle is a sensible efficiency improvement, and the fault-injection scheduler is a thoughtful design element. However, the central claim of detecting completeness bugs rests on the semantic preservation of the metamorphic rewrite rules, which is asserted rather than proven; the counterexample in the 'one-div' rule is a concrete threat to the oracle's soundness and therefore to the completeness-bug findings. Reproducibility is also limited by the absence of an artifact and unpinned VM versions.","major_comments":[{"comment":"The rewrite rule 'one-div' in Appendix A (1 → $r/ $r) is not semantics-preserving for $r = 0. In Rust, integer division by zero panics, so the transformed Rust function crashes while the original function returns 1. Since Step 6 in §2 classifies any crash of the product program on the unmodified VM as a completeness bug, a randomly generated $r = 0 would produce a false positive. The same appendix also lists 'and-to-rem' (?a & 1 → ?a % 2) and its reverse, which are equivalent only for unsigned integers; for signed types, negative operands break the equivalence because '%' preserves the dividend's sign while '&' does not. Because eight of the eleven reported bugs are completeness bugs detected via the metamorphic oracle, this unsoundness is load-bearing. Please add a side condition excluding $r = 0 (or another provably semantics-preserving encoding), restrict or justify the signedness assumptions for the modulo/bitwise rules, and re-validate the reported completeness bugs under the corrected rule set.","section":"Appendix A, Step 6"},{"comment":"The experimental setup is not reproducible as reported. The paper tests 'main branches' of six zkVMs at various dates but provides no commit hashes, no build configurations, no Rust toolchain versions, and no artifact or repository link for ARGUZZ itself. Without pinned versions of the systems under test and of the fuzzer, the refinding results in Table 4 and the coverage numbers in RQ4 cannot be verified or compared against the current state of the zkVMs. Please release the ARGUZZ artifact and provide exact commit hashes and setup instructions for all tested zkVMs, as is standard for systems papers in this venue.","section":"§4.1, Experiments in the wild"}],"minor_comments":[{"comment":"The instruction label 'eany' appears in the top plot; this is likely a typographical error for 'ecall' and should be corrected.","section":"Figure 15"},{"comment":"Table 3 reports that the vast majority of instruction-modification injections produce OOPS with a non-zero exit code, but the paper does not discuss whether such crashes were ever investigated as potential completeness bugs and discarded. A brief explanation of the triage process for these cases would clarify the oracle's precision.","section":"§4.2, RQ6"},{"comment":"The CIRCIL-to-Rust translation is described as 'direct and preserves circuit semantics,' but the inline-assembly macro in Figure 6b uses 'register' constraints without specifying a clobber list; the paper should confirm that the assembly snippets are correct under the Rust inline-asm rules and across the tested Rust compiler versions.","section":"Step 3, §3.1"},{"comment":"When discussing the novelty claim, the paper may want to explicitly note that MTZK targets ZK compilers rather than full zkVM execution pipelines, which it already does; adding a sentence on how ARGUZZ's fault-injection mechanism differs from the error-handling fault injection in FUZZERR and similar tools would strengthen the related-work contrast.","section":"§5, Related Work"}],"recommendation":"major_revision","confidential_remarks":"The paper would be much stronger with an artifact release and pinned versions, which would also allow the community to attempt independent refinding of the six reported bugs. The unsoundness of the 'one-div' rewrite is the clearest correctness risk; I believe it is fixable (e.g., by side conditions) and that the reported bugs are likely real, but the authors must address it explicitly. The absence of a baseline comparison with a straightforward adaptation of CIRCUZZ is a minor novelty concern but not an obstacle."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Zhen, read this one. It's the first automated fuzzer aimed at zkVMs, and it found real bugs: three soundness, eight completeness, across RISC Zero, Nexus, and Jolt. The RISC Zero soundness bug got a $50k bounty and was in production despite audits. That alone puts it on the map.\n\nWhat's genuinely new: they take CIRCUZZ's metamorphic testing, move it to the zkVM execution model, merge original and transformed functions into one Rust product program with a known output, and add a fault-injection pass that mimics a malicious prover to expose underconstrained constraints. The inline-assembly extension to CIRCIL gives instruction coverage that plain generation misses. The evaluation is thorough: vendor-acknowledged patches for all but one bug, a refinding study that recovered all soundness bugs within 24h on 5 seeds, and ablation-style analyses of the scheduler and injection types. The writing is clear, and the related work is placed honestly.\n\nSoft spots. The metamorphic oracle is load-bearing and the rewrite rules in Appendix A are asserted rather than proven semantics-preserving. Rule one-div rewrites 1 to $r / $r with no side condition excluding $r=0. In Rust, that division panics, so a transformed program can crash on the unmodified VM and be flagged as a completeness bug when the zkVM did nothing wrong. Similarly, and-to-rem and rem-to-and are not equivalent for signed integers, and the paper never says the generated types are always unsigned. None of the eleven reported bugs look like these artifacts—they're all confirmed by developers—but the tool's own oracle has a false-positive path that should be patched and the remaining rules verified or at least fuzzed for equivalence. Reproducibility also suffers: no artifact, no pinned VM commits, so the in-the-wild findings can't be rerun as-is. The refinding study covered only 10 bugs and missed four completeness bugs, which is honest but leaves those four depending on the un-pinned configuration.\n\nBottom line: the empirical core is as solid as this kind of work gets, and the bugs are real. The formal gap in the rewrite rules is a fixable defect, not a fatal one. Send it to review, but ask for a semantics-preservation argument or automated equivalence check on the transformations, and a released artifact or pinned versions.","headline":"ARGUZZ earns its keep: eleven vendor-confirmed zkVM bugs and a clever product-program oracle, but the rewrite rules need a semantics proof before the completeness claims are airtight.","tokens_in":23993,"tokens_out":3543,"would_cite":true,"duration_ms":28003,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"ARGUZZ found eleven previously unknown bugs in production zkVMs by combining product-program metamorphic testing with malicious-prover fault injection, including a critical RISC Zero soundness flaw worth a $50,000 bounty.","keywords":["zero-knowledge virtual machines","metamorphic testing","product programs","fault injection","soundness bugs","completeness bugs","zkVM fuzzing","RISC-V"],"falsifier":"Re-run ARGUZZ's metamorphic campaigns with the $r / r$ rule (and any rule that introduces a fresh variable, such as add-sub-random-value) guarded by a nonzero condition on $r$ or disabled entirely, and check whether all eight reported completeness bugs still reproduce; any crash that disappears is attributable to the rewrite rule, not the zkVM. As a check on the soundness claims, apply each vendor's patch to the constraint system and confirm that the corresponding fault-injected proof, such as $7 \\bmod 5 = 0$ in RISC Zero, is then rejected by the unmodified verifier.","tokens_in":2052,"feed_emoji":"🐛","tokens_out":3345,"duration_ms":108151,"temperature":0.7,"pith_summary":"ARGUZZ is a fuzzer for zero-knowledge virtual machines (zkVMs), the systems that execute general-purpose Rust programs off-chain and produce succinct proofs of correct execution. The paper claims that two testing ideas, combined, can systematically uncover the two bug classes that matter most in these systems: soundness bugs, where the VM accepts an invalid execution, and completeness bugs, where a valid execution is wrongly rejected. The first idea rewrites a generated circuit into a semantically equivalent variant, merges both into one 'product program' whose expected output is known in advance, and runs it inside the zkVM, so any crash or unexpected output signals a bug. The second idea injects faults into the VM's execution logic at points taken from the real execution trace, imitating a malicious or buggy prover, and checks whether the unmodified verifier still accepts a proof of a wrong result. Applied to six production zkVMs, the tool found eleven previously unknown bugs in three of them, including a RISC Zero soundness bug that earned a $50,000 bounty despite prior audits.","feed_headline":"Fuzzer finds 11 bugs in zkVMs, earns $50,000 bounty","feed_subtitle":"A $50,000 RISC Zero payout shows systematic testing can catch what audits miss.","key_machinery":"The load-bearing object is the product program: instead of executing an original circuit and its transformed twin separately and comparing outputs externally, ARGUZZ compiles both into Rust functions and merges them into a single zkVM program whose expected output is the known constant SUCCESS, returned only when all variants agree. That gives the fuzzer a built-in oracle with no separate checking step, and bundling $k$ variants tests a $k$-safety hyperproperty in one run while paying trace-padding cost once. The second mechanism is instruction-modification fault injection: guided by the trace collected during the normal run, ARGUZZ rewrites one decoded instruction (for example, replacing a remainder's divisor with its dividend) at a deliberately chosen step, so the inconsistency is localized and the rest of the trace re-stabilizes around the faulty state, the configuration most likely to slip past imprecise constraints. A fairness scheduler picks the least-frequently injected instruction, and an inline-assembly extension to the CIRCIL circuit language forces coverage of rare RISC-V instructions such as mulhsu, which is what exposed the Jolt sumcheck failure.","core_discovery":"The central claim is that zkVM correctness can be tested end-to-end without access to the VM's internals beyond its execution stage: generate a random circuit, apply semantics-preserving algebraic rewrites, translate both into Rust, and fuse them into a single product program whose only correct outputs are the constants SUCCESS (all variants agree) and OOPS (they disagree). This turns metamorphic testing into a single-execution oracle while cutting prover overhead, because trace padding to the next power of two is paid once rather than per program. The second half of the claim is that underconstrained constraint systems, the source of soundness bugs, escape such equality checks, so ARGUZZ additionally re-runs the product program with a fault injected into one executed instruction, letting the altered value ripple through normal data dependencies, and reports a soundness bug only when the program's output changes and the unmodified verifier still accepts the proof. The paper reports eleven previously unknown bugs across RISC Zero, Nexus, and Jolt: three soundness bugs, all found by fault injection (a missing constraint on three-register instructions in RISC Zero, an unconstrained store operand in Nexus, an unconstrained lui immediate in Jolt), and eight completeness bugs found by the metamorphic product programs, ranging from off-by-one cycle counts and memory-size miscalculations to sumcheck failures on rare instructions such as mulhsu.","pith_inferences":["The metamorphic rewrite rules are taken to preserve Rust semantics exactly, but at least one rule, rewriting the constant 1 into $r / r$, introduces a division-by-zero panic when $r = 0$; if any of the eight reported completeness crashes came from such a rewrite, it would be a false positive rather than a zkVM defect, and re-running with that rule disabled would settle it.","The product-program oracle is not tied to zkVMs: since the paper notes any technique producing programs with known outputs could replace it, the same merge-and-compare construction could be applied to other proof-producing stacks, such as zkEVMs, validity-rollup provers, or differential testing of RISC-V compilers.","The pattern behind the RISC Zero bug, a missing operand-binding constraint shared by every three-register instruction, suggests that zkVM constraint systems could be audited by enumerating instruction encodings by shape and probing each family for symmetric operand behavior, a check a fuzzer could automate directly.","The fact that fault injection, not metamorphic testing, found every soundness bug suggests the two techniques probe disjoint failure modes, and a testing budget should fund their combination rather than either alone."],"forward_implications":["Soundness bugs that escape metamorphic testing can be exposed by fault injection: all three soundness bugs ARGUZZ found were triggered by the instruction-modification injection, which simulates a malicious prover that the unmodified verifier then fails to catch.","Because the expected output of a product program is known in advance, completeness bugs show up as crashes or mismatches on the unmodified VM, and the paper reports eight such bugs across RISC Zero, Nexus, and Jolt, including an off-by-one cycle-counting error in RISC Zero.","The merged single-run design makes testing affordable on slow prover stacks: proving time is dominated by padded trace size, and bundling several equivalent functions pays the power-of-two padding once instead of once per function.","Inline assembly in generated circuits raises instruction coverage by roughly 15 to 45 percent across the six zkVMs and is directly responsible for at least one found bug, the Jolt mulhsu sumcheck failure.","Bug-refinding experiments show the approach is practical on modest hardware: all soundness bugs were rediscovered within hours on 4-CPU campaigns, two of the completeness bugs in under 20 minutes."],"supporting_citations":[{"why":"CIRCUZZ, the metamorphic-testing fuzzer for zero-knowledge pipelines whose CIRCIL language, rewrite rules, and oracle approach ARGUZZ ports to zkVMs.","marker":"[23]"},{"why":"The original metamorphic-testing formulation that provides the semantic-equivalence oracle used throughout.","marker":"[17]"},{"why":"Introduces product programs, the construction that lets ARGUZZ merge equivalent functions into one executable with a known output.","marker":"[12]"},{"why":"Foundational fault-injection methodology that ARGUZZ's malicious-prover mechanism extends to zkVM execution logic.","marker":"[7]"},{"why":"RISC Zero, the production zkVM where the $50,000 soundness bug, a missing constraint on three-register instructions, was found.","marker":"[5]"},{"why":"The Jolt design, SNARKs for VMs via lookups, whose constraint system contains the lui soundness bug and the five completeness bugs.","marker":"[8]"},{"why":"Nexus, the zkVM where the unconstrained store-operand soundness bug and two completeness bugs were found.","marker":"[3]"},{"why":"The Dory commitment scheme whose failure on traces under 256 cycles is Jolt bug 9, found by ARGUZZ's metamorphic programs.","marker":"[30]"}],"fun_headline_variants":["Arguzz finds 11 zkVM bugs, $50k bounty","First automated zkVM tester uncovers 11 bugs","zkVM bug hunt: 11 flaws, one $50k payout","Arguzz: new zkVM tool nets 11 bugs"],"cache_read_input_tokens":26240,"weakest_assumption_plain":"The load-bearing premise is that every metamorphic rewrite rule preserves the exact behavior of the Rust program on every input, so a crash or output mismatch in the merged product program can only be caused by the zkVM, yet the rule that rewrites the constant 1 into $r / r$ introduces a division-by-zero panic when $r = 0$, which would make a transformed program crash without any zkVM defect.","fun_headline_variants_meta":{"raw":{"variants":["Arguzz finds 11 zkVM bugs, $50k bounty","First automated zkVM tester uncovers 11 bugs","zkVM bug hunt: 11 flaws, one $50k payout","Arguzz: new zkVM tool nets 11 bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000587,"raw_usage":{"total_tokens":2811,"prompt_tokens":1055,"completion_tokens":1756,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":671,"completion_tokens_details":{"reasoning_tokens":1682}},"tokens_in":671,"tokens_out":1756,"duration_ms":10957,"temperature":1.0,"reasoning_tokens":1682,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T15:52:44.638055+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Re-run ARGUZZ's metamorphic campaigns with the $r / r$ rule (and any rule that introduces a fresh variable, such as add-sub-random-value) guarded by a nonzero condition on $r$ or disabled entirely, and check whether all eight reported completeness bugs still reproduce; any crash that disappears is attributable to the rewrite rule, not the zkVM. As a check on the soundness claims, apply each vendor's patch to the constraint system and confirm that the corresponding fault-injected proof, such as $7 \\bmod 5 = 0$ in RISC Zero, is then rejected by the unmodified verifier.","supporting_citations":[{"cited_title":"Fuzzing processing pipelines for zero-knowledge circuits","cited_arxiv_id":null,"evidence_quote":"CIRCUZZ, the metamorphic-testing fuzzer for zero-knowledge pipelines whose CIRCIL language, rewrite rules, and oracle approach ARGUZZ ports to zkVMs."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The original metamorphic-testing formulation that provides the semantic-equivalence oracle used throughout."},{"cited_title":"Relational verification using product programs","cited_arxiv_id":null,"evidence_quote":"Introduces product programs, the construction that lets ARGUZZ merge equivalent functions into one executable with a known output."},{"cited_title":"Fault injection for dependability validation: A methodology and some applications.TSE, 16:166–182, 1990","cited_arxiv_id":null,"evidence_quote":"Foundational fault-injection methodology that ARGUZZ's malicious-prover mechanism extends to zkVM execution logic."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"RISC Zero, the production zkVM where the $50,000 soundness bug, a missing constraint on three-register instructions, was found."},{"cited_title":"Jolt: SNARKs for virtual machines via lookups","cited_arxiv_id":null,"evidence_quote":"The Jolt design, SNARKs for VMs via lookups, whose constraint system contains the lui soundness bug and the five completeness bugs."},{"cited_title":"https://github.com/nexus-xyz/ nexus-zkvm","cited_arxiv_id":null,"evidence_quote":"Nexus, the zkVM where the unconstrained store-operand soundness bug and two completeness bugs were found."},{"cited_title":"Dory: Efficient, transparent arguments for generalised inner products and polynomial commit- ments.Cryptol","cited_arxiv_id":null,"evidence_quote":"The Dory commitment scheme whose failure on traces under 256 cycles is Jolt bug 9, found by ARGUZZ's metamorphic programs."}],"review_version":1}