Pith. sign in

REVIEW 2 major objections 4 minor 1 cited by

Arguzz: Testing zkVMs for Soundness and Completeness Bugs

T0 review · 2 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2509.10819 v1 pith:EDDZZXG4 submitted 2025-09-13 cs.SE cs.CRcs.PL

Christoph Hochrainer , Valentin Wüstholz , Maria Christakis This is my paper · ORCID
classification cs.SEcs.CRcs.PL
keywords zero-knowledgevirtualmachinesmetamorphictestingproductprogramsfaultinjectionsoundnessbugscompletenesszkVMfuzzingRISC-V
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 4 minor

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.

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 (2)
  1. [Appendix A, Step 6] 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.
  2. [§4.1, Experiments in the wild] 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.
minor comments (4)
  1. [Figure 15] The instruction label 'eany' appears in the top plot; this is likely a typographical error for 'ecall' and should be corrected.
  2. [§4.2, RQ6] 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.
  3. [Step 3, §3.1] 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.
  4. [§5, Related Work] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: ARGUZZ's bug findings are externally confirmed and its rewrite rules are enumerated and checkable; the one-div rule is a correctness risk, not a circular derivation.

full rationale

ARGUZZ does not derive its bug findings from a fitted parameter or from a self-citation chain. The metamorphic oracle is generated by applying rewrite rules listed in Appendix A, most of which are ordinary algebraic identities; the product program encodes the comparison internally, and the claimed 'known expected output' (SUCCESS) is simply the equality of the original and transformed functions. The central empirical contribution, eleven bugs in RISC Zero, Nexus, and Jolt, was externally confirmed: RISC Zero awarded a $50,000 bounty and developers issued fixes, and the bug-refinding experiment checks that applying the fixes removes the bugs. That makes the results externally falsifiable rather than circular. The one substantive concern is that the paper asserts the Appendix A transformations are semantics-preserving without proving it, and at least one rule is not: 'one-div' rewrites 1 to $r / $r, which panics under Rust semantics when $r = 0, while Step 6 classifies any product-program crash as a completeness bug. Similarly, 'and-to-rem' and 'rem-to-and' are not equivalent for signed Rust integers. This is a real correctness risk in the oracle and could cause false completeness-bug reports, but it is not a circular derivation: the reported bugs were acknowledged and fixed by the respective developers, and none is shown to be caused by these specific rules. The self-citation to CIRCUZZ supplies the transformation framework, but the rules are enumerated in the paper and are independently checkable, so the citation is not load-bearing in the sense of an unverified unique theorem. No fitted input is renamed as a prediction, and no known result is repackaged under new coordinates. Accordingly, the circularity score is 1.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper is an empirical tool evaluation, not a mathematical derivation. No fitted parameters or invented physical entities are used. The load-bearing assumptions are the correctness of the metamorphic oracle, the zkVM threat model, and the representativeness of the tested systems.

assumptions (3)
  • ad hoc to paper Each metamorphic rewrite rule in Appendix A preserves Rust program semantics inside the zkVM.
    Load-bearing for the oracle. Rule 'one-div' (1 -> $r/$r) is not valid when $r = 0 because Rust panics on division by zero, which could create false completeness-bug reports.
  • domain assumption The unmodified verifier is the trusted component; fault injection into the prover that yields a verified OOPS output implies a soundness bug.
    This is the standard zkVM threat model and the basis for classifying the three soundness bugs.
  • domain assumption The six selected zkVMs are representative and their main branches at the time of testing contained the buggy behavior, with vendor confirmation of each report.
    The evaluation generalization depends on the six VMs being representative and on vendor confirmation of each report.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Arguzz: Testing zkVMs for Soundness and Completeness Bugs." pith.science (2026). https://pith.science/paper/EDDZZXG4

@misc{pith2026250910819,
  author       = {Pith},
  title        = {Pith review of: Arguzz: Testing zkVMs for Soundness and Completeness Bugs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EDDZZXG4}},
  note         = {Machine review of arXiv:2509.10819}
}
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.

Figures

Figures reproduced from arXiv: 2509.10819 by the authors.

