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.
@InProceedings{maric_et_al:OASIcs.FMBC.2025.8, author = {Mari\'{c}, Filip and Scholz, Bernhard and Suboti\'{c}, Pavle}, title = {{Formal Verification of a Fail-Safe Cross-Chain Bridge}}, booktitle = {6th International Workshop on Formal Methods for Blockchains (FMBC 2025)}, pages = {8:1--8:18}, 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.8}, URN = {urn:nbn:de:0030-drops-230342}, doi = {10.4230/OASIcs.FMBC.2025.8}, annote = {Keywords: Cross-Chain Bridge, Formal Verification, Logic, Security} }
Feedback for Dagstuhl Publishing