ForgeYields Gateway Solvency

ForgeYields uses a TokenGateway to account for assets that move between local user actions, pending redeem claims, and remote bridge flows. The unit at risk is the ERC20 asset held by the gateway.

This case study verifies the active-mode accounting rule for TokenGateway: the gateway balance must cover the active buffer plus assets reserved for redeems. Once the gateway enters depreciation mode, ForgeYields intentionally stops using _redeemInfo.assetsLocked, so the invariant is guarded by depreciated.

Why this matters

The gateway has two local claims on its ERC20 balance: liquid buffer assets and assets already locked for users who requested a redeem. The buffer is the spendable part of the gateway balance: assets that remain available for active operations such as remote transfers or future redeem locking. If active code allowed buffer plus locked redeems to exceed the token balance, a later redeem, bridge transfer, or report could operate on accounting that the contract cannot fund.

How this was modeled and proven

The Verity model tracks the gateway's local solvency slice: token balance, buffer, locked redeem assets, and depreciation status. ERC20 calls, Hyperlane messages, report bytes, redeem NFTs, and bridge dispatch are represented by decoded scalar inputs or ghost balance updates because the invariant depends on their accounting effect, not the external transport.

The model is in Contract.lean. The guarded invariant is in Specs.lean, and the reference proofs are in Proofs.lean. The proof splits on active versus depreciated mode, then proves the arithmetic update for each successful path.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.ForgeYields.GlobalSolvency.Compile

Proof status

Proven. All seven reference theorems compile with zero sorry and zero axiom.

Proof Inputs

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

• modedepreciated == 0 or depreciated != 0

  TokenGateway mode require guards

  Active functions prove the numeric balance inequality. The depreciated redeem path proves the guarded invariant through the depreciation branch.

• available accountingassets ≤ buffer, assets ≤ assetsLocked, assets ≤ assetBalance

  successful require guards and transfer success

  Outflows only succeed when the modeled accounting bucket being decremented can cover the amount. This is what prevents the proof from relying on underflow behavior.

• handle lock boundlockAssets ≤ buffer + assetsIn

  decoded handle message successful path

  Inbound messages can move assets into locked redeem accounting only after the resulting buffer can cover the lock.

• checked arithmeticassetBalance + assets, buffer + assets, assetsLocked + assets < 2^256

  Solidity 0.8 checked addition

  Whenever the model adds to a Uint256 slot, the theorem states the same non-overflow condition Solidity requires for the call to continue.

A Lean-facing simplification would be to package these into predicates such as successfulActiveOutflow and successfulCheckedAdd. That would shorten theorem signatures, but it would not remove any proof obligation. Keeping them explicit makes the benchmark easier to audit.

Learn more

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