Document Open Access Logo

Future Monitors in Optimistic Rollups

Authors Margarita Capretto , Martín Ceresa , César Sánchez

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2026.7.pdf
  • Filesize: 2.03 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
Keywords
  • Optimistic Rollups
  • Layer-2
  • Fraud Proof
  • Monitorability
  • Future

Metrics

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 Get BibTex

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) https://doi.org/10.4230/OASIcs.FMBC.2026.7

Author Details

Margarita Capretto
  • IMDEA Software Institute, Madrid, Spain
  • Universidad Politécnica de Madrid (UPM), Spain
Martín Ceresa
  • Input Output, Madrid, Spain
César Sánchez
  • IMDEA Software Institute, Madrid, Spain

Funding

This work was funded in part by the DECO Project (PID2022-138072OB-I00) funded by MCIN/AEI/10.13039/501100011033 and by the ESF+, FPI PREP2022-000334 and Grant CEX2024-001471-M funded by MICIU/AEI/10.13039/501100011033.

References

  1. Wolfgang Ahrendt and Richard Bubel. Functional verification of smart contracts via strong data integrity. In Proc. 9th Int'l Symp, on Leveraging Applications of Formal Methods, Verification and Validation: Applications (ISoLA'20)), volume 12478 of LNCS, pages 9-24. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_2.
  2. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. ConCert: a smart contract certification framework in Coq. In Proc. of the 9th ACM SIGPLAN Int'l Conf. on Certified Programs and Proofs (CPP'20), pages 215-218. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373829.
  3. Shaun Azzopardi, Joshua Ellul, and Gordon J. Pace. Monitoring smart contracts: ContractLarva and open challenges beyond. In Proc. of the 18th Int'l Conf. on Runtime Verification (RV'18), volume 11237 of LNCS, pages 113-137. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03769-7_8.
  4. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In Proc. of the 1st Workshop on Formal Methods for Blockchains (FMBC'19), volume 12232 of LNCS, pages 368-379. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_28.
  5. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fourneta, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella Béguelin. Formal verification of smart contracts: Short paper. In Proc. of Workshop on Programming Languages and Analysis for Security (PLAS@CCS'16), pages 91-96. ACM, 2016. URL: https://doi.org/10.1145/2993600.2993611.
  6. Ran Canetti, Ben Riva, and Guy N. Rothblum. Practical delegation of computation using multiple servers. In Proc. of the 18th ACM Conf. on Computer and Communications Security (CCS'11), pages 445-454. ACM, 2011. URL: https://doi.org/10.1145/2046707.2046759.
  7. Ran Canetti, Ben Riva, and Guy N. Rothblum. Refereed delegation of computation. Information and Computation, 226:16-36, 2013. URL: https://doi.org/10.1016/j.ic.2013.03.003.
  8. Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sanchez, and César Sánchez. A secure sequencer and data availability committee for rollups. In Proc. of the 2025 ACM SIGSAC Conf. on Computer and Communications Security, (CCS'25), pages 2129-2143. ACM, 2025. URL: https://doi.org/10.1145/3719027.3765187.
  9. Margarita Capretto, Martín Ceresa, and César Sánchez. Transaction monitoring of smart contracts. In Proc. of the 22nd Int'l Conf. on Runtime Verification (RV'22), volume 13498 of LNCS, pages 162-180. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17196-3_9.
  10. Margarita Capretto, Martín Ceresa, and César Sánchez. Monitoring the future of smart contracts. In Proc. of the 27th Int'l Conf. on Fundamental Approaches to Software Engineering (FASE'24), volume 14573 of LNCS, pages 122-142. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57259-3_6.
  11. Martín Ceresa and César Sánchez. Towards a mechanization of fraud proof games in lean. In 6th Int'l Workshop on Formal Methods for Blockchains, (FMBC'25), volume 129 of OASIcs, pages 5:1-5:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/OASIcs.FMBC.2025.5.
  12. Sylvain Conchon, Alexandrina Korneva, and Fatiha Zaïdi. Verifying smart contracts with Cubicle. In Proc. of the 1st Workshop on Formal Methods for Blockchains (FMBC'19), volume 12232 of LNCS, pages 312-324. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_23.
  13. Joshua Ellul and Gordon J. Pace. Runtime verification of Ethereum smart contracts. In Proc. of the 14th European Dependable Computing Conference (EDCC'18), pages 158-163. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/EDCC.2018.00036.
  14. Harry Kalodner, Steven Goldfeder, Xiaoqi Chen, S. Matthew Weinberg, and Edward W. Felten. Arbitrum: Scalable, private smart contracts. In Proc. of the 27th USENIX Conf. on Security Symposium (USENIX Security 18), pages 1353-1370. USENIX Association, 2018. URL: https://www.usenix.org/conference/usenixsecurity18/presentation/kalodner.
  15. Ao Li, Jemin Andrew Choi, and Fan Long. Securing smart contract with runtime validation. In Proc. of 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'20), pages 438-453. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385982.
  16. Ralph C. Merkle. A digital signature based on a conventional encryption function. In A Conf. on the Theory and Applications of Cryptographic Techniques on Advances in Cryptology (CRYPTO'87), pages 369-378. Springer-Verlag, 1988. Google Scholar
  17. Satoshi Nakamoto. Bitcoin: a peer-to-peer electronic cash system, 2008. Google Scholar
  18. Zeinab Nehaï and François Bobot. Deductive proof of industrial smart contracts using Why3. In Proc. of the 1st Workshop on Formal Methods for Blockchains (FMBC'19), volume 12232 of LNCS, pages 299-311. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_22.
  19. Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. VerX: Safety verification of smart contracts. In Proc of the 41st IEEE Symp. on Security and Privacy (S&P'20), pages 1661-1677. IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00024.
  20. Daian Phil. Analysis of the dao exploit, 2016. URL: https://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/.
  21. Jonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert, and Richard Bubel. Formal analysis of smart contracts: Applying the KeY system. In Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, volume 12345 of LNCS, pages 204-218. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64354-6_8.
  22. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Scilla: a Smart Contract Intermediate-Level LAnguage. https://arxiv.org/abs/1801.00687, 2018.
  23. Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. SmartPulse: Automated checking of temporal properties in smart contracts. In Proc. of the 42nd IEEE Symp. on Security and Privacy (S&P'21), pages 555-571. IEEE, 2021. URL: https://doi.org/10.1109/SP40001.2021.00085.
  24. Nick Szabo. Smart contracts: Building blocks for digital markets. Extropy, 16, 1996. Google Scholar
  25. WebAssembly Working Group. WebAssembly. URL: https://webassembly.org/.
  26. Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, 2014. Google Scholar
  27. Bin Yu, Xu Lu, Hao Chen, Ming Lei, and Xiaobing Wang. Runtime verification of Ethereum smart contracts based on MSVL. In Proc. of the Int'l Workshop on Structured Object-Oriented Formal Language and Method (SOFL+MSV 2020), volume 12723 of LNCS, pages 142-153. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-77474-5_10.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact