Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929677908574208 |
|---|---|
| author | Konnov, Igor Kukovec, Jure Pani, Thomas Saltini, Roberto Tran, Thanh Hai |
| author_facet | Konnov, Igor Kukovec, Jure Pani, Thomas Saltini, Roberto Tran, Thanh Hai |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_07958 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Technical Report: Exploring Automatic Model-Checking of the Ethereum specification Konnov, Igor Kukovec, Jure Pani, Thomas Saltini, Roberto Tran, Thanh Hai Logic in Computer Science Distributed, Parallel, and Cluster Computing F.3.1; C.2.4 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. |
| title | Technical Report: Exploring Automatic Model-Checking of the Ethereum specification |
| topic | Logic in Computer Science Distributed, Parallel, and Cluster Computing F.3.1; C.2.4 |
| url | https://arxiv.org/abs/2501.07958 |