Beyond Audits: Mathematically Verifying the Safety of the Sonic Gateway

TL;DR

The Sonic Gateway is Sonic’s native decentralized bridge. It facilitates token transfers between Ethereum and Sonic and provides an innovative fail-safe mechanism.

In case either the Gateway or Sonic experiences prolonged failures, users can recover their bridged funds on Ethereum. The security of the Gateway is paramount due to the considerable value secured. As of April 2025, we’ve already locked a value of $1.09B.

To go beyond testing and auditing, the state of practice in the blockchain industry, we took an uncompromising security posture and have provided the first formal verification of a fail-safe bridge. Formal verification is a field in computer science that mathematically checks a system's behavior using formal/logical models and their properties.

Introduction

The Sonic Gateway has been extensively tested and audited independently by three auditing companies (OpenZepelin, Certora, Quantstamp). However, we have nonetheless gone a step further and formally verified the Gateway’s design to show with mathematical rigor that it’s safe.

We prove that all Gateway behaviours in the logical gateway model cannot result in users losing funds. We’re the first to apply formal verification to a cross-chain bridge. At Sonic, we strongly champion rigorous mathematical guarantees in Web3 and predict that formal verification will be standard practice for all Web3 components in the future.

This article introduces the Sonic Gateway's anatomy and describes how it operates. We outline how we specified and proved its correctness using the Isabelle/HOL proof assistant, a semi-automated proof system for higher-order logic theorems. The entire specification and proof can be found here. 

The Sonic Gateway

The Sonic Gateway is a fail-safe bridge that can transfer tokens between Ethereum and Sonic. The term "fail-safe" refers to the fact that users will not lose funds if the bridge fails (e.g. crashes).

Figure 1 shows the Sonic Gateway. The bridge operates on a pair of blockchains, C_s and C_r, where C_s is the sender chain (Ethereum) used to deposit tokens, and C_r is the receiver chain (Sonic) used to claim tokens.

To implement a bridge, the blockchain C_s has a smart contract SCdeposit, and C_r has a smart contract SCclaim. Token transfers from C_s to C_r operate using a pair of transactions denoted as Lock and Mint. Assuming that a user already has at least v tokens available on C_s, the user invokes a Lock transaction on C_s (step 1) to transfer tokens in their balance to the SCdeposit balance.

To verify that a Lock transaction has been successfully executed, SCdeposit keeps a log containing data about all executed lock transactions. Before tokens can be issued by SCclaim on C_r using a Mint transaction (step 2), the solvency needs to be ensured. SCclaim issues new tokens only if the user has locked tokens on SCdeposit. This requires SCclaim operating on C_r to read the state of SCdeposit from a different blockchain (C_s), which it cannot do directly. The bridge uses Merkle proofs, which act as a trusted witness to check whether the tokens were locked. 

The witness proves the existence of a specific transaction (or its effect) for blockchain C_r at a block height on blockchain C_s. This Merkle proof is an existence argument for the Mint transaction. Simultaneously, the state root hash of the world state of C_s is shipped via the trusted channel, the Inter-Blockchain Communication (IBC) Relay.

We assume that a special contract SCoracle keeps track of state root hashes and that a consensus of trusted users regularly updates the state root hashes by invoking Update transactions. When executing a Mint transaction, the contract SCclaim on C_r verifies that the Lock transaction took place on C_s at block height using the Merkle proof and state root hash of C_s read from SCoracle, which confirms that the log locks contain valid data about the Lock transaction.

If the proof verification succeeds, the user's balance is increased by v. To prevent double claims of the same deposit, SCclaim keeps a directory of minted deposits. Burn and Release transactions (steps 3 and 4) are similar to Lock and Mint transactions; we omit these details. 

What is unique to the Sonic Gateway is that it implements a mechanism that enables users to retrieve their funds on C_s, even if the bridge goes out of operation. The bridge is declared dead once the SCoracle contract (on C_s) does not execute a state root update transaction within a fixed time. The bridge is declared dead by setting a dead flag in the SCdeposit contract and copying the last known state root of C_r from SCoracle to SCdeposit.

Once the bridge is declared dead, this status cannot be undone. When the bridge is dead, users retrieve their assets using Withdraw and Cancel transactions. Furthermore, note that Release transactions do not depend on C_r and are executed similarly, regardless of whether the bridge is dead.

The last known state root hash of C_r verifies the user's balance. If the user had v tokens on C_r when the last state root was given to the SCoracle, they can generate a Merkle tree proof for that and invoke a Withdraw transaction on SCdeposit.  When the proof verification succeeds, v tokens are transferred from the SCdeposit contract to the user's balance. Every withdrawal transaction is logged in the withdrawals array to prevent double withdrawals.

Finally, the user has deposited and locked some v tokens on C_s but has not yet claimed them, or they have claimed them. Still, there was no state root update after that claim, so there are no corresponding tokens on C_r that they could retrieve using the Withdraw operation.

A Cancel transaction must be used in such cases. With this transaction, the user provides a Lock transaction ID and the Merkle tree proof that there was no corresponding Mint on SCclaim on C_r in the last known state. Once the Cancel transaction is successful, the information about the canceled Lock transaction is removed from the locks log to prevent double cancellation.

Specification and Proof

We want to ensure that the Sonic Gateway's design works as intended. First, we describe the design in mathematical language, describing the properties that must hold. We then work with a theorem prover to add additional properties to the design so the theorem prover can certify its safety. 

We use Isabelle/HOL as a verification framework. We perform the verification process using a stepwise refinement approach. We start with an abstract model and refine it by adding more implementation details. This process has verified the final 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.

As with many formal method specifications, we view the system as a transition system. We first specify the state of the contracts. For instance, we could define a record type for the state of SCdeposit and collate all the contracts as a mapping of address to contract state.

We define transition steps as transactions and their associated arguments as shown below:

We define a recursive execution step and encode how the state changes with each transition. 

Reachability between blockchain states is defined inductively. Each state is reachable from itself. If C′ is reachable from C by a series of steps, and executing a step reaches C′′ from C′, then C′′ is reachable from C by the combined series of steps.

The predicate reachableInterleaved caller C C' stepsCaller stepsOther is defined inductively and checks whether the steps can be executed, regardless of the steps taken by other users.

We define the properties we want to hold for the transition system. For instance, we always want an equilibrium between blockchain tokens: 

The central theorem below stipulates that from any state where the bridge is unusable, each user can issue transactions that will execute independently of other users' transactions and always result in retrieving all the user's tokens.

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 model's source code, properties, and proofs can be found here. 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).

Future Work

We plan to continue the verification effort for auxiliary components (e.g.,, MPT, relay) in the future and evaluate design improvements. In addition, we’ll be interested in formally proving Sonic’s economy in conjunction with the SFC contract and the bridges.