Lido V3 Vault Solvency Guarantee

\texttt{locked}

VaultHub._locked()
ETH that cannot be withdrawn from the vault

\;\cdot\;(

\texttt{BP}

TOTAL_BASIS_POINTS
= 10,000

-

\texttt{RR}

reserveRatioBP
The vault's reserve ratio (e.g. 3000 = 30%)

)\;\geq\;

\texttt{liability}

liabilityShares → ETH
stETH owed to depositors, via getPooledEthBySharesRoundUp

\;\cdot\;

\texttt{BP}

TOTAL_BASIS_POINTS
= 10,000

stETH can only be minted if the vault's total locked ETH exceeds its total minted stETH.

View Lean

Lido V3 introduced StakingVaults, which allow stETH to be minted against ETH held in isolated vaults. The VaultHub contract enforces overcollateralization: part of the vault's value must remain locked, covering the outstanding stETH liability plus a reserve buffer.

View technical design

Why It Matters

VaultHub only allows minting when totalValue ≥ _locked(). If _locked() didn't satisfy this inequality (due to an overflow, rounding error, or edge case), a vault could pass that check while locking less ETH than the stETH minted against it.

How This Was Modeled and Proven

The _locked() function uses non-linear uint256 arithmetic (multiplications, ceiling division, max()) that standard verification tools cannot reason about. This property was flagged as unproven (finding F-01) in Certora's formal verification report.

The contract logic was modeled in Verity, a framework for expressing smart contract logic in a way that allows mathematical proofs. The theorem was given to AI agents as a benchmark task. A proof was generated by GPT 5.4 for ~$45 (3M tokens) and is provided as reference.

Scope

This proof covers the formula: for any inputs, _locked() never underestimates how much ETH should be locked.

It does not cover whether the vault actually holds that much ETH. That is enforced at runtime: VaultHub checks totalValue ≥ locked at mint time. If a validator is slashed between oracle reports, the vault may temporarily be under-collateralized. The contract handles this through forced validator exits (EIP-7002) and permissionless forceRebalance().

Proof artifacts

Contract.lean contains the Verity model of the contract logic.
Specs.lean defines the solvency specification.
Proofs.lean contains the reference proof generated by GPT 5.4.
The proof is checked by Lean 4's kernel, a small program that accepts or rejects proofs deterministically. If the proof were wrong, it would not compile.
Note: the current proof is neither optimized for performance nor elegance. It may be replaced by a cleaner version as the benchmark is run with more models.

Function	Theorem	Status
_locked()	locked_funds_solvency	Proven

Verify it yourself

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Lido.VaulthubLocked.Proofs

If the build succeeds, the proof is correct. Source repository

Hypotheses

The proof uses zero axioms. The theorem requires these hypotheses, which encode assumptions about valid protocol states:

max liability shares cover current shares
Certora P-VH-04, verified
The proof assumes maxLiabilityShares ≥ liabilityShares. VaultHub's minting and reporting logic maintain this core invariant. _locked() is computed from maxLiabilityShares (worst-case), not current shares. Without this, the locked amount wouldn't cover the real liability.
reserve ratio is above zero
Certora P-VH-03, verified
The proof assumes reserveRatioBP > 0, enforced by connectVault(). A zero reserve ratio would make the overcollateralization trivial, but the proof structure requires it for the algebra to work out.
reserve ratio is below 100%
Certora P-VH-03, verified
The proof assumes reserveRatioBP < 10000. This is critical. If reserveRatioBP ≥ 10000, the subtraction BP − RR underflows in uint256, producing a nonsensical denominator. On-chain, Solidity 0.8+ would revert; in the Lean model, it wraps.
Lido total shares are non-zero
Lido base assumption
The proof assumes totalShares > 0. Share-to-ETH conversion needs it: if totalShares = 0, ceilDiv divides by zero and underestimates the liability. In practice, it is always true after Lido's bootstrap deposit.
total pooled ether is non-zero
Lido base assumption
The specification assumes totalPooledEther > 0. The proof does not use it (prefixed with _ in Lean). It is included for specification completeness: a pool with shares but no ether would be nonsensical.

Five additional hNoOverflow hypotheses guard that intermediate uint256 products stay below 2²⁵⁶. With Lido's total staked ETH at ~30M ETH (~2⁸⁵ wei), products reach ~2¹⁷⁰, far below the 2²⁵⁶ limit.

View in Lean Certora report

Learn More

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

More research

Kuru V2 Shared Withdrawal Budget

A successful batch of ordinary withdrawals in the model reduces the shared budget by exactly its recorded payout value, across all accounts and tokens.

for

Dromos MetaDEX Allocation Conservation

In the root-ledger model, chain allocations sum to committed voting power.

for

KPK Shares Settlement Accounting

A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.

for