Lido V3 Vault Solvency Guarantee
A vault is required to lock more ETH than the stETH minted against it.
Lido V3 introduced StakingVaults, which allow stETH to be minted against ETH held in isolated vaults and used for validator operations. The VaultHub contract enforces overcollateralization by requiring that part of the vault's value remains locked, covering both the outstanding liability and an additional reserve providing a buffer against losses such as slashing.
Why this matters
- Vault-minted stETH is always redeemable for ETH at 1:1, the core invariant of the Lido protocol
- Losses in one vault never spill over to stETH holders or other vaults
- The reserve margin creates a buffer before a vault becomes unhealthy and is subject to forced rebalancing
Why this is difficult
The _locked() function uses non-linear uint256 arithmetic: multiplications, ceiling division via Math256.ceilDiv, and a max() over the reserve and a minimum floor, all within 2256 bounds.
This property was flagged as unproven (finding F-01) in Certora's formal verification report. Standard SMT-based tools typically cannot handle non-linear integer reasoning with division.
Why you can trust this
The proof was generated automatically and checked by the Lean 4 theorem prover. Every logical step is verified deterministically by Lean's kernel, a small, well-audited program that accepts or rejects proofs.
If the proof were incorrect, it would not compile.
You do not need to trust the proof generator.
Verify it yourself
git clone https://github.com/lfglabs-dev/verity-benchmark cd verity-benchmark ./scripts/run_default_agent.sh lido/vaulthub_locked/locked_funds_solvency
If the build succeeds, the proof is correct. No other check is needed.
Trust model
To trust this result, you only need to trust:
- The Lean proof checker (open source, widely used)
- The stated assumptions (listed below)
You do not need to trust:
- The AI that generated the proof
- The authors of this page
Assumptions
The proof holds under explicit preconditions, each enforced by VaultHub's connection and minting logic.
- Max liability bound:
maxLiabilityShares ≥ liabilityShares. Enforced by_increaseLiabilityon every mint. The actual shares minted never exceed the per-oracle-period maximum. - Reserve ratio bounds:
0 < reserveRatioBP < 10000. Set at vault connection and validated by_connectVault. A 30% ratio means 1.43 ETH must be locked per stETH minted. - Positive protocol state:
totalShares > 0andtotalPooledEther > 0. Required for share-to-ETH conversion. Always true while Lido has active deposits. - No arithmetic overflow: intermediate products like
liabilityShares × totalPooledEtherandliability × reserveRatioBPstay withinuint256.
What was proven
Five theorems, from the core solvency result to supporting lemmas:
- locked_funds_solvency: the main result. The output of
_locked(), scaled by the reserve-ratio complement, always exceeds the stETH liability scaled by total basis points. - ceildiv_sandwich: rounding up never loses value.
ceilDiv(x, d) · d ≥ x. Key arithmetic fact used in the main proof. - shares_conversion_monotone: if vault A holds more shares than vault B, it also owes more ETH.
getPooledEthBySharesRoundUppreserves ordering. - max_liability_shares_bound: the vault's current
liabilitySharesnever exceedsmaxLiabilityShares, as maintained by VaultHub's minting and reporting logic. - reserve_ratio_bounds: the
reserveRatioBPis always between 1 and 9999, enforced at vault connection.
Learn more
What is a formal proof? A short explanation for non-specialists.