Formal Verification of a Fail-Safe Cross-Chain Bridge

The blockchain ecosystem has rapidly evolved over the last decade, most notably with the rise of Ethereum [32] and Bitcoin [23]. At the end of 2024, the top 636 smart contract blockchains had a market cap of 2.9 trillion dollars [11].

As the blockchain ecosystem continues to grow, it has become increasingly heterogeneous, consisting of blockchains with unique designs and varying characteristics (proof-of-work, proof-of-stake, costs, performance, programming languages, etc.). Thus, each blockchain provides users with a diverse experience, security guarantees, and financial incentives, making it unlikely that a single dominant blockchain design will emerge [7].

Unfortunately, without a method of communication between blockchains, the advantages of a multichain world are limited. Since blockchains have closed-world assumption about their tokens, digital assets are not universal entities and cannot exist outside of their chains.

To this end, decentralized cross-chain bridges have been proposed (e.g., [33]) to provide interoperability between blockchains. Given two blockchains, a cross-chain bridge allows users to transfer tokens from a sender chain $C_s$ to a receiver chain $C_r$. When an asset is transferred from $C_s$ to $C_r$, the asset is locked on $C_s$, and a new asset is minted on $C_r$, representing the original asset on $C_s$. When the newly created asset is transferred back to chain $C_s$, the corresponding asset on $C_r$ is burned, and the locked asset on $C_s$ is released. Smart contracts on both blockchains implement this protocol, and a relay network is used to establish communication between the two chains.

Given the various security exploits targeting bridges [18, 19, 34], designing a safe bridge is paramount. Developing a safe bridge involves guaranteeing several safety and liquidity invariants. For instance, we want to ensure that there is always a 1-to-1 relationship between locked and minted assets. Otherwise, double-spending [17] attacks may arise. Liquidity invariants guarantee that the user can always perform an action to access the their asset. The bridge has fail safety, i.e., that all tokens will be unlocked in a blockchain $C_s$ if blockchain $C_r$ irrecoverably crashes.

Standard audit and testing methods can be employed to increase the likelihood of safety on the bridge. However, these methods, due to their inability to account for all possible behaviors, are insufficient. This is evidenced by the fact that bridges have become notorious targets for hackers. As of 2024, bridge-related hacks cost more than $2.8 billion, representing approximately 40% of all hacks in the Web3 [16]. Given the potential for sizable losses, relying only on ad-hoc testing and auditing techniques is perilous. A more rigorous method to ensure bridge safety is to employ formal verification. Here, we construct mathematical objects describing the bridge behavior and mathematical proofs to ensure the bridge protocol is correct for all possible inputs and configurations.

This paper presents an industrial case study in which we formally prove the safety of the formal abstract model of Sonic Gateway. This cross-chain bridge provides interoperability between the Ethereum and Sonic blockchains. While formal methods have been employed for individual blockchain components [6], to the best of our knowledge, our work is the first to prove the safety of a fail-safe cross-chain bridge model formally.

We formalize the bridge within the interactive theorem prover Isabelle/HOL [25] and establish safety by identifying and proving several fundamental safety properties. We perform our verification using a stepwise refinement approach [31, 9]: We start with an abstract model and then refine it by adding more and more implementation details. This process has verified the final Sonic Gateway design and contributed to the design of cross-chain bridges by identifying essential properties that are pervasive to all fail-safe cross-chain bridges.

Our contributions are summarized as follows:

1. 1.

   A detailed formal description of the fail-safe Sonic Gateway cross-chain bridge including safety properties,

2. 2.

   A formal specification and correctness proof for the Sonic Gateway cross-chain bridge,

3. 3.

   Experimental evaluation and experience of the verification effort.

This paper is structured as follows. Section 2 describes the Sonic Gateway bridge. In Section 3, we detail the formal specification of the Sonic Gateway bridge, and in Section 4, we provide a corresponding proof of its safety. We evaluate the verification process in Section 5, and Section 6 details related work. We conclude in Section 7.

