When the Proof Refuses, You're Looking at an Attack.

Part 1 ended with the vault preserving its token-price invariant: under every non-loss action, the vault-token price never decreases. That rules out one whole class of attacks — nobody round-trips through the vault and walks out with more than they put in.

But "you can't profit from a round trip" is only half of what a depositor cares about. The other half is the symmetric question: if I round-trip a deposit, how much do I lose to rounding? The floors in the vault's conversion formulas are tuned in the vault's favor — that's how the first attack gets ruled out — so some loss is unavoidable. The question is whether it's bounded, by how much, and under what conditions.

This post turns "loss is bounded" into a machine-checked theorem. The interesting part isn't the proof; the proof is mechanical. The interesting part is that the shape of the side conditions Lean forces on us turns out to be the same shape as a well-known class of real-world attacks — and reading the proved bound back against deployment reality is itself the security analysis.

Asking for the obvious thing

The natural property to state is: for any deposit a, the round-trip loss is at most some small fraction ε of a.

To say this cleanly we move to ℚ — it's awkward to express "0.01%" or "1 basis point" in ℕ without manual cross-multiplications, and the Lean ecosystem handles rationals well enough that there's no reason not to. The tolerance ε becomes a parameter; pick any positive rational.

The theorem we want is something like:

theorem deposit_then_redeem_loss_naive
    {s s' s'' : State} {user : Addr} {a shares assets_back : ℕ} {ε : ℚ}
    (hε_pos : 0 < ε)
    (hd : deposit s user a = some (s', shares))
    (hr : redeem s' user shares = some (s'', assets_back)) :
    (a : ℚ) - (assets_back : ℚ) < ε * (a : ℚ) := by sorry

deposit returns the new state alongside the shares it minted; redeem returns the new state alongside the assets it paid out. The round trip is just "feed the shares from deposit into redeem," and the loss is the difference between what went in (a) and what came back (assets_back).

Hand this to the AI and ask for a proof. It will fail. The interesting part is how it fails.

The counter-example is the donation attack

Push it for the counter-example and you get back:

a * (T + vT) < B + vA

With T and B for the vault's share supply and asset balance, and vT/vA for Part 1's virtual offsets, this says the per-vault-token price (B + vA) / (T + vT) is larger than a itself — pricing one full vault token costs more assets than the depositor is bringing in. The floor in vaultTokenFor sends the depositor's share count to zero; the subsequent redeem of zero shares returns zero assets; the loss is 100% of the deposit.

This shape — deposit small relative to a high price, fresh depositor wiped out — is the donation-attack precondition¹. An attacker inflates B by transferring assets directly into the vault (a path that doesn't mint shares; the transfer just shows up as a "profit" event on the vault's books). The per-share price spikes. The next depositor's deposit, if it's small relative to that spiked price, gets rounded to zero shares.

So the AI's refusal isn't a tooling limitation. The theorem we tried to prove is genuinely false, and the witness for its falsity is a known exploit pattern. The proof attempt did exactly what we asked of it — and in doing so, handed us back the threat model.

The two-line refinement — and what Lean does for you

The counter-example tells us the bound has to be conditional. We can already guess the rough shape, in plain English:

• the price shouldn't be too high relative to what a depositor pays;
• the deposit shouldn't be too small.

Notice: these are not bounds. They are vague directions. "Not too high" relative to what? Smaller than what number? The actual side conditions, the ones that make the theorem provable, are specific functional relationships between the price, the deposit, the tolerance ε, and possibly other quantities. We don't know them.

That's fine. We don't have to.

The Lean-based AI workflow is built around exactly this gap. You hand the AI the two informal directions — "find me bounds on the price and the deposit that make this provable" — and let it propose specific side conditions and try to prove the theorem under them. If the proposed bounds are right, Lean accepts the proof; if they're wrong, Lean rejects it, and the AI iterates. There is no path to "looks plausible but is actually wrong": the kernel either accepts the script or it doesn't.

This is the part that does the heavy lifting. Without Lean in the loop, an AI that proposes a side condition is just guessing, and you have to vet the guess by hand. With Lean in the loop, the AI proposes and defends its guess; if it can't defend it, you get a precise error to iterate against. Wrong bounds fail loudly. Right bounds compile.

After a handful of iterations — the AI proposes a bound, Lean complains, the AI tightens, eventually Lean accepts — you end up with a statement like:

theorem deposit_then_redeem_loss
    {s s' s'' : State} {user : Addr} {a shares assets_back : ℕ} {P ε : ℚ}
    (hε_pos : 0 < ε)
    (h_price_cap : vaultTokenPrice s ≤ P)
    (h_a_min : (P + 1) / ε ≤ (a : ℚ))
    (hd : deposit s user a = some (s', shares))
    (hr : redeem s' user shares = some (s'', assets_back)) :
    (a : ℚ) - (assets_back : ℚ) < ε * (a : ℚ) := ...

The two side conditions: vaultTokenPrice s ≤ P (the vault-token price is below some cap P) and (P + 1) / ε ≤ a (the deposit is at least that much). The cap P is a parameter; the depositor threshold is determined by the cap and the tolerance.

The proof body is about 80 lines of Lean — floor-bound manipulations, the algebraic identity that makes the two floors' contributions cancel cleanly, a handful of nlinarith calls. I asked, I checked the statement, I ran lake build, it passed. I did not read the proof body.

Reading the bound against deployment reality

The interesting work starts now. We have a machine-checked statement: under vaultTokenPrice s ≤ P and (P + 1) / ε ≤ a, the round-trip loses strictly less than ε · a. The next question is whether these two conditions hold for the depositors we care about.

The deposit threshold

(P + 1) / ε ≤ a says the deposit has to be at least roughly P / ε asset units, plus a small additive term. For 18-decimal assets — the bulk of ERC-20s — a single human-scale token is 1018 raw units. Even at ε = 10-6 (one part per million) and a price of 103, the threshold is around 109 raw units — many orders of magnitude below any human-scale deposit. A frontend can additionally enforce a minimum-deposit check before forwarding the transaction. For 18-decimal deployments expecting human-scale users, this condition can be easily satisfied.

For lower-decimal assets — USDC, USDT, and a few others use 6 — the picture is different. The threshold's raw-unit count is the same, but the asset's per-token raw-unit count is now 106 rather than 1018, so the threshold occupies a larger fraction of a token, and how comfortably it holds depends on the expected price range. At a near-inception price (P ≈ 1) and a basis-point tolerance (ε = 10-4), the threshold is around 105 raw units — well under a dollar in USDC. As P climbs, or ε tightens, the bound becomes meaningfully tight, and whether it actually holds is worth checking against a specific deployment's operating range rather than asserted in general.

The price cap

The price cap is the harder one.

Under normal vault operation — yield accruing slowly, principal moving in via deposits and out via redeems — the price grows slowly and predictably. Whatever P the deployment commits to (call it the price at deployment plus a generous growth budget), the running price stays well below it.

The problem is that the price can also be moved by paths the vault doesn't fully control. In our simple model, the main such path is donation — assets transferred to the vault without going through deposit, landing on its books as profit. Real production vaults expose more: oracle inputs that can be skewed, strategy adapters that interact with external markets, or more generally any valuation of the underlying positions which can spike momentarily. Any of these can move the per-share price along channels the vault's user-facing entry points never see directly.

For any nontrivial vault, then, the price cap is a protocol invariant to defend rather than an assumption to take for granted. Whether the cap can be violated is the security question.

Mitigations enforce the cap as a protocol invariant

If you're designing a vault and the inflation surface is a real concern, the takeaway from the proved theorem is: your mitigation's job is to make vaultTokenPrice s ≤ P a protocol invariant. Different vault designs take different routes; one concrete approach worth examining is the per-period price-growth cap.

Morpho Vault V2 takes this route: the vault tracks an internal "fair price" that grows at most some configured amount per unit time, and the vault's externally exposed conversion rate is clipped to the fair price. A donation that spikes the underlying asset-to-share ratio doesn't propagate to depositors — they convert at the slower fair price — until the fair price's growth budget catches up. The donated value still accretes to existing shareholders over time, and the price depositors see remains protocol-enforced moment-to-moment — our theorem's P cap is a direct protocol invariant.

The reason this design exists, and the reason it has the shape it does, is exactly the bound our theorem proved. The mitigation is a constructive answer to "how do you enforce the side condition?"

What the workflow gives you

What we did in this post, the steps spelled out:

1. Asked the obvious thing. Lean refused.
2. Looked at the refusal. The counter-example was the donation-attack precondition.
3. Refined the spec with two informal constraints — "price bounded", "deposit large enough" — and let the AI propose the explicit bounds. Lean verified them.
4. Read the bounds against deployment reality. One condition is free in practice; the other is the live attack surface.
5. Looked at production-vault designs and saw the mitigation as a direct enforcer of the side condition.

The point worth highlighting: steps 2 through 5 are security analysis, not proof engineering. The proof process — the refusal, the side conditions, the bounds — does the analytical work. Lean's role isn't to bless something we already know; it's to force the questions worth asking.

The AI's role isn't to be trustworthy; it's to be a fast proposer of side conditions and proofs. Trust comes from the kernel. The only thing that needs human judgement is reading the proved statement back against the deployment context — "is this bound realistic? what can violate it?" — and that is exactly the kind of judgement formal methods are meant to amplify.

The Lean sources for this post — LossBound.lean, along with the Part 1 files it builds on — live in the simple-tokens-and-vaults/ directory.