Document Open Access Logo

Formal Verification of a Fail-Safe Cross-Chain Bridge

Authors Filip Marić , Bernhard Scholz , Pavle Subotić

PDF HTML 5

Files

Thumbnail PDF
PDF
OASIcs.FMBC.2025.8.pdf
  • Filesize: 1.32 MB
  • 18 pages
HTML5 Logo HTML (experimental)
OASIcs.FMBC.2025.8.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • Cross-Chain Bridge
  • Formal Verification
  • Logic
  • Security

Metrics

Abstract

Cross-chain bridges are financial services that interconnect blockchains. High monetary values flow through these bridges, and their security must be safeguarded. However, designing real-world cross-chain bridges is a difficult endeavor. Due to blockchain’s closed-world nature, tokens cannot be transferred from a sender to a receiver chain; on the contrary, they need complex logic that maintains an equilibrium on both chains, even if either the chains or the bridge fail. This paper formally verifies a model of a novel fail-safe cross-chain bridge to ensure correctness. We define formal requirements and prove the bridge is safe using the Isabelle/HOL proof assistant.

Cite As Get BibTex

Filip Marić, Bernhard Scholz, and Pavle Subotić. Formal Verification of a Fail-Safe Cross-Chain Bridge. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/OASIcs.FMBC.2025.8

Author Details

Filip Marić
  • University of Belgrade, Serbia
Bernhard Scholz
  • Sonic Research, Sydney, Australia
Pavle Subotić
  • Sonic Research, Belgrade, Serbia

Acknowledgements

We want to thank Sonic Labs engineers Jan Kalina and Jirka Malek for designing and implementing the fail-safe bridge. Without their insights and explanations, we would not have been able to build the model.

Supplementary Materials

