2026-08-04T09:40:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23034 2025-10-02T12:30:31Z ddc:004 open_access

Formal Verification of a Fail-Safe Cross-Chain Bridge Marić, Filip Scholz, Bernhard Subotić, Pavle Cross-Chain Bridge Formal Verification Logic Security 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Filip Marić and Bernhard Scholz and Pavle Subotić 2025 Is Part Of OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2025.8 urn:nbn:de:0030-drops-230342 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.8 eng https://creativecommons.org/licenses/by/4.0/legalcode