Figure 1
Figure 1. Overview of typical zkVM stages. and may even lead to liveness issues. Additionally, in some cases, the constraints may simply be wrong, that is, they may misrepresent the intended semantics of the VM. Such mis￾matches can lead to both soundness and completeness issues, depending on whether they allow invalid executions or reject valid ones. Both types of bugs have serious consequences. Soundness bugs can lead to fr… view at source ↗
Figure 2
Figure 2. Overview of ARGUZZ. verifier is the final stage that checks the proof (see [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Example CIRCIL circuits and Rust functions generated by ARGUZZ. outputs, and line 3 computes the value of the output using a basic arithmetic expression. Step 2: Circuit transformation. We use a similar set of semantics-preserving transformations as CIRCUZZ [23]. These include transformations based on algebraic identities, such as commutativity, associativity, distributivity, and De Morgan’s laws. They apply to logi… view at source ↗
Figures from the paper (17 more)
Figure 5
Figure 5. Figure 5: Part of product program in Rust generated from [PITH_FULL_IMAGE:figures/full_fig_p005_5.png]
Figure 4
Figure 4. Figure 4: Product program in Rust generated by ARGUZZ using the functions of Figs. 3c and 3d. of remu in a fault-injected run, increasing the chances of exposing soundness bugs related to that specific operation. Step 7: VM execution with malicious prover. Finally, we re-run the…
Figure 6
Figure 6. Figure 6: Example CIRCIL circuit and Rust function gen￾erated by ARGUZZ using the inline-assembly extension. 3.2 Product-Program Generation Our fault-injection mechanism requires programs with known outputs to reliably detect soundness bugs. However, gener￾ating programs of conf…
Figure 7
Figure 7. Figure 7: Generic instruction-modification injection per [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]
Figure 8
Figure 8. Figure 8: Distribution of injection frequencies across instructions for each zkVM, comparing [PITH_FULL_IMAGE:figures/full_fig_p012_8.png]
Figure 9
Figure 9. Figure 9: Execution time versus product-program size for RISC Z [PITH_FULL_IMAGE:figures/full_fig_p019_9.png]
Figure 10
Figure 10. Figure 10: Execution time versus product-program size for N [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Execution time versus product-program size for J [PITH_FULL_IMAGE:figures/full_fig_p020_11.png]
Figure 12
Figure 12. Figure 12: Execution time versus product-program size for SP1. [PITH_FULL_IMAGE:figures/full_fig_p021_12.png]
Figure 13
Figure 13. Figure 13: Execution time versus product-program size for O [PITH_FULL_IMAGE:figures/full_fig_p021_13.png]
Figure 14
Figure 14. Figure 14: Execution time versus product-program size for P [PITH_FULL_IMAGE:figures/full_fig_p022_14.png]
Figure 15
Figure 15. Figure 15: Instruction-frequency distributions in binaries generated from [PITH_FULL_IMAGE:figures/full_fig_p023_15.png]
Figure 16
Figure 16. Figure 16: Instruction-frequency distributions in binaries generated from [PITH_FULL_IMAGE:figures/full_fig_p024_16.png]
Figure 17
Figure 17. Figure 17: Instruction-frequency distributions in binaries generated from [PITH_FULL_IMAGE:figures/full_fig_p025_17.png]
Figure 18
Figure 18. Figure 18: Instruction-frequency distributions in binaries generated from [PITH_FULL_IMAGE:figures/full_fig_p026_18.png]
Figure 19
Figure 19. Figure 19: Instruction-frequency distributions in binaries generated from [PITH_FULL_IMAGE:figures/full_fig_p027_19.png]
Figure 20
Figure 20. Figure 20: Instruction-frequency distributions in binaries generated from [PITH_FULL_IMAGE:figures/full_fig_p028_20.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

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

    cs.CR 2026-07 accept novelty 6.5 of 10

    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.

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages · cited by 1 Pith paper

  1. [1]

    https://docs.gnark

    gnark: A fast zk-SNARK library that offers a high- level API to design circuits. https://docs.gnark. consensys.io

    work page

  2. [2]

    Jolt.https://github.com/a16z/jolt

    work page

  3. [3]

    https://github.com/nexus-xyz/ nexus-zkvm

    Nexus. https://github.com/nexus-xyz/ nexus-zkvm

    work page

  4. [4]

    Noir.https://noir-lang.org

    work page

  5. [5]

    RISC Zero.https://github.com/risc0/risc0

    work page

  6. [6]

    Mining API error- handling specifications from source code

    Mithun Acharya and Tao Xie. Mining API error- handling specifications from source code. InFASE, volume 5503 ofLNCS, pages 370–384. Springer, 2009

    work page 2009

  7. [7]

    Fault injection for dependability validation: A methodology and some applications.TSE, 16:166–182, 1990

    Jean Arlat, Martine Aguera, Louis Amat, Yves Crouzet, Jean-Charles Fabre, Jean-Claude Laprie, Eliane Martins, and David Powell. Fault injection for dependability validation: A methodology and some applications.TSE, 16:166–182, 1990

    work page 1990

  8. [8]

    Jolt: SNARKs for virtual machines via lookups

    Arasu Arun, Srinath Setty, and Justin Thaler. Jolt: SNARKs for virtual machines via lookups. Cryptol- ogy ePrint Archive, Paper 2023/1217, 2023. https: //eprint.iacr.org/2023/1217

    work page 2023

Show all 47 references
  1. [9]

    Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo

    Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. The oracle problem in software testing: A survey.TSE, 41:507–525, 2015

    2015

  2. [10]

    Fuzztruction: Using fault injection-based fuzzing to leverage implicit domain knowledge

    Nils Bars, Moritz Schloegel, Tobias Scharnowski, Nico Schiller, and Thorsten Holz. Fuzztruction: Using fault injection-based fuzzing to leverage implicit domain knowledge. InSecurity, pages 1847–1864. USENIX, 2023

    2023

  3. [11]

    No peer, no cry: Network application fuzzing via fault injection

    Nils Bars, Moritz Schloegel, Nico Schiller, Lukas Bern- hard, and Thorsten Holz. No peer, no cry: Network application fuzzing via fault injection. InCCS, pages 750–764. ACM, 2024

    2024

  4. [12]

    Relational verification using product programs

    Gilles Barthe, Juan Manuel Crespo, and César Kunz. Relational verification using product programs. InFM, volume 6664 ofLNCS, pages 200–214. Springer, 2011

    2011

  5. [13]

    D’Argenio, and Tamara Rezk

    Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. Secure information flow by self-composition. InCSFW, pages 100–114. IEEE Computer Society, 2004

    2004

  6. [14]

    Cir- com: A circuit description language for building zero- knowledge applications.Trans

    Marta Bellés-Muñoz, Miguel Isabel, Jose Luis Muñoz- Tapia, Albert Rubio, and Jordi Baylina Melé. Cir- com: A circuit description language for building zero- knowledge applications.Trans. Dependable Secur. Com- put., 20:4733–4751, 2023

    2023

  7. [15]

    Clarke, and Yunshan Zhu

    Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. InTACAS, volume 1579 ofLNCS, pages 193–

  8. [16]

    A survey of compiler testing.Comput

    Junjie Chen, Jibesh Patra, Michael Pradel, Yingfei Xiong, Hongyu Zhang, Dan Hao, and Lu Zhang. A survey of compiler testing.Comput. Surv., 53:4:1–4:36, 2020

    2020

  9. [17]

    Tsong Yueh Chen, S. C. Cheung, and Siu-Ming Yiu. Metamorphic testing: A new approach for generating next test cases. Technical Report HKUST–CS98–01, HKUST, 1998

    1998

  10. [18]

    A general framework for dy- namic stub injection

    Maria Christakis, Patrick Emmisberger, Patrice Gode- froid, and Peter Müller. A general framework for dy- namic stub injection. InICSE, pages 586–596. IEEE Computer Society/ACM, 2017

    2017

  11. [19]

    Clark and Dhiraj K

    Jeffrey A. Clark and Dhiraj K. Pradhan. Fault injection: A method for validating computer-system dependability. Computer, 28:47–56, 1995

    1995

  12. [20]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. Hyperprop- erties. InCSF, pages 51–65. IEEE Computer Society, 2008

    2008

  13. [21]

    Abstract interpreta- tion: A unified lattice model for static analysis of pro- grams by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpreta- tion: A unified lattice model for static analysis of pro- grams by construction or approximation of fixpoints. In POPL, pages 238–252. ACM, 1977

    1977

  14. [22]

    Finding and under- standing defects in static analyzers by constructing au- tomated oracles.PACMSE, 1:1656–1678, 2024

    Weigang He, Peng Di, Mengli Ming, Chengyu Zhang, Ting Su, Shijie Li, and Yulei Sui. Finding and under- standing defects in static analyzers by constructing au- tomated oracles.PACMSE, 1:1656–1678, 2024

    2024

  15. [23]

    Fuzzing processing pipelines for zero-knowledge circuits

    Christoph Hochrainer, Anastasia Isychev, Valentin Wüstholz, and Maria Christakis. Fuzzing processing pipelines for zero-knowledge circuits. InCCS. ACM,

  16. [24]

    Tsai, and Ravishankar K

    Mei-Chen Hsueh, Timothy K. Tsai, and Ravishankar K. Iyer. Fault injection techniques and tools.Computer, 30:75–82, 1997

    1997

  17. [25]

    DifuzzRTL: Dif- ferential fuzz testing to find CPU bugs

    Jaewon Hur, Suhwan Song, Dongup Kwon, Eunjin Baek, Jangwoo Kim, and Byoungyoung Lee. DifuzzRTL: Dif- ferential fuzz testing to find CPU bugs. InS&P, pages 1286–1303. IEEE Computer Society, 2021

    2021

  18. [26]

    Automatically detecting error handling bugs us- ing error specifications

    Suman Jana, Yuan Kang, Samuel Roth, and Baishakhi Ray. Automatically detecting error handling bugs us- ing error specifications. InSecurity, pages 345–362. USENIX, 2016. 29

    2016

  19. [27]

    Fuzzing error handling code using context-sensitive software fault injection

    Zu-Ming Jiang, Jia-Ju Bai, Kangjie Lu, and Shi-Min Hu. Fuzzing error handling code using context-sensitive software fault injection. InSecurity, pages 2595–2612. USENIX, 2020

    2020

  20. [28]

    Interrogation testing of program analyzers for soundness and precision issues

    David Kaindlstorfer, Anastasia Isychev, Valentin Wüstholz, and Maria Christakis. Interrogation testing of program analyzers for soundness and precision issues. InASE, pages 319–330. ACM, 2024

    2024

  21. [29]

    TheHuzz: Instruction fuzzing of processors using golden-reference models for finding software-exploitable vulnerabilities

    Rahul Kande, Addison Crump, Garrett Persyn, Patrick Jauernig, Ahmad-Reza Sadeghi, Aakash Tyagi, and Jeyavijayan Rajendran. TheHuzz: Instruction fuzzing of processors using golden-reference models for finding software-exploitable vulnerabilities. InSecurity, pages 3219–3236. US...

    2022

  22. [30]

    Dory: Efficient, transparent arguments for generalised inner products and polynomial commit- ments.Cryptol

    Jonathan Lee. Dory: Efficient, transparent arguments for generalised inner products and polynomial commit- ments.Cryptol. ePrint Arch., page 1274, 2020

    2020

  23. [31]

    IFIZZ: Deep-state and efficient fault-scenario generation to test IoT firmware

    Peiyu Liu, Shouling Ji, Xuhong Zhang, Qinming Dai, Kangjie Lu, Lirong Fu, Wenzhi Chen, Peng Cheng, Wen- hai Wang, and Raheem Beyah. IFIZZ: Deep-state and efficient fault-scenario generation to test IoT firmware. InASE, pages 805–816. IEEE Computer Society, 2021

    2021

  24. [32]

    Metamorphic testing of Datalog engines

    Muhammad Numair Mansur, Maria Christakis, and Valentin Wüstholz. Metamorphic testing of Datalog engines. InESEC/FSE, pages 639–650. ACM, 2021

    2021

  25. [33]

    Detecting critical bugs in SMT solvers using blackbox mutational fuzzing

    Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz, and Fuyuan Zhang. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In ESEC/FSE, pages 701–712. ACM, 2020

    2020

  26. [34]

    Dependency-aware metamorphic test- ing of Datalog engines

    Muhammad Numair Mansur, Valentin Wüstholz, and Maria Christakis. Dependency-aware metamorphic test- ing of Datalog engines. InISSTA, pages 236–247. ACM, 2023

    2023

  27. [35]

    LFI: A prac- tical and general library-level fault injector

    Paul Dan Marinescu and George Candea. LFI: A prac- tical and general library-level fault injector. InDSN, pages 379–388. IEEE Computer Society, 2009

    2009

  28. [36]

    McMillan

    Kenneth L. McMillan. Interpolation and model check- ing. InHandbook of Model Checking, pages 421–446. Springer, 2018

    2018

  29. [37]

    ECSTATIC: An extensible framework for testing and debugging configurable static analysis

    Austin Mordahl, Zenong Zhang, Dakota Soles, and Shiyi Wei. ECSTATIC: An extensible framework for testing and debugging configurable static analysis. InICSE, pages 550–562. IEEE Computer Society, 2023

    2023

  30. [38]

    Sánchez, and Antonio Ruiz Cortés

    Sergio Segura, Gordon Fraser, Ana B. Sánchez, and Antonio Ruiz Cortés. A survey on metamorphic testing. TSE, 42:805–824, 2016

    2016

  31. [39]

    Fuzzing API error handling behaviors using coverage guided fault injec- tion

    Shashank Sharma, Sai Ritvik Tanksalkar, Sourag Cheru- pattamoolayil, and Aravind Machiry. Fuzzing API error handling behaviors using coverage guided fault injec- tion. InAsiaCCS. ACM, 2024

    2024

  32. [40]

    Cascade: CPU fuzzing via intricate program generation

    Flavien Solt, Katharina Ceesay-Seitz, and Kaveh Razavi. Cascade: CPU fuzzing via intricate program generation. InSecurity. USENIX, 2024

    2024

  33. [41]

    Secure information flow as a safety problem

    Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. InSAS, volume 3672 ofLNCS, pages 352–367. Springer, 2005

    2005

  34. [42]

    Validating SMT solvers via semantic fusion

    Dominik Winterer, Chengyu Zhang, and Zhendong Su. Validating SMT solvers via semantic fusion. InPLDI, pages 718–730. ACM, 2020

    2020

  35. [43]

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

    Dongwei Xiao, Zhibo Liu, Yiteng Peng, and Shuai Wang. MTZK: Testing and exploring bugs in zero-knowledge (ZK) compilers. InNDSS. The Internet Society, 2025

    2025

  36. [44]

    MorFuzz: Fuzzing processor via runtime instruction morphing enhanced synchronizable co-simulation

    Jinyan Xu, Yiyuan Liu, Sirui He, Haoran Lin, Yajin Zhou, and Cong Wang. MorFuzz: Fuzzing processor via runtime instruction morphing enhanced synchronizable co-simulation. InSecurity, pages 1307–1324. USENIX, 2023

    2023

  37. [45]

    Finding and understand- ing bugs in software model checkers

    Chengyu Zhang, Ting Su, Yichen Yan, Fuyuan Zhang, Geguang Pu, and Zhendong Su. Finding and understand- ing bugs in software model checkers. InESEC/FSE, pages 763–773. ACM, 2019

    2019

  38. [46]

    Statfier: Automated testing of static analyzers via semantic-preserving program transformations

    Huaien Zhang, Yu Pei, Junjie Chen, and Shin Hwei Tan. Statfier: Automated testing of static analyzers via semantic-preserving program transformations. InES- EC/FSE, pages 237–249. ACM, 2023

    2023

  39. [47]

    Understanding and detecting annotation-induced faults of static analyzers.PACMSE, 1:722–744, 2024

    Huaien Zhang, Yu Pei, Shuyun Liang, and Shin Hwei Tan. Understanding and detecting annotation-induced faults of static analyzers.PACMSE, 1:722–744, 2024. 30

    2024

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.