TermMax Single-Segment Buy-XT Reserve Integrity

∀ s amountIn, virtualXtReserve′ = virtualXtReserve − singleSegmentBuyXtTokenAmtOut(daysToMaturity, virtualXtReserve, amountIn, feeRatio, liqSquare, offset)

When a user swaps debt tokens for XT, the reserve goes down by exactly what the pricing curve says it should.

s: the contract state (storage) at the time of the swap.
virtualXtReserve / virtualXtReserve′: XT reserve before / after.
singleSegmentBuyXtTokenAmtOut(...): how many XT the curve says the user gets. Modeled in Lean from the Solidity source.

View Lean

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.

What this covers

The modeled call stack follows the debtToken → XT branch of swapExactTokenToToken through every internal helper down to the curve computation:

swapExactTokenToToken → _swapAndUpdateReserves → _buyXt → _buyToken → _buyXtStep → TermMaxCurve.buyXt → cutsReverseIter → calcIntervalProps
MathLib.plusInt256 (signed-integer addition on uint256) is also modeled.
The nonReentrant modifier is included. The reentrancy lock is modeled as a separate storage slot.

Out of scope: other token-pair branches of swapExactTokenToToken, access control (onlyBorrowingIsAllowed), token transfers, rebalancing, events, and multi-cut curve iteration.

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

Simplifications

The model preserves the reserve-update logic for this execution path, with deliberate simplifications. The full details are documented in Contract.lean.

Single active curve cut only. The Solidity contract supports multiple curve cuts and iterates over them. This model covers exactly one active cut at index 0, with cuts[0].xtReserve = 0. Multi-cut swaps are not covered.
One swap direction. Only the debtToken → XT path is modeled. The other token-pair branches of swapExactTokenToToken are not included.
Access control omitted. The onlyBorrowingIsAllowed modifier does not touch the reserve, so it is left out without weakening the guarantee.
Post-swap side effects omitted. Token transfers, rebalancing, and events all happen after the reserve write and are guarded by nonReentrant, so they cannot affect the proven property.
Checked arithmetic abstracted. Solidity 0.8 checked arithmetic in plusInt256 is modeled with Verity's unsigned arithmetic operations. This proof verifies the reserve update inside that arithmetic model, not Solidity's overflow-revert behavior.

A few cosmetic differences also exist: struct fields are passed as individual parameters instead of structs, and library functions are inlined as helpers. These change the shape of the code but not its logic.

Verify it yourself

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

If the build succeeds, the proofs are correct. Source repository

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.

Guarantee	Status
virtualXtReserve′ = virtualXtReserve − curveOutput	proven

View specs in Lean View proofs in Lean

Hypotheses

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.

swap input is non-zero
swapExactTokenToToken gates the body with if (tokenAmtIn != 0)
The debt token input is non-zero: debtTokenAmtIn ≠ 0. The Solidity entry point skips the swap body when the input is zero. The model covers the non-trivial execution path.
reentrancy lock is not held
OpenZeppelin ReentrancyGuard slot
The OpenZeppelin reentrancy lock must be open, nonReentrancyLock = 0, not already held by a prior call. The function uses a nonReentrant modifier, so the swap executes only when the lock is open.
virtual XT reserve is non-zero
calcIntervalProps divides by vXtReserve
The virtual XT reserve after the curve offset is non-zero: plusInt256(virtualXtReserve, cutOffset) ≠ 0. The curve formula divides the liquidity squared by this value, so a zero reserve would cause a division-by-zero revert.
output fits within the XT reserve
cutsReverseIter single-cut liquidity check
The computed XT output cannot exceed the available reserve: curveOutput ≤ virtualXtReserve. In the Solidity source, exceeding this triggers revert InsufficientLiquidity().
output meets the caller's minimum
_buyToken slippage check
The net output, XT received plus debt tokens returned, must meet the caller's minimum: tokenAmtOut + debtTokenAmtIn ≥ minTokenOut. In the Solidity source, failing this triggers revert UnexpectedAmount(minTokenOut, netOut).

View specs in Lean View 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.

More research

Dromos MetaDEX Allocation Conservation

In the root-ledger model, chain allocations sum to committed voting power.

for

KPK Shares Settlement Accounting

A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.

for

Railnet Queue Nominal Conservation

No matter how many partial redemptions happen, or in what order, the queue never records paying out more than it recorded receiving.

for