Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection

• URL: http://arxiv.org/abs/2608.30648v1
• Date: Mon, 31 Aug 2026 11:50:37 GMT
• Title: Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection
• Abstract summary: 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.
• Score: 3.6756416620917522
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Zero-knowledge domain-specific language (ZK DSL) toolchains compile programs into constraint systems and generate witnesses for cryptographic proofs. Bugs in these toolchains can leave the enforced constraints weaker than the source-program semantics, admitting proofs for invalid executions. Such soundness bugs may remain invisible to valid-execution testing because all valid executions still behave correctly. We present Liezz, a testing framework that generates ZK DSL programs and exposes these bugs through adversarial witness injection. 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. The resulting witness is invalid by construction. A correct toolchain must reject it; acceptance exposes a soundness bug. Controlled divergence and multiple witness-splicing strategies preserve enough consistency to expose missing constraints. Liezz also generates parameterized standard-library calls to reach complex functionality. Liezz supports Circom, Corset, Gnark, and Noir. It finds 13 bugs, including seven with soundness impact. Several are reachable only through generated standard-library calls. Under the same testing budget, a valid-execution baseline does not expose any of the soundness failures revealed by accepted injected witnesses, showing that adversarial witness injection reaches failures missed by valid-execution testing.

Related papers

• RosettaBitcoin: An Artifact-Backed Experience Report on Verification Infrastructure for Agent-Assisted Consensus Validators [0.0]
  This experience report studies RosettaBitcoin, a single-developer project that built twelve separately implemented Bitcoin testnet4 consensus validators.<n>We analyze the snapshot's tracked evidence database, curated artifact index, canonical conformance fixtures, validation scripts, blocker records, and version history.<n>The case suggests that explicit failure records, fixtures, port-owned, and validating imports can make agent-assisted systems more auditable.
  arXiv  Detail & Related papers  (2026-09-01T17:22:07Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• TTHE: Test-Time Harness Evolution [50.26245555541721]
  Existing approaches optimize such harnesses before deployment, searching training or development data for a fixed agent workflow that is then frozen at test time.<n>We ask whether the harness can instead be optimized during evaluation itself, using only the unlabeled execution traces the agent produces on the test inputs.<n>During evaluation, TTHE maintains a population of candidate harnesses and refines them through an agentic proposer that reasons over their execution traces.<n>A judge then commits an improved harness from execution-derived proxy signals, and the selected program persists to govern subsequent inputs.
  arXiv  Detail & Related papers  (2026-07-09T05:53:39Z)
• A Minimal Executable Proof for Multi-Language Contract Traceability [0.0]
  This paper reports a deliberately small executable proof for a DAG-TOML contract.<n>It shows how a contract, implementation graph, traceability chain, and review gate can be checked against executable witnesses.
  arXiv  Detail & Related papers  (2026-05-27T14:37:26Z)
• CIVeX: Causal Intervention Verification for Language Agents [0.0]
  We introduce CIVeX, a causal intervention verifier that maps proposed actions to structural causal queries over a committed action-state graph.<n>On Causal-ToolBench (1,890 instances, 7 seeds), CIVeX yields zero observed false executions across moderate and adversarial confounding.<n>On IHDP and ZOZO Open Bandit (real production logs with uniform-random ground truth), CIVeX matches Oracle correct-execution within 0.1pp and cuts per-execute false-execution by >=50x over naive baselines.
  arXiv  Detail & Related papers  (2026-05-09T21:06:15Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
  arXiv  Detail & Related papers  (2026-04-29T09:57:07Z)
• AnyPoC: Universal Proof-of-Concept Test Generation for Scalable LLM-Based Bug Detection [21.99631570872796]
  We present AnyPoC, a general multi-agent framework that analyzes and fact-checks a candidate bug report.<n>AnyPoC produces 1.3x more valid PoCs for true-positive bug reports and rejects 9.8x more false-positive bug reports.<n>To date, AnyPoC has discovered 122 new bugs (105 confirmed, 86 already fixed), with 45 generated PoCs adopted as official regression tests.
  arXiv  Detail & Related papers  (2026-04-13T18:44:02Z)
• DuET: Dual Execution for Test Output Prediction with Generated Code and Pseudocode [56.14374797825548]
  We introduce LLM-based pseudocode execution, which grounds prediction on more error-resilient pseudocode.<n>We propose DuET, a dual-execution framework that combines both approaches by functional majority voting.<n>On LiveCodeBench, DuET achieves the state-of-the-art performance, improving Pass@1 by 13.6 pp.
  arXiv  Detail & Related papers  (2026-04-13T14:18:58Z)
• Scaling Agentic Verifier for Competitive Coding [66.11758166379092]
  Large language models (LLMs) have demonstrated strong coding capabilities but still struggle to solve competitive programming problems correctly in a single attempt.<n>Execution-based re-ranking offers a promising test-time scaling strategy, yet existing methods are constrained by either difficult test case generation or inefficient random input sampling.<n>We propose Agentic Verifier, an execution-based agent that actively reasons about program behaviors and searches for highly discriminative test inputs.
  arXiv  Detail & Related papers  (2026-02-04T06:30:40Z)
• Arguzz: Testing zkVMs for Soundness and Completeness Bugs [4.015374459538631]
  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.
  arXiv  Detail & Related papers  (2025-09-13T14:36:49Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $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)
• GPT-HateCheck: Can LLMs Write Better Functional Tests for Hate Speech Detection? [50.53312866647302]
  HateCheck is a suite for testing fine-grained model functionalities on synthesized data. We propose GPT-HateCheck, a framework to generate more diverse and realistic functional tests from scratch. Crowd-sourced annotation demonstrates that the generated test cases are of high quality.
  arXiv  Detail & Related papers  (2024-02-23T10:02:01Z)

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.