SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients

• URL: http://arxiv.org/abs/2608.17738v1
• Date: Tue, 18 Aug 2026 13:03:22 GMT
• Title: SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients
• Abstract summary: We introduce Consensus-SpecTec, a mechanized specification of the consensus algorithm.<n>We also present SpecTrum, a framework that addresses this problem in three stages.<n>We identify 27 cross-client divergence cases, 22 of which cannot be found without premises inserted in our mechanization.
• Score: 3.016888279148097
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ethereum's consensus safety relies on independent consensus client implementations agreeing on every state transition. When they diverge due to implementation errors, the network can fork, finality can stall, and severe attacks are possible. To prevent such consensus divergences, Ethereum provides a Python reference implementation (consensus-spec), which acts as a specification, and a hand-crafted official test suite (spectests). However, as an executable implementation, Ethereum's specification defines validity implicitly through runtime behavior. As a result, it lacks a systematic way to ensure that all validity conditions are thoroughly evaluated. We present SpecTrum, a framework that addresses this problem in three stages. First, we introduce Consensus-SpecTec, a mechanized specification of the Ethereum consensus algorithm, which makes validity conditions explicit as if-premises. Second, we define premise coverage, a metric that measures which if-premises are evaluated to true and false across spectests. Third, we develop a specification-based test generator that extracts constraints on premises not evaluated to false by spectests and generates inputs to evaluate them. Applying SpecTrum to five major Ethereum consensus clients, we identify 27 cross-client divergence cases, 22 of which cannot be found without the premises inserted in our mechanization. All 27 cases reproduce across fork versions, and extending the mechanized specification to a new fork takes modest effort proportional to the specification difference.

Related papers

• ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
  Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification.<n>We present proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model.
  arXiv  Detail & Related papers  (2026-08-31T14:00:31Z)
• SpecPath: Testing Coding Agents Across Contract-Equivalent Specification Histories [13.437222222971272]
  We identify specification-path sensitivity, a failure mode in which requirement histories that are equivalent in their final meaning lead the same agent system to produce behaviorally different programs.<n>We introduce SpecPath, a diagnostic evaluation that holds the repository, final contract, verifier, agent system, and execution budget fixed while changing only the revision path that leads to the contract.
  arXiv  Detail & Related papers  (2026-08-10T16:19:00Z)
• Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
  Coding agents often over-trust their own local validation routines and declare success on artifacts that satisfy surface checks.<n>This problem is especially acute in conversion, where prior evaluation is outcome-driven.<n>Across blind conversion attempts, the best system reaches 26.7--28.9% overall pass rate despite Spec pass rates up to 91.1%.<n>This suggests that failures stem more from contract-misaligned self-validation than from limited budget or backbone strength.
  arXiv  Detail & Related papers  (2026-05-27T19:57: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)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol.<n>CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions.<n>We observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate.
  arXiv  Detail & Related papers  (2026-04-14T04:31:45Z)
• When Specifications Meet Reality: Uncovering API Inconsistencies in Ethereum Infrastructure [16.114947403968326]
  APIDiffer is the first specification-guided differential testing framework.<n>It transforms API specifications into comprehensive test suites.<n>APIDiffer uncovered 72 bugs, with 90.28% already confirmed or fixed by developers.
  arXiv  Detail & Related papers  (2026-03-06T08:28:44Z)
• Proof of Trusted Execution: A Consensus Paradigm for Deterministic Blockchain Finality [0.391985484065646]
  We propose Proof of Trusted Execution (PoTE), a consensus paradigm where agreement emerges from verifiable execution rather than replicated re-execution.<n>Because the execution is deterministic and the proposer is uniquely derived from public randomness, PoTE avoids forks, eliminates slot.time bottlenecks, and commits blocks in a single round of verification.
  arXiv  Detail & Related papers  (2025-12-10T08:04:38Z)
• SConU: Selective Conformal Uncertainty in Large Language Models [59.25881667640868]
  We propose a novel approach termed Selective Conformal Uncertainty (SConU)<n>We develop two conformal p-values that are instrumental in determining whether a given sample deviates from the uncertainty distribution of the calibration set at a specific manageable risk level.<n>Our approach not only facilitates rigorous management of miscoverage rates across both single-domain and interdisciplinary contexts, but also enhances the efficiency of predictions.
  arXiv  Detail & Related papers  (2025-04-19T03:01:45Z)
• Conformal Prediction Sets with Improved Conditional Coverage using Trust Scores [52.92618442300405]
  It is impossible to achieve exact, distribution-free conditional coverage in finite samples.<n>We propose an alternative conformal prediction algorithm that targets coverage where it matters most.
  arXiv  Detail & Related papers  (2025-01-17T12:01:56Z)
• Short Paper: Accountable Safety Implies Finality [10.589723476970443]
  Two key desiderata have been studied for Byzantine-fault tolerant (BFT) state-machine replication (SMR) consensus protocols. We show that accountable safety implies finality, thereby unifying earlier results.
  arXiv  Detail & Related papers  (2023-08-31T17:58:38Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)

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.