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 It 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

Hypotheses

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.

• active and depreciated modes proven separately

  TokenGateway mode require guards

  Every path is proven in both cases: depreciated == 0 (active) or depreciated != 0 (depreciated). Active functions prove the numeric balance inequality. The depreciated redeem path proves the guarded invariant through the depreciation branch.

• outflows never exceed what they draw from

  successful require guards and transfer success

  An outflow succeeds only when the accounting bucket it decrements covers the amount: assets ≤ buffer, assets ≤ assetsLocked, and assets ≤ assetBalance. Require guards and transfer success enforce this. It keeps the proof from relying on underflow behavior.

• inbound messages lock only what the buffer covers

  decoded handle message successful path

  A successful handle message requires lockAssets ≤ buffer + assetsIn. So inbound messages move assets into locked redeem accounting only after the resulting buffer can cover the lock.

• balance additions never overflow

  Solidity 0.8 checked addition

  The sums assetBalance + assets, buffer + assets, and assetsLocked + assets must each stay below 2^256. 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.