Technical Report: Exploring Automatic Model-Checking of the Ethereum specification

TL;DR

This paper explores automated model-checking of the Ethereum 3SF consensus protocol's Accountable Safety property using TLA+, SMT, and Alloy, demonstrating feasibility for small instances and emphasizing manual abstraction's role.

Contribution

It introduces a formalization and verification approach for Ethereum's 3SF protocol, highlighting manual abstraction techniques and cross-validation with multiple tools.

Findings

Exhaustive verification feasible for small configurations

No violations of Accountable Safety found in tested instances

Manual abstraction significantly aids in managing complexity

Abstract

We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification. Our primary tools are TLA+ for specification and the Apalache model checker for verification. Our formalization builds on the executable Python specification of 3SF. To begin, we manually translate this specification into TLA+, revealing significant combinatorial complexity in the definition of Accountable Safety. To address these challenges, we introduce several layers of manual abstraction: (1) replacing recursion with folds, (2) substituting abstract graphs with integers, and (3) decomposing chain configurations. To cross-validate our results, we develop alternative encodings in SMT (CVC5) and Alloy. Despite the inherent complexity, our results demonstrate that exhaustive verification of Accountable Safety is feasible for small instances - supporting up to 7 checkpoints and 24 validator votes. Moreover, no violations of Accountable Safety are observed, even in slightly larger configurations. Beyond these findings, our study highlights the importance of manual abstraction and domain expertise in enhancing model-checking efficiency and showcases the flexibility of TLA+ for managing intricate specifications.