This section describes the Sonic Gateway fail-safe cross-chain bridge. A detailed example of bridge operations is given in Appendix A. The bridge is illustrated in Figure 1. Here, the bridge operates on a pair of blockchains $C_s$ and $C_r$, where $C_s$ is the sender chain, used to deposit (aka. lock) tokens, and $C_r$ is the receiver chain, used to claim (aka. mint) tokens. The blockchain $C_s$ has a smart contract $S{C}_{deposit}$, and $C_r$ has a smart contract $S{C}_{claim}$. For simplicity, we assume that users transfer fungible tokens from an ERC20 [29] contract $T_{orig}$ (although these could also be native tokens of $C_s$) to $C_r$, where they are represented by tokens on a dedicated ERC20 contract $T_{mint}$.

This section briefly outlines the Isabelle/HOL specification of the Sonic fail-safe bridge. Due to space constraints, many details are omitted. For full details, we refer the reader to the Isabelle/HOL source, available at https://github.com/filipmaric/bridge_formalization. We expressed the Sonic bridge implementation, originally in Solidity, as a purely functional program in Isabelle/HOL. Translation from Solidity to Isabelle/HOL is done manually, trying to be as close as possible to Solidity’s semantics. For simplicity, the basic types of Solidity (uint256, bytes32, address) are all modeled as natural numbers in Isabelle/HOL, ignoring overflow issues. In Solidity, mappings storing natural numbers default to 0 for non-existent keys. The function lookup_nat (and similarly lookup_bool) that we define and use mimics that behavior. An Isabelle/HOL record models the internal state of each contract.

The balances mapping in the ERC20State assigns token amounts to user addresses. In the SCDepositState, the locks mapping records all successful Lock transactions, mapping transaction IDs to hash values derived from the sender address, token, and amount. The withdrawals mapping tracks users who executed Withdraw transactions to retrieve balances from the dead bridge. The address of $S{C}_{oracle}$ is stored in SCOracleAddr, while deadState holds the last valid state root before the bridge failure (0 indicates the bridge is not declared dead). States of other contracts (e.g., SCClaimState) are similarly defined.

The storage states of all contracts define the blockchain state, mapping contract addresses to their respective states. Due to the Isabelle/HOL type system, each smart contract type requires a separate mapping.

We define functions to read and modify smart contract states. For example, the following helper function reads a user’s balance from the specified ERC20 contract state.

As in Solidity, contract functions can be called on a chain via a contract address. For instance,

Each call may fail, e.g., if no valid contract exists at the given address. In such cases, the chain state remains unchanged. We defined an Isabelle/HOL counterpart for each contract function by following our Solidity implementation closely. For example, the following Solidity function in the SCDeposit contract checks whether the bridge is dead. The last valid state root hash is stored in the deadState field when the bridge fails.

This function is implemented in Isabelle/HOL as follows:

The function returns a triple: the first element indicates success or failure, the second whether the bridge is dead, and the third the updated state. Monad syntax could remove explicit state passing and status checks.

In our Solidity implementation, some contract functions verify Merkle tree proofs to confirm the presence of specific memory content in another chain, ensuring a key-value pair exists in a mapping. Our specification follows a stepwise refinement approach, omitting proof details and instead postulating axioms that these proofs must satisfy. These axioms are expressed as Isabelle/HOL [4]. First, we postulate that the following functions can be defined so that they satisfy the two given axioms:

• $\mathrm{■}$

  generateStateRoot creates a state root hash value,

• $\mathrm{■}$

  generateLockProof generates a proof for the fact that lock[ID] = val,

• $\mathrm{■}$

  verifyLockProof verifies if the given proof is valid for the given state root.

We also postulate the honesty assumption for the consensus of users who perform the regular state root updates, by assuming that whenever an Update operation succeeds the state root hash given to the oracle is indeed the state root hash of the current blockchain state (as generated by the generateStateRoot function).

This is sufficient to define the token mint operation and prove its properties (for other operations, in the same manner we introduce mint proofs, burn proofs, balance proofs etc.). A concrete implementation for these three abstract functions should be provided at later stages. This implementation can be based on Merkle-tree proofs (as used in our Solidity implementation), but other types of proofs, such as zero-knowledge proofs, could also be used. For illustration, we present our specifications for the mint function.

