Arbitration games from Referee Delegation of Computations are central to layer two optimistic rollup architectures (L2), one of the most prominent mechanisms for scaling blockchains. L2 blockchains operate on the principle that computations are valid unless proven otherwise. Challenging incorrect computations requires users to construct fraud proofs through a dispute resolution process that involves two opposing players. Fraud proofs are objects that establish when proposed computations are invalid, and they are so computationally small and cheap that can be checked by the underlying trusted blockchain. Arbitration games, this challenging process, involve one player posing strategic questions and another player revealing details about computations. Arbitration games start from the posting of Disputable Assertions (DAs), DAs contain partial information about computations including their result. Since there is no trust between players, hashes are posted as compact witnesses of knowledge. One player provides information decomposing hashes while the other decides which "path" to take navigating the computation trace. When a path is exhausted, all the required information to compute the result from the data provided following the path has been revealed and the path can be proven to be faulty or correct. We explore in this paper the formalization of arbitration games in Lean4, introducing the first machine-checkable strategies that honest players can play guaranteeing success. These strategies ensure: on one side, the successful debunking of dishonest computations via the construction of fraud proofs, while in the other, the successful navigation of the challenge process through correct answers. In short, these are the winning strategies that honest players (on both sides) can follow. We explore in this paper formal abstractions to capture disputable assertions, arbitration games on finite binary trees asserting data-availability and membership, game transformations, and then discuss how to work towards a general formal framework for referee delegation of computations.
@InProceedings{ceresa_et_al:OASIcs.FMBC.2025.5, author = {Ceresa, Mart{\'\i}n and S\'{a}nchez, C\'{e}sar}, title = {{Towards a Mechanization of Fraud Proof Games in Lean}}, booktitle = {6th International Workshop on Formal Methods for Blockchains (FMBC 2025)}, pages = {5:1--5:17}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-371-3}, ISSN = {2190-6807}, year = {2025}, volume = {129}, editor = {Marmsoler, Diego and Xu, Meng}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.5}, URN = {urn:nbn:de:0030-drops-230327}, doi = {10.4230/OASIcs.FMBC.2025.5}, annote = {Keywords: blockchain, formal methods, layer-2, optimistic rollups, arbitration games} }
Feedback for Dagstuhl Publishing