Arguzz: Testing zkVMs for Soundness and Completeness Bugs

• URL: http://arxiv.org/abs/2509.10819v1
• Date: Sat, 13 Sep 2025 14:36:49 GMT
• Title: Arguzz: Testing zkVMs for Soundness and Completeness Bugs
• Abstract summary: We present Arguzz, the first automated tool for testing zkVMs for soundness and completeness bugs.<n>By injecting faults into the VM, Arguzz mimics malicious or buggy provers to uncover overly weak constraints.
• Score: 4.015374459538631
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Zero-knowledge virtual machines (zkVMs) are increasingly deployed in decentralized applications and blockchain rollups since they enable verifiable off-chain computation. These VMs execute general-purpose programs, frequently written in Rust, and produce succinct cryptographic proofs. However, zkVMs are complex, and bugs in their constraint systems or execution logic can cause critical soundness (accepting invalid executions) or completeness (rejecting valid ones) issues. We present Arguzz, the first automated tool for testing zkVMs for soundness and completeness bugs. To detect such bugs, Arguzz combines a novel variant of metamorphic testing with fault injection. In particular, it generates semantically equivalent program pairs, merges them into a single Rust program with a known output, and runs it inside a zkVM. By injecting faults into the VM, Arguzz mimics malicious or buggy provers to uncover overly weak constraints. We used Arguzz to test six real-world zkVMs (RISC Zero, Nexus, Jolt, SP1, OpenVM, and Pico) and found eleven bugs in three of them. One RISC Zero bug resulted in a $50,000 bounty, despite prior audits, demonstrating the critical need for systematic testing of zkVMs.

Related papers

• Efficient Branch-and-Bound Testing and Verification of zkVMs [26.60003840008197]
  We present ZEBRA, a fully automated verification and bug-detection framework.<n>ZEBRA reduces zkVM verification to a solution-set cardinality problem over a canonical trace space.<n>ZEBRA discovers 11 zero-day bugs; 6 have already been independently confirmed and 3 have been fixed by developers.
  arXiv  Detail & Related papers  (2026-09-14T04:35:11Z)
• Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection [3.6756416620917522]
  We present Liezz, a testing framework that generates ZK DSL programs and exposes bugs through adversarial witness injection.<n>For each generated deterministic program, Liezz executes two public input assignments with different outputs and splices their witnesses, combining the input of one execution with the output of the other.<n> Controlled divergence and multiple witness-splicing strategies preserve enough consistency to expose missing constraints.
  arXiv  Detail & Related papers  (2026-08-31T11:50:37Z)
• ViGoR-Bench: How Far Are Visual Generative Models From Zero-Shot Visual Reasoners? [48.43592287326448]
  ViGoR Vision-Gnerative Reasoning-centric Benchmark is a unified framework designed to dismantle this mirage.<n>ViGoR distinguishes itself through four key innovations: 1) holistic cross-modal coverage bridging Image-to-Image and Video tasks; 2) a dual-track mechanism evaluating both intermediate processes and final results; 3) an evidence-grounded automated judge ensuring high human alignment.<n> Experiments on over 20 leading models reveal that even state-of-the-art systems harbor significant reasoning deficits.
  arXiv  Detail & Related papers  (2026-03-26T18:40:09Z)