A blockchain state is considered reachable from a starting state if a sequence of successful operations (steps, transactions) exists that leads to the final state when executed starting from the initial state. To define this relation, we first introduce a representation of the steps (with comments after each step type indicating the step parameters).

Each step is executed by calling its corresponding function on some chain contract.

Finally, we inductively define reachability between two blockchain states. Each state is reachable from itself by the empty list of steps. If ${𝒞}^{\prime }$ is reachable from $𝒞$ by a list steps, and executing step reaches ${𝒞}^{\prime \prime }$ from ${𝒞}^{\prime }$, then ${𝒞}^{\prime \prime }$ is reachable from $𝒞$ by the list obtained by joining steps and step.

Steps issued by a specific caller are interleaved with steps issued by other users. When distinguishing between them is important, we use the predicate reachableInterlaved caller $𝒞$ ${𝒞}^{\prime }$ stepsCaller stepsOther, which is also defined inductively. The following function, defined by primitive recursion, checks whether the given list of steps can be successfully executed, regardless of the steps taken by other users.

We have proven numerous properties of our bridge, beginning with simple, low-level technical properties and culminating in high-level properties that express user safety. The proof concludes with the central fail-safety theorem, which states that even when the bridge is dead, every user can execute a series of transactions to retrieve all their assets (i.e., the tokens they locked, plus the tokens received from others, minus the tokens transferred to others). Our fail-safety features ensure this guarantee and the primary challenge was to prove it formally. The main idea of the proof is as follows.

• $\mathrm{■}$

  If the bridge is alive, after the deposit by a LOCK, the user can make a MINT, then a BURN, and finally RELEASE to retrieve their tokens on the sender chain.

• $\mathrm{■}$

  Assume that the bridge is dead and that the last valid state known on SCDeposit is $𝒞$ (that is the state when the last UPDATE happened before the bridge became unresponsive).

  • –

    If only the LOCK occurred before $𝒞$, and the tokens have not been claimed (or if MINT occurred after the last state update), the user can retrieve their funds using the CANCEL_WD operation.

  • –

    If a MINT is recorded in $𝒞$, and there was no BURN after it (or if it occurred after the last state update), the user has minted tokens in $𝒞$, and can retrieve them using the WITHDRAW_WD operation.

  • –

    Finally, if a BURN is recorded in $𝒞$, the user can retrieve their tokens using the standard RELEASE operation (just as they would while the bridge is active).

Many theorems share assumptions describing the situation where the bridge is dead. Instead of repeating these assumptions in every theorem and deriving their consequences in each proof, we used Isabelle/HOL locales [4]. We defined the locale BridgeDead to describe the state of a dead bridge. This situation is depicted in Fig. 2. The execution begins in some initial state ${𝒞}_I$. For simplicity, we assume that the first operation after the bridge is deployed is a state UPDATE, which transitions it to state ${𝒞}_I^{\prime }$. After this, the bridge operates normally, executing a sequence of steps denoted by stepsInit. At some state ${𝒞}_U$, the final state UPDATE occurs, leading to state ${𝒞}_U^{\prime }$. Following that, additional steps (denoted by stepsNoUpdate) are executed before the bridge becomes inactive. The step that indicates the bridge is dead is denoted by stepDeath. At this point, the field deadState in the SCDeposit contract is set to the state root of the last known valid state, which in this case is ${𝒞}_U$. Subsequently, more steps (denoted by steps) are executed on the SCDeposit contract, leading to the current state $𝒞$. The complete sequence of all steps from ${𝒞}_I$ to $𝒞$ is denoted by stepsAll.

Several auxiliary functions are defined to compute token amounts to formulate the central fail-safety theorem.

• $\mathrm{■}$

  depositedAmountTo – this function calculates the total amount of tokens $T_{orig}$ that a caller has deposited into $S{C}_{deposit}$ by executing Lock transactions.

• $\mathrm{■}$

  retrievedAmountFrom – this function calculates the total amount of tokens $T_{orig}$ that a caller has retrieved from the contract $S{C}_{deposit}$ by executing Release, Withdraw, and Cancel transactions.

