Wildcat Borrow Liquidity Invariant

Wildcat V2 is a credit-market protocol. A Wildcat market is a lending market where lenders deposit assets, the borrower can draw down liquidity, and the contract still needs to preserve enough assets to satisfy lender obligations and protocol fees.

The relevant guard lives on the successful path of borrow(uint256 amount). Before the borrow is allowed, Wildcat computes a liquidity requirement from the current market state and only lets the borrower remove assets that remain above that threshold.

Why this matters

The failure mode here is economic, not cosmetic. If the borrow guard overestimates borrowable assets or underestimates required liquidity, the borrower can pull funds out of the market that should have remained available for lender withdrawals or protocol fees.

A borrow that succeeds but leaves the market below the required liquidity threshold would mean the reserve logic failed exactly where it matters: on the path that actually transfers assets out of the contract.

How this was modeled / proven

The model isolates the successful borrow path from Wildcat V2 tag v2.0.0 at commit a70f297fbd1b1ab597e0e9a3458a2d13a34b4657. In the benchmark, _getUpdatedState() is compressed to a precomputed protocol-fee delta applied before the borrow check, and the pending-withdrawal and normalized-unclaimed-withdrawal fields are treated as already current borrow-check inputs.

totalAssets is modeled as a trusted storage mirror of the contract's asset balance. Sanctions, hooks, and the final transfer remain structurally visible in the model but are treated as trusted boundaries. Wildcat's packed state is flattened into ordinary storage slots so the proof can reason directly about the semantic fields instead of packed-slot encoding details.

The full safety argument is proved in Lean 4 with no axioms. Concretely, the main theorem shows that if amount <= borrowableAssetsAfterUpdate, then subtracting amount from totalAssets still leaves at least the required liquidity. The mechanical post-state write characterization of the successful borrow path is also fully proven.

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

Proof status

The Wildcat case has one main theorem: positive_borrow_preserves_required_liquidity. The case builds successfully and all theorems are fully proven with no remaining axioms.

View contract modelView specs in LeanView proofs in Lean

Assumptions / hypotheses

• borrowerFlaggedOf s = 0borrower is not sanctioned

  Trusted sanctions boundary

  The case assumes the borrower passes Wildcat's sanctions check. Sanctions implementation details are outside this benchmark slice.

• isClosedOf s = 0market is not closed

  borrow precondition

  The successful-path theorem only reasons about states where the market is open and borrowing is still allowed.

• hookAllowsBorrowOf s != 0borrow hook succeeds

  Trusted hook boundary

  The borrow hook is an external call to an operator-configured contract whose behavior is unknown to the model. The proof assumes it returns successfully on the path being analyzed.

• scaledPendingWithdrawalsOf s ≤ scaledTotalSupplyOf spending withdrawals do not exceed total supply

  outstandingSupply underflow guard

  This is the basic accounting side condition needed to make the outstanding-supply subtraction meaningful on the modeled path.

• uint256 range conditionschecked fee and liquidity arithmetic stays in range

  compressed overflow preconditions

  The checked uint256 intermediate sums and products used in fee accrual and liquidity arithmetic are assumed to stay within range. This includes the fee update, reserve product, normalization product, and the subsequent liquidity sums.

• amount ≤ borrowableAssetsAfterUpdate sborrow amount respects the updated guard

  main arithmetic precondition

  The theorem is about successful positive borrows. The borrow amount must be at most the borrowable assets computed from the updated state.

• totalAssetsOftrusted balance mirror for totalAssets

  modeling assumption

  The model treats totalAssets as a trusted storage mirror of the market's actual ERC20 balance instead of re-modeling asset.balanceOf(address(this)).

• _getUpdatedState() compressionfee update is precomputed

  modeling assumption

  Instead of re-running Wildcat's full state-update pipeline, the model takes the protocol-fee increase as a given input and treats pending and unclaimed withdrawal balances as already up to date at borrow time.

View specs in LeanView proofs in Lean

Learn more

Upstream Wildcat V2 source, the production borrow path modeled in this case.

Wildcat benchmark case, plus the contract model, specs and proofs.

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