Volume
OASIcs, Volume 142
7th International Workshop on Formal Methods for Blockchains (FMBC 2026)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC)
Event
Editors
Publication Details
- published at: 2026-05-20
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-424-6
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 142, FMBC 2026, Complete Volume
Abstract
OASIcs, Volume 142, FMBC 2026, Complete Volume
Cite as
7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 1-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{bartoletti_et_al:OASIcs.FMBC.2026,
title = {{OASIcs, Volume 142, FMBC 2026, Complete Volume}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {1--124},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026},
URN = {urn:nbn:de:0030-drops-260025},
doi = {10.4230/OASIcs.FMBC.2026},
annote = {Keywords: OASIcs, Volume 142, FMBC 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bartoletti_et_al:OASIcs.FMBC.2026.0,
author = {Bartoletti, Massimo and Marmsoler, Diego},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {0:i--0:xiv},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.0},
URN = {urn:nbn:de:0030-drops-260015},
doi = {10.4230/OASIcs.FMBC.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Scaling Formal Verification Across DeFi Ecosystems (Invited Talk)
Abstract
Formal verification is essential for ensuring the safety of smart contracts in decentralized finance (DeFi), but scaling these techniques across diverse blockchain ecosystems remains a challenge. In this talk, we present our experience making formal verification practical across multiple platforms, including the EVM, Solana, Stellar, and Sui. We discuss how automated reasoning techniques can be adapted to different execution models and programming paradigms while still providing strong correctness guarantees. We focus on what it takes to apply verification in real-world settings: handling complex DeFi primitives, integrating with development workflows, and maintaining usability for engineers. Drawing from verification projects with production protocols, we highlight key challenges and lessons learned in bringing formal methods from theory into practice.
Cite as
Pamina Georgiev. Scaling Formal Verification Across DeFi Ecosystems (Invited Talk). In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{georgiev:OASIcs.FMBC.2026.1,
author = {Georgiev, Pamina},
title = {{Scaling Formal Verification Across DeFi Ecosystems}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {1:1--1:1},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.1},
URN = {urn:nbn:de:0030-drops-256986},
doi = {10.4230/OASIcs.FMBC.2026.1},
annote = {Keywords: Formal Verification, Smart Contracts}
}
Document
Invited Talk
Verifying zkEVMs: Making Large Scale Formal Verification Work (Invited Talk)
Abstract
The effort to formally verify core parts of zkVMs for their deployment on the Ethereum L1 has been ongoing for over a year now, with many teams involved and progress across several axes. This talk will focus on formally verifying such a large, complex, and unstable stack, the lessons learned, and the remaining challenges.
Cite as
Alexander Hicks. Verifying zkEVMs: Making Large Scale Formal Verification Work (Invited Talk). In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hicks:OASIcs.FMBC.2026.2,
author = {Hicks, Alexander},
title = {{Verifying zkEVMs: Making Large Scale Formal Verification Work}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {2:1--2:1},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.2},
URN = {urn:nbn:de:0030-drops-256995},
doi = {10.4230/OASIcs.FMBC.2026.2},
annote = {Keywords: Formal Verification, Zero-Knowledge Virtual Machines}
}
Document
Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL
Abstract
Smart contracts deployed on the Ethereum blockchain execute on the Ethereum Virtual Machine (EVM) and handle financial operations such as payments, asset transfers, and auctions. Given the high value they control, correctness in these contracts is critical, as errors and vulnerabilities have led to losses totalling hundreds of millions of dollars. To address this problem, we develop a novel formalization of the EVM. Compared to existing formalizations, our formalization is in Isabelle/HOL, covers all current EVM opcodes, and formalizes cross-contract execution. Thus, it allows us to express properties which are out of scope for other formalizations. To allow for the execution of our formalization, we implement a code generator, allowing it to be exported as a stand-alone Haskell program. We then validate the semantics by executing νmprint{25000} test cases from the official Ethereum test suite. Our formalization can be used to verify concrete smart contracts but also to reason about the correctness of tools and techniques which manipulate bytecode, such as compilers or optimizers.
Cite as
Ashley Card and Diego Marmsoler. Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{card_et_al:OASIcs.FMBC.2026.3,
author = {Card, Ashley and Marmsoler, Diego},
title = {{Isabelle/EVM: A Novel Formalization of the EVM in Isabelle/HOL}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {3:1--3:16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.3},
URN = {urn:nbn:de:0030-drops-257005},
doi = {10.4230/OASIcs.FMBC.2026.3},
annote = {Keywords: Ethereum Virtual Machine, Isabelle/HOL, Smart Contracts}
}
Document
A Formal Approach to AMM Fee Mechanisms with Lean 4
Abstract
Decentralized Finance (DeFi) has revolutionized financial markets by enabling complex asset-exchange protocols without trusted intermediaries. Automated Market Makers (AMMs) are a central component of DeFi, providing the core functionality of swapping assets of different types at algorithmically computed exchange rates. Several mainstream AMM implementations are based on the constant-product model, which ensures that swaps preserve the product of the token reserves in the AMM - up to a trading fee used to incentivize liquidity provision. Trading fees substantially complicate the economic properties of AMMs, and for this reason some AMM models abstract them away in order to simplify the analysis. However, trading fees have a non-trivial impact on users' trading strategies, making it crucial to develop refined AMM models that precisely account for their effects. In this work, we extend a foundational model of AMMs by introducing a new parameter, the trading fee ϕ ∈ (0,1], into the swap rate function. Fee amounts increase inversely proportional to ϕ. When ϕ = 1, no fee is applied and the original model is recovered. We analyze the resulting fee-adjusted model from an economic perspective. We show that several key properties of the swap rate function, including output-boundedness and monotonicity, are preserved. At the same time, other properties - most notably additivity - no longer hold. We precisely characterize this deviation by deriving a generalized form of additivity that captures the effect of swaps in the presence of trading fees. In particular, we prove that when ϕ < 1, executing a single large swap yields strictly greater profit than splitting the trade into smaller ones. Finally, we derive a closed-form solution to the arbitrage problem in the presence of trading fees and prove its uniqueness. All results are formalized and machine-checked in the Lean 4 proof assistant.
Cite as
Marco Dessalvi, Massimo Bartoletti, and Alberto Lluch-Lafuente. A Formal Approach to AMM Fee Mechanisms with Lean 4. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dessalvi_et_al:OASIcs.FMBC.2026.4,
author = {Dessalvi, Marco and Bartoletti, Massimo and Lluch-Lafuente, Alberto},
title = {{A Formal Approach to AMM Fee Mechanisms with Lean 4}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {4:1--4:18},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.4},
URN = {urn:nbn:de:0030-drops-257015},
doi = {10.4230/OASIcs.FMBC.2026.4},
annote = {Keywords: Smart contracts, Decentralized Finance, Verification, Blockchain}
}
Document
Smart Tests for a Smart Contract Language
Abstract
Smart contracts are high-stakes software: their immutable, publicly accessible, code may govern assets worth millions, meaning that even minor defects can have severe consequences. The most used techniques to ensure smart contract correctness are testing and formal verification. Testing is almost always employed but is often restricted to unit tests (which often miss edge cases) and has limited coverage, while formal verification can provide strong guarantees but is often costly and complex to apply, demanding substantial time and expertise. Property-based testing bridges this gap by exploring large input spaces and shrinking failures to minimal counterexamples, helping uncover defects early in development. Formal verification can be left to critical features once testing has filtered out common issues.
To add to the challenges smart contract developers face, most languages used were not designed with safety and security guarantees built-in. Daml is a smart contract language designed with correctness in mind, featuring a strong static type system, functional programming paradigms, and built-in abstractions for common smart contract patterns. However, Daml currently lacks support for property-based testing, limiting developers' ability to systematically explore input spaces and verify contract properties.
This paper introduces Hypothesis2Daml, an open-source library that brings property-based testing to the Daml ecosystem by connecting the Hypothesis testing framework with the Daml JSON API. Hypothesis2Daml enables developers to specify invariants, preconditions, and stateful workflows over realistic ledger interactions, while providing automatic input generation, shrinking, and isolation of ledger state between test cases. The approach is evaluated using a benchmark consisting of eight contracts, three Daml templates, and twenty-eight property-based tests covering happy paths, negative cases, and alternative interaction orders. The results show that property-based testing is feasible for Daml smart contracts, can systematically expose violated properties with minimal counterexamples, and supports effective debugging of realistic, stateful workflows.
Cite as
Miguel Valido and António Ravara. Smart Tests for a Smart Contract Language. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{valido_et_al:OASIcs.FMBC.2026.5,
author = {Valido, Miguel and Ravara, Ant\'{o}nio},
title = {{Smart Tests for a Smart Contract Language}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {5:1--5:14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.5},
URN = {urn:nbn:de:0030-drops-257021},
doi = {10.4230/OASIcs.FMBC.2026.5},
annote = {Keywords: Smart contracts, Blockchain, Daml, Property-based testing, Hypothesis}
}
Document
Deductive Verification of SmartML Smart Contracts with KeY
Abstract
Unintended behavior in smart contracts can lead to major financial losses. Due to the immutable nature of blockchains, it is of utmost importance to ensure the functional correctness of smart contracts before deployment. Formal verification is a powerful technology for such critical applications, as it can show the absence of errors. Current approaches focus on verifying programs on specific blockchains, such as the Ethereum Virtual Machine (EVM). Consequently, the SmartML smart contract modeling language was developed to design smart contracts independently of any particular blockchain.
In this work, we present a novel approach for formally verifying SmartML contracts via an automatic translation to Java Card and the Java Modeling Language (JML). We extend SmartML with SmartJML, a JML-like specification language, and describe how SmartML and SmartJML can be automatically translated into Java Card and JML. With this, the established deductive verification tool KeY can be used for conducting proofs on the generated Java Card program. The faithfulness of our translation ensures that the obtained guarantees hold for the original SmartML models. In addition to the theoretical work, we provide a prototypical implementation of the automatic translation and evaluate it with a case study of an escrow.
Cite as
Tudor Christian Balan, Wolfram Pfeifer, and Adele Veschetti. Deductive Verification of SmartML Smart Contracts with KeY. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{balan_et_al:OASIcs.FMBC.2026.6,
author = {Balan, Tudor Christian and Pfeifer, Wolfram and Veschetti, Adele},
title = {{Deductive Verification of SmartML Smart Contracts with KeY}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {6:1--6:16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.6},
URN = {urn:nbn:de:0030-drops-257030},
doi = {10.4230/OASIcs.FMBC.2026.6},
annote = {Keywords: Formal Verification, Deductive Verification, Smart Contract Verification}
}
Document
Future Monitors in Optimistic Rollups
Abstract
Blockchains are decentralized systems that provide trustable execution guarantees. Most modern blockchains offer smart contracts, programs governing the functionality and logic of blockchain transactions. The model of computation of smart contracts is typically transactional: either transactions immediately revert or immediately commit. When transactions commit, the effect of executing them becomes permanent and cannot be undone.
Future monitors were proposed as a defense mechanism that enables smart contracts to state properties across multiple transactions. By delaying the consolidation of a transaction, future monitors wait for future transactions to occur before committing or failing.
Optimistic Rollups provide the perfect environment to implement future monitors. These systems are layer-2 solutions proposed for scaling blockchains, and they delay transaction effects in order to allow observers to challenge and remove malicious block proposals.
In this paper, we describe an implementation of future monitors in Optimistic Rollups. We propose a succinct way to encode all potential future states in rollup blocks. We provide novel fraud-proof mechanisms designed to arbitrate the high-level algorithm that determines the effect of transactions using future monitors. Finally, we present winning strategies for honest players, proving that our fraud-proof mechanisms preserve the guarantees of Optimistic Rollups while enabling future monitor capabilities.
Cite as
Margarita Capretto, Martín Ceresa, and César Sánchez. Future Monitors in Optimistic Rollups. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{capretto_et_al:OASIcs.FMBC.2026.7,
author = {Capretto, Margarita and Ceresa, Mart{\'\i}n and S\'{a}nchez, C\'{e}sar},
title = {{Future Monitors in Optimistic Rollups}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {7:1--7:18},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.7},
URN = {urn:nbn:de:0030-drops-257043},
doi = {10.4230/OASIcs.FMBC.2026.7},
annote = {Keywords: Optimistic Rollups, Layer-2, Fraud Proof, Monitorability, Future}
}
Document
Detecting Cross-Function Reentrancy from EVM Traces
Abstract
Reentrancy remains one of the most critical vulnerabilities affecting Ethereum smart contracts. While many existing analysis tools focus on detecting classical single-function reentrancy, more complex forms such as cross-function reentrancy are harder to identify because they depend on execution semantics and interactions between multiple functions. In this work, we study reentrancy at the level of Ethereum Virtual Machine (EVM) execution traces. We extend the TxSpector framework with new Datalog-based detection rules designed to capture cross-function reentrancy patterns. To support this analysis, we also modernize the trace extraction component by adapting it to recent versions of the Ethereum client and updated EVM instructions. The proposed approach is evaluated on real Ethereum on-chain transaction traces. The results show that our method is able to detect cross-function reentrancy behaviors that are not captured by the original TxSpector rules, demonstrating the effectiveness of pattern-based logic detection at the EVM execution level.
Cite as
Semia Guesmi, Carla Piazza, Andrea Gasparetto, Matteo Rizzo, and Sabina Rossi. Detecting Cross-Function Reentrancy from EVM Traces. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{guesmi_et_al:OASIcs.FMBC.2026.8,
author = {Guesmi, Semia and Piazza, Carla and Gasparetto, Andrea and Rizzo, Matteo and Rossi, Sabina},
title = {{Detecting Cross-Function Reentrancy from EVM Traces}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {8:1--8:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.8},
URN = {urn:nbn:de:0030-drops-257058},
doi = {10.4230/OASIcs.FMBC.2026.8},
annote = {Keywords: Blockchain, smart contract, Reentrancy detection, EVM, design Patterns, logic rules}
}
Document
Short Paper
Towards Property-Based Testing of Smart Contracts Using Gas Analysis (Short Paper)
Abstract
Testing has become an integral part of the software development process in order to ensure the correct and safe execution of programs. A powerful approach to testing is property-based testing that aims at generating unit tests that verify that a certain property of interest holds. However, smart contracts are also characterized by important non-functional aspects, such as the gas consumption required to execute their functions. Static gas analyzers are able to obtain parametric gas bounds - that soundly over-approximate - the gas consumption of executing each of the public functions within a smart contract. This paper discusses our ideas towards combining both formal methods, property-based testing and gas analysis, in order to generate gas-aware unit tests that can ensure the gas requirements provided by the programmers.
Cite as
Elvira Albert, Emanuele De Angelis, Marco Di Ianni, Fabio Fioravanti, and Pablo Gordillo. Towards Property-Based Testing of Smart Contracts Using Gas Analysis (Short Paper). In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 9:1-9:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{albert_et_al:OASIcs.FMBC.2026.9,
author = {Albert, Elvira and De Angelis, Emanuele and Di Ianni, Marco and Fioravanti, Fabio and Gordillo, Pablo},
title = {{Towards Property-Based Testing of Smart Contracts Using Gas Analysis}},
booktitle = {7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
pages = {9:1--9:8},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-424-6},
ISSN = {2190-6807},
year = {2026},
volume = {142},
editor = {Bartoletti, Massimo and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.9},
URN = {urn:nbn:de:0030-drops-257069},
doi = {10.4230/OASIcs.FMBC.2026.9},
annote = {Keywords: Property-based Testing, Blockchain, Ethereum, Gas}
}