Alchemix V3 Earmark Conservation

Alchemix is a self-repaying lending protocol. A user deposits a yield-bearing token (MYT) as collateral and mints a synthetic debt token (alAsset). The yield from that collateral flows to the Transmuter, which uses it to pay down the user's debt automatically.

Each position keeps two numbers:

• debt: how much alAsset the user owes the protocol.
• earmarked: how much of that debt has already been booked for repayment by incoming yield. The user's outstanding balance is debt - earmarked; as earmarked rises, the user owes less.

cumulativeEarmarked is the global sum the Transmuter reads when it pulls collateral. The conservation invariant says it always equals the per-account picture, even though the protocol never iterates accounts.

Why this matters

If the per-account and the global picture diverged, redemption would either over-debit user collateral (the protocol thinks more debt is earmarked than actually is) or short-pay the Transmuter (the global lags behind real per-account claims). Either failure breaks the synthetic peg.

The earmarking system updates the global immediately and the per-account state lazily. The conservation invariant is what makes the lazy update safe: every consumer that reads an account's current earmarked debt sees a value that, summed across all accounts, matches the global. Alchemix's lead developer flagged the lazy-lag pattern in the source at line 1014 (“Global can lag local by rounding”); the proof shows the lag is harmless under the invariant.

How this was modeled / proven

Function names, storage slot names, and field names match the Solidity source verbatim, including leading underscores on private members. Every block in every modeled function carries an inline source-line annotation (-- src: AlchemistV3.sol:Lxxxx-Lyyyy) so a reviewer can read the Lean and the Solidity side by side.

For each of the five operations, the proof reads the post-state storage slots off the contract body via a dedicated slot-write lemma (the same pattern Lido VaulthubLocked uses), then chains through atomic Q128 algebra and the projection formula to land the conservation equality. The hardest steps, _earmark and redeem, both rely on a per-account survival-ratio scaling lemma derived from the slot-write rule for _redemptionWeight and _earmarkWeight.

The model deviates from the deployed contract in six places. Each is a deliberate scope choice; each weakens the proven statement compared to a guarantee about deployed bytecode. They are spelled out below rather than tucked into a footnote.

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

Produced as part of the Verity benchmark, an open database of formally specified contract properties.

Proof status

The five core preservation theorems are fully proven from operational semantics. After a review pass, three of the hypotheses originally surfaced on those theorems were discharged: two via composition (call-site theorems) and one via a strengthened invariant (the line-1306 clamp). All in all, the file proves the user-facing theorems listed below plus their supporting lemmas, with no axioms, no sorry, no admit.

View contract modelView specs in LeanView proofs in Lean

Assumptions / hypotheses

Three of the original six hypotheses were proved and removed. These are the three that remain.

• Q128 idealizationfloor-rounded Q128 ops behave like exact rationals

  Modeling assumption (irreducible at this level)

  The contract uses floor-rounded Q128.128 math. The proof treats it like exact arithmetic, so it ignores tiny per-step rounding drift and proves the design-level conservation rule instead.
  Removing this assumption would require a different theorem: a bounded-rounding-error result for ONE_Q128.

• Weight snapshots non-zero (model artifact)lastAccruedEarmarkWeight and lastAccruedRedemptionWeight are non-zero where required

  Model artifact, not present in deployed Solidity

  This one is a model artifact. We found concrete counterexamples showing that the relevant preservation statements are false in the current model if the weight snapshots needed by that operation are allowed to be zero.
  These are counterexamples to dropping the hypothesis, not counterexamples to the theorem as stated. The real contract advances the epoch and resets the index after a full wipe. Our model flattens that epoch-and-index structure into one weight, so zero snapshots must stay excluded until epochs are modeled directly.

• Projected debt conservation (sister invariant)sumProjectedDebt s ids = totalDebt s

  Sister of the main invariant; preservation is a follow-up case

  The natural sister of the earmark-conservation invariant: where sumProjectedEarmarked = cumulativeEarmarked aggregates per-id projected earmarked debt, this aggregates per-id projected total debt and equates it to the global totalDebt. The bridge H6_from_projectedDebt_conservation proves the original Q128-projected bridging identity (that Σ unearmarkedRemaining × redemptionSurvivalRatio equals totalDebt − cumulativeEarmarked) follows from this sister + the main invariant + the line-1306 sister.
  It should be provable with the same proof pattern we used here, but only after modeling the debt-changing operations this case left out (_addDebt, _resetDebt, constructor setup). That is a follow-up case, so the sister itself remains a scope cut for now.

View specs in LeanView proofs in Lean

Learn more

Upstream Solidity contract: AlchemistV3.sol.

Full case directory in the Verity benchmark repository.

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