TermMax Single-Segment Buy-XT Reserve Integrity

TermMax (by Term Structure) is a fixed-rate lending protocol. Users trade between debt tokens and XT (extended tokens) through on-chain order books, where pricing is governed by a bonding curve parameterized by liquidity, a time-dependent interest factor, and configurable fee ratios.

The TermMaxOrderV2 contract's swapExactTokenToToken function is the entry point for exact-input swaps. This case study isolates the debtToken → XT path on a single curve segment: the path a user takes when borrowing against one active curve cut. The proof tracks the modeled call stack from the swap entry point down through the curve library and confirms that the reserve update matches the curve computation exactly inside that model.

Why this matters

The virtualXtReserve is the accounting variable that tracks how much XT liquidity remains in the order. Every subsequent swap prices off this value. If the reserve update diverges from the curve computation, even by one wei, all future swaps on that order will price off an incorrect base, and the order's implied interest rate will drift from its configured curve.

How this was modeled

The benchmark extracts eight Solidity functions across three source files (TermMaxOrderV2.sol, TermMaxCurve.sol, MathLib.sol) into a single Verity contract block. Each Solidity helper is kept as a separate Verity function to preserve the call structure of the original code.

TermMax's curve can have multiple cuts, each with its own liquidity parameters. This model covers the case where there is exactly one active cut at index 0 and that cut has xtReserve = 0. That means the Solidity loop that iterates over cuts runs exactly once, and if the swap needs more liquidity than that single cut provides, the model reverts with InsufficientLiquidity().

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

Proof status

This case has one headline theorem in Lean 4. The corresponding proof file in the Verity benchmark repository is sorry-free, so the claim below is accepted by Lean's kernel rather than by informal review.

View specs in LeanView proofs in Lean

Assumptions

The proof uses zero axioms. The five hypotheses below are preconditions for successful execution. Each one mirrors an explicit check or implicit requirement in the Solidity source.

• hNonZeroInputdebtTokenAmtIn ≠ 0

  swapExactTokenToToken gates the body with if (tokenAmtIn != 0)

  The Solidity entry point skips the swap body when the input is zero. The model covers the non-trivial execution path.

• hLockOpennonReentrancyLock = 0

  OpenZeppelin ReentrancyGuard slot

  The function uses a nonReentrant modifier. The lock must be open (not already held by a prior call) for the swap to execute.

• hVXtNonZeroplusInt256(virtualXtReserve, cutOffset) ≠ 0

  calcIntervalProps divides by vXtReserve

  The curve formula divides the liquidity squared by the virtual XT reserve (after applying the curve offset). A zero virtual reserve would cause a division-by-zero revert.

• hNoCrosscurveOutput ≤ virtualXtReserve

  cutsReverseIter single-cut liquidity check

  The computed XT output cannot exceed the available reserve. In the Solidity source, exceeding this triggers revert InsufficientLiquidity().

• hMinOuttokenAmtOut + debtTokenAmtIn ≥ minTokenOut

  _buyToken slippage check

  The net output (XT received plus debt tokens returned) must meet the caller's minimum. In the Solidity source, failing this triggers revert UnexpectedAmount(minTokenOut, netOut).

View specs in LeanView proofs in Lean

Learn more

Upstream Solidity contracts: TermMaxOrderV2.sol, TermMaxCurve.sol, MathLib.sol.

Full case directory in the Verity benchmark repository.

Verity benchmark repository, which contains the formal specification, machine-checked proofs, and the broader benchmark suite this case belongs to.

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