Lido V3 Vault Solvency Guarantee

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 this 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.

What this invariant covers

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().

How this was 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.

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.

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. Source repository

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.

Hypotheses

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

  • hMaxLSmaxLiabilityShares ≥ liabilityShares

    Certora P-VH-04, verified

    Core invariant maintained by VaultHub's minting and reporting logic. _locked() is computed from maxLiabilityShares (worst-case), not current shares. Without this, the locked amount wouldn't cover the real liability.

  • hRR_posreserveRatioBP > 0

    Certora P-VH-03, verified

    Enforced by connectVault(). A zero reserve ratio would make the overcollateralization trivial but the proof structure requires it for the algebra to work out.

  • hRR_ltreserveRatioBP < 10000

    Certora P-VH-03, verified

    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.

  • hTStotalShares > 0

    Lido base assumption

    Required for share-to-ETH conversion. If totalShares = 0, ceilDiv divides by zero and underestimates the liability. In practice, always true after Lido's bootstrap deposit.

  • hTPEtotalPooledEther > 0

    Lido base assumption

    Unused by the proof (prefixed with _ in Lean). 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 2256. With Lido's total staked ETH at ~30M ETH (~285 wei), products reach ~2170, far below the 2256 limit.

View in LeanCertora report

Learn more

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

More research

Verity Verified Compiler

A Formally Verified Smart Contract Compiler in Lean 4.

Publication

Verity Benchmark

A benchmark suite for AI-driven formal proof generation on real smart contracts.

Publication

What is a formal proof?

A short explanation for non-specialists.

Explainer