• Agentic Harness for Real-World Compilers [22.07908620753322]
  We introduce the agentic harness designed to assist large compiler agents in understanding and fixing compiler bugs.<n>Our focus is on LLVM, one of the most widely used compiler infrastructures. Central to-autofix are agent-friendly LLVM tools, and a tailored minimal agent-autofix-mini for fixing LLVM bugs.
  arXiv  Detail & Related papers  (2026-03-20T15:56:43Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBench is an evaluation framework for self-evolving benchmarks that scrapes and evaluates agents on freshly discovered kernel bugs.<n> kEnv is an agent-agnostic crash-resolution environment for kernel compilation, execution, and feedback.<n>Using kEnv, we benchmark three state-of-the-art agents, showing that they resolve 74% of crashes on the first attempt.
  arXiv  Detail & Related papers  (2026-02-02T19:06:15Z)
• AICD Bench: A Challenging Benchmark for AI-Generated Code Detection [91.21422299346199]
  AICD Bench is the most comprehensive benchmark for AI-generated code detection.<n>It spans $emph2M examples$, $emph77 models$ across $emph11 families$, and $emph9 programming languages$, including recent reasoning models.
  arXiv  Detail & Related papers  (2026-02-02T13:24:14Z)
• EVM-QuestBench: An Execution-Grounded Benchmark for Natural-Language Transaction Code Generation [9.472124187479915]
  In on-chain transaction scenarios, even a minor error can cause irreversible loss for users.<n>We introduce EVM-QuestBench, an execution-grounded benchmark for natural-language transaction-script generation.<n>We evaluate 20 models and find large performance gaps, with split scores revealing persistent asymmetry between single-action precision and multi-step workflow completion.
  arXiv  Detail & Related papers  (2026-01-10T13:25:27Z)
• ZeroOS: A Universal Modular Library OS for zkVMs [14.822170571629252]
  zkVMs promise general-purpose verifiable computation through ISA-level compatibility with modern programs and toolchains.<n>Modern programs often cannot run or even compile without an operating system and libc.
  arXiv  Detail & Related papers  (2025-12-10T04:00:40Z)
• How Many Code and Test Cases Are Enough? Evaluating Test Cases Generation from a Binary-Matrix Perspective [51.30005925128432]
  evaluating test cases automatically generated by Large Language Models (LLMs) is a critical yet challenging task.<n>Existing benchmarks suffer from high computational costs, score inflation, and a bias towards trivial bugs over rare, critical faults.<n>We introduce a framework that formalizes benchmark construction as finding an optimal diagnostic basis in a binary code-test matrix.
  arXiv  Detail & Related papers  (2025-10-09T18:29:24Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [57.476483009565044]
  $rm Csmall LEVER$ is a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean.<n>Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification.
  arXiv  Detail & Related papers  (2025-05-20T05:15:47Z)
• Eliminating Hallucination-Induced Errors in LLM Code Generation with Functional Clustering [0.0]
  We present functional clustering, a black-box wrapper that eliminates nearly all hallucination-induced errors while providing a tunable confidence score.<n>Our verifier preserves baseline pass@1 on solvable tasks yet slashes the error rate of returned answers from 65% to 2%.<n>Because the method requires only sampling and sandbox execution, it applies unchanged to closed-source APIs and future models.
  arXiv  Detail & Related papers  (2025-05-16T18:19:38Z)
• CrashFixer: A crash resolution agent for the Linux kernel [58.152358195983155]
  This work builds upon kGym, which shares a benchmark for system-level Linux kernel bugs and a platform to run experiments on the Linux kernel.<n>This paper introduces CrashFixer, the first LLM-based software repair agent that is applicable to Linux kernel bugs.
  arXiv  Detail & Related papers  (2025-04-29T04:18:51Z)
• KGym: A Platform and Dataset to Benchmark Large Language Models on Linux Kernel Crash Resolution [59.20933707301566]
  Large Language Models (LLMs) are consistently improving at increasingly realistic software engineering (SE) tasks. In real-world software stacks, significant SE effort is spent developing foundational system software like the Linux kernel. To evaluate if ML models are useful while developing such large-scale systems-level software, we introduce kGym and kBench.
  arXiv  Detail & Related papers  (2024-07-02T21:44:22Z)
• Heckler: Breaking Confidential VMs with Malicious Interrupts [2.650561978417805]
  Heckler is a new attack wherein the hypervisor injects malicious non-timer interrupts to break the confidentiality and integrity of CVMs. With AMD SEV-SNP and Intel TDX, we demonstrate Heckler on OpenSSH and to bypass authentication.
  arXiv  Detail & Related papers  (2024-04-04T11:37:59Z)
• IRFuzzer: Specialized Fuzzing for LLVM Backend Code Generation [3.4764546186868452]
  We implement IRFuzzer to investigate the effectiveness of specialized fuzzing of the LLVM compiler backend.<n>The mutator in IRFuzzer is capable of generating a wide range of LLVM IR inputs, including structured control flow, vector types, and function definitions.<n>We show that IRFuzzer is more effective than existing fuzzers by fuzzing on 29 mature LLVM backend targets.
  arXiv  Detail & Related papers  (2024-02-07T21:02:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.