StarkGate Bridge Escrow Lower Bound

escrow_lower_bound_spec(s) := assetBalanceOfassetBalanceOf(s)
The modeled ERC20 token balance held by the StarkGate bridge contract on L1.(s) ≥ cumulativeDepositsOfcumulativeDepositsOf(s)
Total tokens accepted by the bridge through successful deposit calls. Each deposit increments this counter.(s) − cumulativeWithdrawalsOfcumulativeWithdrawalsOf(s)
Total tokens released by the bridge through withdrawals and deposit reclaims. Each outflow increments this counter.(s)

The L1 bridge balance always covers cumulative deposits minus cumulative withdrawals.

View Lean

StarkGate is the canonical token bridge between Ethereum L1 and Starknet L2. Users deposit tokens on L1, which are held in escrow by the StarknetTokenBridge contract until they are claimed on L2. Conversely, L2 withdrawals trigger L1 token releases. The unit at risk is the ERC20 balance locked in the bridge contract.

We formally verified the fundamental escrow accounting rule: the bridge balance must always cover total accepted deposits minus total released outflows. If this invariant broke, tokens credited on L2 would lack backing on L1.

Why It Matters

A token bridge holds user funds in escrow. Every deposit increases a cumulative counter; every withdrawal or reclaim increases a second counter. The difference between these counters is the outstanding liability: tokens deposited on L1 that have not yet been withdrawn or reclaimed. The bridge's actual token balance must never fall below this liability, or the bridge would be unable to fulfill a legitimate withdrawal.

If the escrow accounting allowed the balance to drop below the outstanding liability, a user who deposited tokens and later received them on L2 could find no backing on L1 when they try to withdraw back. The invariant is the fundamental solvency guarantee that makes the bridge trustworthy.

What this invariant covers

The proof covers the modeled accounting effect of deposit, withdraw, and depositReclaim. Each transition updates the ghost balance and cumulative counters, and the proof shows the lower bound holds in the post-state.

The invariant is a lower bound, not an equality. The bridge balance can exceed deposits minus withdrawals if tokens are sent directly to the contract without going through deposit, or if fee accruals increase the balance. Both cases strengthen the lower bound rather than violating it.

How this was modeled and proven

The Verity model tracks the L1 escrow accounting slice: the bridge's token balance, cumulative accepted deposits, and cumulative withdrawals. Cross-domain Starknet messaging, L2-side logic, fee mechanics, and the per-token deployment lifecycle are abstracted as gates on the successful path. Each function is modeled as a transition that updates three ghost variables, and each proof shows the arithmetic update preserves the lower bound.

The model is in Contract.lean. The invariant is in Specs.lean, and the reference proofs are in Proofs.lean.

Function	Theorem	Status
deposit	deposit_preserves_escrow_lower_bound	proven
withdraw	withdraw_preserves_escrow_lower_bound	proven
depositReclaim	depositReclaim_preserves_escrow_lower_bound	proven

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
lake build Benchmark.Cases.Starkware.StarkgateEscrow.Compile

If the build succeeds, the proofs are correct. Source repository

Scope

The proof covers the three core L1 bridge functions that move token balance: deposit, withdraw, and depositReclaim. All three compile with zero sorry and zero axiom.

Cross-domain Starknet messaging (sending L1-to-L2 messages, consuming L2-to-L1 messages, cancelling pending deposits) is modeled as a gate that succeeds on the modeled path. The proof checks the resulting accounting update, not the messaging transport.

Proof artifacts

Contract.lean: Verity model of the StarkGate L1 bridge accounting
Specs.lean: the escrow lower-bound invariant specification
Proofs.lean: three reference theorems with no sorry or axiom

Modeling simplifications

The L1 ERC20 balance is modeled as a ghost assetBalance. External token storage and transfer mechanics are outside the bridge accounting slice.
Cumulative deposits and withdrawals are modeled as two ghost counters. Each deposit increments the deposit counter; each withdrawal or reclaim increments the withdrawal counter. The invariant uses Nat subtraction, so when withdrawals exceed deposits the bound is zero and holds trivially.
Fee mechanics are modeled as donation-equivalent: fees that accrue to the bridge balance increase the left-hand side without affecting the counters, which strengthens the lower bound.
The proof models a single token type at a time. Each token bridge deployment is an independent contract instance with its own balance and counters, so multi-token interactions cannot interfere.

Assumptions

The proofs use zero Lean axioms. The items below are theorem hypotheses for the successful Solidity path: require guards and Solidity 0.8 checked-arithmetic facts. They are grouped here by meaning; the Lean file keeps them explicit so each proof obligation remains auditable.

deposit guardamount > 0hAmountGt0
deposit require guard
The bridge rejects zero-amount deposits. The proof only needs this to select the successful execution path; it does not affect the accounting arithmetic.
withdrawal balanceamount ≤ assetBalancehAmountLeBalance
successful transfer and checked subtraction
Outflows only succeed when the bridge balance can cover the withdrawal amount. This is what prevents the proof from relying on underflow behavior.
checked arithmeticbalance + amount, deposits + amount, withdrawals + amount < 2^256hAssetNoOverflow, hDepNoOverflow, hWithdNoOverflow
Solidity 0.8 checked arithmetic
This is the non-overflow case for Solidity 0.8 checked arithmetic. If an addition to a Uint256 slot would overflow, the real call reverts. The theorem covers the matching successful path where that addition fits in 256 bits.

View in Lean

Learn more

What is a formal proof? A short explanation for non-specialists.

More research

1inch XYCSwap Curve Safety

Formally verified fee-adjusted constant-product curve safety for 1inch Aqua XYCSwap.

for

Pendle PY Supply Pairing

Formally verified PT and YT supply-pairing accounting for Pendle V2 mintPY and successful pre-expiry redeemPY paths.

for

KyberSwap Partial-Fill Price Floor

Formally verified helper-level partial-fill price-floor guard for MetaAggregationRouterV2.

for