• $\mathrm{■}$

  transferredAmountFrom – this function calculates the total amount of minted tokens $T_{mint}$ on the bridge $S{C}_{claim}$ that the caller has transferred to other users, while the function transferredAmountTo calculates the total amount of $T_{mint}$ that other users have transferred to the caller.

When the bridge dies, $S{C}_{oracle}$ contains a state root that encodes aggregated information about all transactions that occurred before the last update before the bridge’s failure (i.e., transactions in the list stepsInit in Figure 2). After this update, transactions (including mints, burns, and transfers) are ignored. We consider a user to have retrieved all their assets if the total amount of tokens they invested (defined as the sum of $T_{orig}$ they locked up to the current state and the $T_{mint}$ they transferred to other users before the last update) is equal to the total amount of tokens they gained (defined as the sum of $T_{orig}$ they retrieved via a Release, Withdraw, or Cancel transaction and the $T_{mint}$ they received from other users before the last update).

Our central theorem demonstrates that, from any state $𝒞$ in which the bridge is dead, each user can issue a list of transactions that will be executable regardless of the transactions made by other users. Moreover, executing these transactions will always result in a state where the user has retrieved all of their tokens.

The steps in the list stepsAll lead from ${𝒞}_{init}$ to $𝒞$. The steps interleaveSteps steps stepsOther, obtained by interleaving the unpredictable steps of other users stepsOther with the steps steps issued by the current user, lead from $𝒞$ to ${𝒞}^{\prime }$, where all tokens have been successfully retrieved.

Note that a similar, less interesting theorem can be proven when the bridge is not dead (under some additional assumptions on the frequency of updates). In this scenario, the caller only needs to issue MINT, BURN, and RELEASE transactions. However, there is no guarantee that the bridge will not fail during the execution of these transactions. If this occurs, the user must switch to the recovery strategy used when the bridge is dead.

Many necessary lemmas contribute to the proof of the central theorem. We formulated and proved lemmas that ensure the executability of each specific operation. For instance, the following theorem guarantees lock cancellation is possible if no claim of minted tokens was made before the last update before the bridge became inactive and if no cancellation occurred before the current state.

Theorems for other “rescue” operations are similar. It is typically necessary to prove that a particular step is possible by showing that some data is set in the required manner. For example, canceling a deposit ID by a caller who requests a specific token amount is only possible if the proof that guarantees that locks[ID] = hash(caller, token, amount) can be verified. It is proved (by induction) that this data guarantees that there was a prior LOCK operation from the caller for the given amount of the give token $T_{orig}$ (assuming that hash function is injective, which is a widespread assumption in a blockchain setting). However, repaying tokens for a canceled deposit also requires enough tokens $T_{orig}$ in the SCDeposit contract balance. This is the most challenging part of the entire proof, as it requires careful analysis of the “cash flow” across all parts of the bridge, considering all operations and steps. Such invariants are proven both globally (characterizing the SCDeposit contract balance after transactions from all users) and on a per-user basis (characterizing $T_{orig}$ and $T_{mint}$ balances for each user). Due to space constraints, we will describe only the former. We introduce the following quantities (all are natural numbers, so they are non-negative):

• $\mathrm{■}$

  SCDepositBalance – the current token balance of the given $S{C}_{Deposit}$ address.

• $\mathrm{■}$

  locked / canceled / withdrawn / released – the total sum of amounts in all LOCK / CANCEL_WD / WITHDRAW_WD / RELEASE steps for a given $S{C}_{deposit}/S{C}_{claim}$ address and token.

• $\mathrm{■}$

  mintedBeforeDeath – the total sum of amounts in all MINT steps executed before the last update before the bridge becomes inactive.

• $\mathrm{■}$

  nonMintedBeforeDeath – the total sum of amounts in all LOCK steps whose ID is not claimed (minted) before the last update before the bridge becomes inactive.

• $\mathrm{■}$

  nonCanceledNonMintedBeforeDeath – the total sum of amounts in all LOCK steps whose ID is not minted before the last update before the bridge becomes inactive and which has not been canceled.

• $\mathrm{■}$

  nonWithdrawnNonBurnedMintedBeforeDeath – the total amount of tokens produced by MINT steps that have not been burned before the last update before the bridge becomes inactive, and have not been withdrawn.

