Async Redemptions on YO: Now Mathematically Proven Safe

A redemption on YO can never settle for more shares than you asked for — that's now a mathematical proof, not just a design goal.

Since May 2025, only 0.6% of redemptions on YO have needed to queue at all. Here's what happens when they do, and how we know the accounting behind it can't go wrong.

What happens when you redeem

When you redeem from a YO vault, the vault first tries to pay you out immediately using idle funds the vault is holding.

That covers the vast majority of redemptions. But a yield vault's job is to keep funds working, not sitting idle. So once in a while, there isn't enough idle cash on hand to cover a redemption instantly. When that happens, the vault doesn't reject your request — it queues it. The vault records exactly what you're owed and pays you as soon as funds free up.

That queue is what "async redemption" means: you ask for your money, and the payout lands a little later instead of immediately.

The real question, especially for anyone building on top of YO: while a request sits in that queue, could the bookkeeping drift? Could the vault take more of your shares than you asked for, or shortchange your payout? That's what got tested.

What "formally verified" actually means

Most security reviews are audits: reviewers read the code, run through test scenarios, and give their opinion. That's useful but it only checks the situations someone thought to test.

Formal verification is a stricter bar. Independent firm Verity Labs turned YO's redemption-queue logic into a mathematical model, wrote down the exact rules the accounting has to follow, and checked those rules against every possible input — not just the ones a human tester might think of. If a single input could break a rule, the proof fails outright.

YO's vaults passed every proof, with no exceptions carved out. The work covers the entire redemption lifecycle: requesting, fulfilling, cancelling, and the share transfer and burn steps underneath.

The guarantee, in plain terms

When a redemption settles, the vault can never take more shares or pay out more assets than you actually requested. What you asked for is the hard limit.

Your payout is your requested amount, nothing more, nothing less. Everyone else's pending redemptions stay untouched while yours settles. No request can reach into anyone else's funds.

Check the proof yourself

The full model, specs, and all 14 proofs are public. Developers can clone the benchmark and rebuild the case locally:

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

A successful build means Lean, the verification tool Verity Labs used, has independently re-checked the entire proof from scratch.

Read the full technical writeup: veritylabs.dev/research/yo-async-redemption-escrow-accounting