一句话：提出机械化规范与前提覆盖度量，引导生成测试，发现以太坊共识客户端的 27 例跨实现分歧。
以太坊共识安全依赖多个独立共识客户端在每个状态转换上保持一致；实现错误会导致分叉、终局性停滞乃至严重攻击。以太坊虽提供 Python 参考实现（consensus-spec）与官方测试集（spectests），但作为可执行实现，其有效性条件隐含在运行时行为中，缺乏系统性手段保证所有有效性条件都被充分求值。本文提出 SpecTrum 框架，分三步解决该问题：首先给出 Consensus-SpecTec——以太坊共识算法的机械化规范，将有效性条件显式表示为 if 前提；其次定义前提覆盖（premise coverage），度量 spectests 中各前提被求值为真和假的情况；最后实现基于规范的测试生成器，提取未被 spectests 覆盖为假的前提约束并生成输入以触发它们。作者将 SpecTrum 应用于五个主流以太坊共识客户端，发现 27 个跨客户端分歧，其中 22 个若没有机械化规范中插入的前提便无法发现；全部 27 例可在各 fork 版本复现，且将机械化规范扩展到新 fork 的工作量与规范差异成正比。
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.
@inproceedings{paperbot12411,
title = {SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients},
author = {Seokhun Jeong and Gyeongmin Dan and Sukyoung Ryu and Sungjae Hwang},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834406}
}