• $\mathrm{■}$

  burnedBeforeDeath – the total sum of amounts in BURN steps for a given address and token that were executed before the last update, when the bridge becomes inactive.

• $\mathrm{■}$

  nonReleasedBurnedBeforeDeath – the total sum of amounts in all BURN steps for a given address and token, that were executed before the last update before the bridge becomes inactive whose ID has not yet been released.

Then, we proved the following five invariants.

1. 1.

   locked = SCDepositBalance + canceled + withdrawn + released

2. 2.

   locked = mintedBeforeDeath + nonMintedBeforeDeath

3. 3.

   nonMintedBeforeDeath = canceled + nonCanceledNonMintedBeforeDeath

4. 4.

   mintedBeforeDeath = withdrawn + nonWithdrawnNonBurnedMintedBeforeDeath +

   burnedBeforeDeath

5. 5.

   burnedBeforeDeath = released + nonReleasedBurnedBeforeDeath

The first invariant is proved by induction by analyzing the transactions that change the token deposit balance. The second invariant is trivial. The others focus on specific operations and are proven by induction and case analysis of the last applied step, where most steps are irrelevant (for example, only MINT and CANCEL_WD operations are relevant for the third invariant). Combining these four invariants yields

SCDepositBalance = nonCanceledNonMintedBeforeDeath +

nonWithdrawnNonBurnedMintedBeforeDeath + nonReleasedBurnedBeforeDeath

From this, we can guarantee sufficient funds for each rescue operation. For instance, when proving that a cancel step is possible, there is a deposit that was not claimed before the last update before the bridge died and that has not yet been canceled. Therefore, the it’s amount is included in the nonCanceledNonMintedBeforeDeath quantity, which, by the previous invariant, is less than or equal to the SCDepositBalance, i.e., the current token balance of the SCDeposit contract. Since the amount the caller requires must match the amount they deposited (which we know from the value of locks[ID] = hash(caller, token, amount), and the assumed injectivity of the hash function), the contract contains the required tokens, making the payback possible. Similar reasoning applies to all other operations.

Many other lower-level properties had to be proven to support the correctness proof. For example, each Mint must be preceded by a Lock, only the entity who made a lock can mint the tokens, once the bridge dies, it can never become life again, etc. We refer readers to the Isabelle/HOL proof documents for their formalization.

The Isabelle formalization was completed by a single individual who had worked part-time on this project for over six months. A rough estimate suggests the formalization required approximately 2–3 full person-months of effort. Isabelle’s definition of the bridge’s formal model comprises around 900 lines of code (LOC), including approximately 50 defined functions, while the accompanying proofs span roughly 15,000 LOC. The current proof contains approximately 750 lemmas and theorems. The proof-checking process takes around 8 minutes on a standard laptop computer (Intel(R) Core(TM) i5-8265U CPU @ 1.60GHz, 8GB of RAM). However, this time could be significantly reduced by replacing several time-consuming, fully automated proofs with more detailed manual proofs.

Several underlying assumptions in our model pose threats to validity and must be addressed to ensure the total correctness of a real-world bridge implementation. Some of these assumptions can be easily ensured through a correct deployment process.

• $\mathrm{■}$

  It is assumed that contracts are correctly deployed and initialized, i.e., that all addresses are correctly set up.

• $\mathrm{■}$

  It is assumed that each bridge and original token has a dedicated minted token, i.e., that minted tokens are not shared.

• $\mathrm{■}$

  It is assumed that users initially have no minted tokens after the bridge is deployed.

• $\mathrm{■}$

  It is assumed that an UPDATE operation occurs immediately after the bridge is deployed, i.e., that the bridge never operates in a state where state roots are uninitialized.

Other assumptions include the following:

• $\mathrm{■}$

  It is assumed that arithmetic overflows will not occur while the bridge is in operation. This is reasonable, as the only arithmetic operations involve updating user token balances.

• $\mathrm{■}$

  It is assumed that the hash function is injective (i.e., no hash collisions) and always produces a nonzero value. This is a common assumption underlying blockchain security.