References

  1. Ki Yung Ahn and Ewen Denney. Testing first-order logic axioms in program verification. In Gordon Fraser and Angelo Gargantini, editors, Tests and Proofs - 4th International Conference, TAP@TOOLS 2010, Málaga, Spain, July 1-2, 2010. Proceedings, volume 6143 of Lecture Notes in Computer Science, pages 22-37. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13977-2_4.
  2. Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, and Natasha Sharygina. Solcmc: Solidity compiler’s model checker. In Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I, pages 325-338, Berlin, Heidelberg, 2022. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-13185-1_16.
  3. Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. Towards verifying ethereum smart contract bytecode in isabelle/hol. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 66-77, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167084.
  4. Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and Proof Contexts. In Mathematical Knowledge Management, MKM, Proceedings, pages 31-43, 2006. URL: https://doi.org/10.1007/11812289_4.
  5. Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, and Vadim Malvone. Solvent: Liquidity verification of smart contracts. In Nikolai Kosmatov and Laura Kovács, editors, Integrated Formal Methods, pages 256-266, Cham, 2025. Springer Nature Switzerland. Google Scholar
  6. Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, and Pavle Subotic. Reusable formal verification of dag-based consensus protocols. CoRR, abs/2407.02167, 2024. URL: https://doi.org/10.48550/arXiv.2407.02167.
  7. Bloomberg. Multi-chain future likely as ethereum’s defi dominance declines. https://www.bloomberg.com/professional/insights/data/multi-chain-future-likely-as-ethereums-defi-dominance-declines/ , February 2022.
  8. Daniel Britten. Building trustworthy smart contracts using interactive theorem proving. Doctor of philosophy (phd) thesis, The University of Waikato, 2024. Supervisors: Steve Reeves, Vimal Kumar. URL: https://hdl.handle.net/10289/16566.
  9. Dominique Cansell. Foundations of the B method. Computers and Informatics, 22, January 2003. Google Scholar
  10. Saksham Chand, Yanhong A. Liu, and Scott D. Stoller. Formal verification of multi-paxos for distributed consensus. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 119-136, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_8.
  11. CoinGecko. Top smart contract platform coins by market cap. https://www.coingecko.com/en/categories/smart-contract-platform , November 2024.
  12. Thierry Coquand and Gérard P. Huet. The calculus of constructions. Inf. Comput., 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  13. Yossi Gilad, Rotem Hemo, Silvio Micali, Georgios Vlachos, and Nickolai Zeldovich. Algorand: Scaling Byzantine agreements for cryptocurrencies. In Proceedings of SOSP 2017, pages 51-68. ACM, 2017. URL: https://doi.org/10.1145/3132747.3132757.
  14. Yoichi Hirai. Defining the ethereum virtual machine for interactive theorem provers. In Michael Brenner, Kurt Rohloff, Joseph Bonneau, Andrew Miller, Peter Y.A. Ryan, Vanessa Teague, Andrea Bracciali, Massimiliano Sala, Federico Pintore, and Markus Jakobsson, editors, Financial Cryptography and Data Security, pages 520-535, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-70278-0_33.
  15. Kamil Jezek. Ethereum data structures. CoRR, abs/2108.05513, 2021. URL: https://doi.org/10.48550/arXiv.2108.05513.
  16. Defi Lama. Hacks. https://defillama.com/hacks, November 2024.
  17. Sung-Shine Lee, Alexandr Murashkin, Martin Derka, and Jan Gorzny. Sok: Not quite water under the bridge: Review of cross-chain bridge hacks. CoRR, abs/2210.16209, 2022. URL: https://doi.org/10.48550/arXiv.2210.16209.
  18. Sung-Shine Lee, Alexandr Murashkin, Martin Derka, and Jan Gorzny. Sok: Not quite water under the bridge: Review of cross-chain bridge hacks. In 2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2023. URL: https://doi.org/10.1109/ICBC56567.2023.10174993.
  19. Ningran Li, Minfeng Qi, Zhiyu Xu, Xiaogang Zhu, Wei Zhou, Sheng Wen, and Yang Xiang. Blockchain cross-chain bridge security: Challenges, solutions, and future outlook. Distrib. Ledger Technol., October 2024. Just Accepted. URL: https://doi.org/10.1145/3696429.
  20. Marta Lokhava, Giuliano Losa, David Mazières, Graydon Hoare, Nicolas Barry, Eli Gafni, Jonathan Jove, Rafal Malinowsky, and Jed McCaleb. Fast and secure global payments with stellar. In Tim Brecht and Carey Williamson, editors, Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, pages 80-96. ACM, 2019. URL: https://doi.org/10.1145/3341301.3359636.
  21. Giuliano Losa and Mike Dodds. On the formal verification of the stellar consensus protocol. In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference), volume 84 of OASIcs, pages 9:1-9:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/OASICS.FMBC.2020.9.
  22. Diego Marmsoler and Achim D. Brucker. Isabelle/solidity: A deep embedding of solidity in isabelle/hol. Form. Asp. Comput., October 2024. Just Accepted. URL: https://doi.org/10.1145/3700601.
  23. Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system, May 2009. URL: http://www.bitcoin.org/bitcoin.pdf.
  24. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  25. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  26. M. Praveen, Raghavendra Ramesh, and Isaac Doidge. Formally verifying the safety of pipelined moonshot consensus protocol. In Bruno Bernardo and Diego Marmsoler, editors, 5th International Workshop on Formal Methods for Blockchains, FMBC 2024, April 7, 2024, Luxembourg City, Luxembourg, volume 118 of OASIcs, pages 3:1-3:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/OASIcs.FMBC.2024.3.
  27. Maria Saraiva de Campos Mendes Ribeiro. Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL. Master’s thesis, Instituto Superior Técnico, 2019. Supervisors: Paulo Alexandre Carreira Mateus, Pedro Miguel dos Santos Alves Madeira Adão. URL: https://fenix.tecnico.ulisboa.pt/downloadFile/1689244997260666/tese_maria_ribeiro.pdf.
  28. William Schultz, Ian Dardik, and Stavros Tripakis. Formal verification of a distributed dynamic reconfiguration protocol. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 143-152. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503688.
  29. Rudrapatna K. Shyamasundar. Erc20: Correctness via linearizability and interference freedom of the underlying smart contract. In Proceedings of the 20th International Conference on Security and Cryptography - Volume 1: SECRYPT, pages 557-566. INSTICC, SciTePress, 2023. URL: https://doi.org/10.5220/0012145800003555.
  30. Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, and Zhong Shao. Foundational verification of smart contracts through verified compilation, 2024. URL: https://doi.org/10.48550/arXiv.2405.08348.
  31. Niklaus Wirth. Program development by stepwise refinement. Commun. ACM, 14(4):221-227, April 1971. URL: https://doi.org/10.1145/362575.362577.
  32. Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger, 2014. EIP-150 Revision. URL: https://ethereum.github.io/yellowpaper/paper.pdf.
  33. Tiancheng Xie, Jiaheng Zhang, Zerui Cheng, Fan Zhang, Yupeng Zhang, Yongzheng Jia, Dan Boneh, and Dawn Song. zkbridge: Trustless cross-chain bridges made practical. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS '22, pages 3003-3017, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3548606.3560652.
  34. Mengya Zhang, Xiaokuan Zhang, Yinqian Zhang, and Zhiqiang Lin. Security of cross-chain bridges: Attack surfaces, defenses, and open problems. In Proceedings of the 27th International Symposium on Research in Attacks, Intrusions and Defenses, RAID '24, pages 298-316, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3678890.3678894.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact