YO Protocol Async Redemption Escrow Accounting

x

shares
The share component supplied to fulfillRedeem or cancelRedeem.

\le

\operatorname{pendingSharesOf}(\sigma,r)

pendingSharesOf
The receiver's aggregate pending-share record before settlement.

\quad\land\quad

a

gross assets
The gross underlying-asset component supplied to settlement.

\le

\operatorname{pendingAssetsOf}(\sigma,r)

pendingAssetsOf
The receiver's aggregate pending gross assets before settlement.

\operatorname{pendingSharesOf}(\sigma',r)

post-state pending shares
The same receiver's pending shares after successful settlement.

=

\operatorname{pendingSharesOf}(\sigma,r)

pre-state pending shares
The shares recorded for the receiver before settlement.

-x

\operatorname{pendingAssetsOf}(\sigma',r)

post-state pending assets
The same receiver's pending gross assets after settlement.

=

\operatorname{pendingAssetsOf}(\sigma,r)

pre-state pending assets
The gross assets recorded for the receiver before settlement.

-a

\operatorname{totalPendingAssetsOf}(\sigma')

post-state totalPendingAssetsOf
YO's global gross pending-asset counter after settlement.

=

\operatorname{totalPendingAssetsOf}(\sigma)

pre-state totalPendingAssetsOf
YO's global gross pending-asset counter before settlement.

-a

A successful settlement cannot subtract more shares or gross assets than that receiver has pending. It subtracts exactly the accepted amounts.

View Lean

YO Protocol queues a vault redemption when idle underlying assets cannot satisfy it immediately. Its pinned YoVault.sol async-redemption logic pools the shares and tracks aggregate pending shares and gross assets by receiver. YoAsyncRedemptionEscrow is the Lean model for this source slice. This case proves the successful request, fulfillment, cancellation, and selected lifecycle transitions stated in Specs.lean.

Why It Matters

When a redemption is queued, the vault records the receiver's shares, the assets they are owed, and the total assets reserved for all queued redemptions. These records must change together. Otherwise, the vault could burn too many shares, reduce a user's claim, or treat reserved assets as available.

The units at risk are YO vault shares and the vault's underlying asset units. For the deployed yoUSD escrow on Base, the underlying asset is USDC. The proven fulfillment path also burns exactly the selected shares, splits the selected gross assets into net assets plus the current withdrawal fee, and, under the modeled no-callback-mutation boundary, leaves every other receiver's pending record unchanged.

What the source also permits

YO confirmed that this flexibility is intentional. If the vault's value becomes uncertain after an incident, the authorized operator can settle a request at a lower exchange rate.

The contract checks the shares and assets separately. It prevents the operator from using more than the receiver has pending, but it does not require the two amounts to remain proportional, or even to both be greater than zero. For example, a request for 100 shares and 200 assets could be settled as 1 share and 199 assets.

A settlement with one amount set to zero can leave the remaining record temporarily stuck. A later redemption request for the same receiver can make it usable again.

This flexibility relies on trusting the authorized Redeemer. The proof confirms that the contract's accounting remains within the recorded limits, but it does not decide whether the chosen rate is fair or protect users if the Redeemer key is compromised.

How This Was Modeled and Proven

We recreated the relevant async-redemption logic in Verity, including requests, fulfillment, cancellation, authorization, share movements, fees, and reverts. We then defined the exact accounting rules that each action must follow.

Lean checked those rules against the model for every permitted input, rather than testing only a selection of examples. The 14 resulting proofs cover the normal lifecycle and selected failure paths. All proofs are complete, with no case-specific axioms or sorry placeholders.

Scope

The model covers the async redemption slice of the pinned YO source: requestRedeem, redeem, fulfillRedeem, cancelRedeem, the internal withdrawal path, authorization, fee updates, and the relevant share transfer and burn helpers.

External preview, ERC-20 balance reads, authority calls, and token transfers are explicit success or revert outcomes. The model proves the escrow's own storage transitions and rollback at the selected boundaries. It assumes no authority or token callback mutates modeled vault storage while a boundary call is in flight. It does not prove external token balances, callback code, oracle pricing, or the implementation of the external authority contract.

Deposits, mints, yield strategy execution, manage, upgrade governance, and event logs are out of scope. The source tracks aggregate records by receiver rather than per-request IDs, and the model keeps that exact aggregation.

This is an accounting proof. It does not prove that an emergency settlement rate is fair, that the vault is solvent, or that the authorized Redeemer key cannot be compromised.

Proof artifacts

Contract.lean models the escrow transition surface.
Specs.lean defines the accounting and lifecycle properties.
Proofs.lean contains all 14 reference proofs.
Compile.lean imports the complete case as the reproducibility target.
Case directory contains the complete benchmark slice.
Benchmark pull request contains the reviewed change set.

Function	Theorem	Status
requestRedeem	request_redeem_branching	proven
requestRedeem	queued_request_aggregation	proven
requestRedeem	two_owner_queue_aggregation	proven
redeem	redeem_wrapper	proven
fulfillRedeem	fulfill_redeem_accounting	proven
cancelRedeem	cancel_redeem_accounting	proven
fulfillRedeem	lifecycle_bounds_and_isolation	proven
fulfillRedeem / cancelRedeem	zero_component_lifecycle	proven
request / settle	candidate_g_source_reachability	proven
request / settle / repair	malformed_pair_lifecycle	proven
request / fulfill / replay	full_clear_requeue_replay	proven
fulfillRedeem	owner_fallback_authorization	proven
fulfillRedeem / cancelRedeem	lifecycle_rollback	proven
fee update / fulfillRedeem	fee_aliasing	proven

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout 7d15f0054037ab6d866888d7ab2e80c64c0d15e9
lake build Benchmark.Cases.YOProtocol.AsyncRedemptionEscrow.Compile

This target imports the contract model, specifications, and all reference proofs. A successful build means Lean checked that complete case. Source repository

Assumptions

These three boundaries summarize the detailed preconditions in the Lean theorems. The complete technical conditions remain available in Proofs.lean; the case adds no Lean axioms.

trusted authorizationan authorized operator chooses the settlement values
YO authorization model
The proof checks what the vault does after a Redeemer or owner is authorized. It does not verify the live role configuration, judge the operator's chosen emergency rate, or protect an existing request if an authorized key is compromised or misused.
external callsexternal calls return the modeled result and do not change vault storage through callbacks
model boundary
Oracle previews, token balance reads, authority checks, and token transfers are modeled as success or revert outcomes. The proof covers the vault's storage changes and selected rollback paths, not the internal behavior or balances of those external contracts.
valid starting statethe vault starts in a valid state and the selected calls satisfy their runtime guards
Solidity execution conditions
The modeled share ledger begins well formed, arithmetic fits within Solidity's limits, and successful calls meet checks such as sufficient balances and a live pending record. The reviewed Base deployment also uses separate addresses for USDC and yoUSD.

Learn More

More Research

Enzyme Onyx Dynamic Fee Accounting

Formally verified management-first fee ordering and exact owed-value accounting for Enzyme Onyx FeeHandler.

for

Superfluid CFA Realtime-Balance Conservation

Formally verified conservation of CFA flow accounting, including a one-level callback.

for

1inch XYCSwap Curve Safety

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

for