• $\mathrm{■}$

  It is assumed that (Merkle-tree) proof checking is fully sound. This is also reasonable, as the correctness of Merkle trees has been formally verified.

• $\mathrm{■}$

  Transaction fees and gas prices are not included in our model.

• $\mathrm{■}$

  Reentrancy attacks are not considered. Although reentrancy poses a significant threat in Solidity smart contracts, it can be prevented through careful implementation (e.g., by following the checks-effects-interactions pattern).

• $\mathrm{■}$

  It is assumed that updates are reliable, i.e., that validators are always honest. This assumption may be the most problematic, as many successful bridge attacks have been carried out by corrupting validators [34]. While specifying the details of a validation protocol can help relax this assumption, some risks will always remain. For example, private keys must be kept secure.

BFT consensus protocols have been verified using interactive theorem provers. The work in [6] develops a modular proof in TLA+ for DAG-based consensus protocols. The work in [26] uses the IVy interactive theorem prover [1] to formally verify a variant of the Moonshine consensus protocol [26]. The work in [21] uses IVy and Isabelle/HOL [24] to verify the Stellar Consensus Protocol [20]. The Algorand [13] consensus protocol has been verified using Coq [12]. The safety of several non-Byzantine protocols, such as variants of Paxos [10, 28] has been verified using interactive theorem proving. To the best of our knowledge, we are the first to propose formal proof for a cross-chain bridge, particularly bridge failure safety.

There has been foundational work in the verification of Ethereum smart contracts. These contracts are compiled into Ethereum Virtual Machine (EVM) bytecode, formally defined for use with interactive theorem provers [14]. A sound program logic at the bytecode level has also been developed [3]. Typically, smart contracts are written in the Solidity programming language, with formal semantics defined in Isabelle/HOL [22]. Another proposed approach in smart contract verification is to define them in specialized languages converted to low-level byte code using verified compilers. For example, Britten’s PhD thesis [8] explores techniques to improve the reliability and security of smart contracts by leveraging formal verification methods through interactive theorem proving in Coq, combined with a verified compiler from the language DeepSEA [30]. In [27], Ribeiro defines the imperative language soli within Isabelle/HOL that captures a significant subset of Solidity, and develops big-step, Hoare logic, and a proof system for it, with soundness and completeness results formally established.

Our approach differs in that the formal bridge model is currently represented as a functional program within Isabelle/HOL, derived through manual translation from Solidity. Consequently, our current work establishes only the correctness of a high-level bridge model, leaving the verification of its Solidity implementation for future work.

Various automated tools analyze Solidity code and detect bugs or violations of specific safety properties (for example, since 2019, the Solidity compiler has included a model checker, SolCMC [2]). However, a key limitation of these tools is their lack of effectiveness in expressing and verifying liquidity properties. Some automated tools are also designed explicitly for verifying liquidity properties, such as Solvent [5].

Our decision to use the interactive theorem prover Isabelle/HOL instead of automated tools was influenced by our prior experience and the fact that any limitations in automated prover support can be overcome by reverting to manual proofs. One possible research direction would be to examine whether state-of-the-art automated tools are capable of proving the liquidity properties of large-scale projects such as a crypto-bridge.

This paper describes the Sonic Gateway fail-safe bridge design and its formalization in Isabelle/HOL. We have formally proven that users can still retrieve all their assets on the sender chain even if the bridge becomes unresponsive on the receiver chain.

Our current abstract model does not account for numerous essential real-world issues, such as gas consumption, potential overflows, reentrancy vulnerabilities, and other Solidity-specific implementation challenges. Addressing these practical concerns will be an integral part of our efforts to ensure that the model reflects these complexities and security requirements in a real-world deployment. Therefore, we plan to bridge the gap between the current abstract Isabelle/HOL bridge model and its real Solidity implementation in our future work. To achieve this, we must provide a detailed description of the Inter-Blockchain Communication (IBC) Relay, which utilizes Merkle-tree proofs and whose correctness is currently only assumed in our formalization. Additionally, we plan to leverage the formal semantics of Solidity in Isabelle/HOL [22] to verify our bridge up to the Solidity implementation level fully formally.