Cork Protocol Pool Solvency

Cork Protocol is a risk layer for DeFi assets like stablecoins, LSTs, and yield-bearing tokens. Each Cork pool pairs a collateral asset (CA) with a reference asset (REF), an existing on-chain token (e.g. a stablecoin or LST) whose peg the pool protects against. Depositors provide CA and receive two tokens: a swap token (cST) granting the right to exchange REF for CA before expiry, and a principal token (cPT) representing the depositor's claim on whatever collateral remains after all swaps are settled. In the happy path (no depeg), cPT holders redeem their full deposit; in a depeg, cST holders exercise the swap to claim collateral, and cPT holders absorb the loss.

unwindExerciseOther lets a user reverse a swap position. The user provides reference assets; the pool computes how many cST shares to release and how much additional collateral to lock. Certora's formal verification of Cork Phoenix defined a solvency invariant called P-02: after any state-changing operation, locked collateral must still cover all outstanding cST claims. They verified P-02 for every other CorkPool function but timed out on this one. This proof closes that gap.

Why this matters

An unwind reverses a swap position: the user sends reference assets back, and the pool returns cST shares to its own balance (reducing outstanding claims) while locking additional collateral. If solvency broke on this code path, the collateral locked could fall short of the remaining outstanding cST, meaning holders who bought depeg protection could find the pool unable to pay out when they exercise their swap.

The function chains three rounding operations across different decimal scales. The proof covers the full parameter space: arbitrary exchange rates and arbitrary decimal combinations.

How this was modeled / proven

The model is built directly from the Solidity source code of Cork Phoenix v1.1.2 (commit 40d9b173c4b), not from Certora's specification. The call path crosses four Solidity files: PoolLib.sol, MathHelper.sol, TransferHelper.sol, and CorkPoolManager.sol. These are inlined into a single Lean file (Contract.lean) since the proof only needs the arithmetic, not the contract boundaries.

When Cork processes an unwind, it computes two things: how many shares to release (using floor rounding, which rounds down) and how much collateral to lock (using ceiling rounding, which rounds up). Both roundings favor the pool: it locks slightly more collateral than strictly needed and releases slightly fewer shares than strictly needed.

The core lemma double_ceilDiv_sandwich proves that this asymmetry is enough to guarantee solvency for any exchange rate and any decimal combination. It says: the ceiling-rounded collateral always covers the floor-rounded shares.

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

Proof status

The Cork case has one main theorem and two supporting results. All are fully proven with no axioms and no sorry.

View contract modelView specs in LeanView proofs in Lean

Assumptions / hypotheses

The proof uses zero axioms. The hypotheses below are preconditions on the contract state before the call. Each mirrors a constraint enforced by Cork's pool creation or by ERC-20 accounting.

• hSolvencyBeforesolvency holds before the call

  P-02 invariant (inductive step)

  The theorem is an inductive step: if solvency held before unwindExerciseOther, it still holds after. The base case is pool creation, where both collateral and outstanding shares start at zero.

• hColScale, hRefScale, hSwapRate, hRefOutcolScaleUp, refScaleUp, swapRate, referenceAssetsOut > 0

  Pool creation + oracle + non-trivial call

  All scale factors, the exchange rate, and the unwind amount must be positive. Scale factors are 10^{(18 - decimals)} (positive for any token with ≤ 18 decimals); the rate comes from the oracle; a zero-amount unwind is a no-op. In Lean's natural number type there is no “unsigned nonzero”, so these are stated individually as > 0.

• hNoOvf1 .. hNoOvf5intermediate uint256 arithmetic stays in range

  Overflow preconditions

  Five hypotheses guard that products and sums during the unwind do not exceed 2²⁵⁶. In practice these hold whenever token supplies and rates stay below ~2¹²⁸ (well within any realistic ERC-20 supply). They could be derived from a single weaker bound on the inputs, but we state them per-operation to match the Solidity exactly.

• hSupplyGeBalswapTotalSupply ≥ swapBalanceOfPool

  ERC-20 invariant

  Total supply of swap shares is at least the pool's own balance. This means outstanding shares (supply minus pool balance) is non-negative. Without this, the right side of the solvency inequality would underflow.

View specs in LeanView proofs in Lean

How this relates to Certora's audit

Certora verified P-02 solvency across 13 CorkPool functions using bounded model checking (SMT solver). Their prover timed out on unwindExerciseOther because the chained rounding produces non-linear arithmetic the solver cannot discharge within its search depth.

We took a different route: manual translation of the arithmetic into Lean 4, then a step-by-step proof that the ceiling/floor asymmetry preserves solvency for all inputs. No search bound, no timeout: the proof is checked by Lean's kernel.

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

Learn more

Upstream Solidity contracts: PoolLib.sol, MathHelper.sol, TransferHelper.sol, CorkPoolManager.sol.

Full case directory in the Verity benchmark repository.

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