Pendle PY Supply Pairing

mintPYmintPY
The modeled successful mint path.:YT supply afterYT supply after
The modeled Yield Token total supply after the call succeeds.=YT supply beforeYT supply before
The modeled Yield Token total supply before the call.+mint amountmint amount
Specs.lean calls this mintPYAmountOf(s): the PY amount computed from the deposited SY.andPT supply afterPT supply after
The modeled Principal Token total supply after the call succeeds.=PT supply beforePT supply before
The modeled Principal Token total supply before the call.+mint amountmint amount
The same amount is applied to the PT side and the YT side.

redeemPY before expiryredeemPY before expiry
The modeled successful redeem path before maturity.:YT supply afterYT supply after
The modeled Yield Token total supply after the call succeeds.=YT supply beforeYT supply before
The modeled Yield Token total supply before the call.-redeem amountredeem amount
Specs.lean calls this redeemPYAmountOf(s): the smaller of the contract-held PT and YT balances.andPT supply afterPT supply after
The modeled Principal Token total supply after the call succeeds.=PT supply beforePT supply before
The modeled Principal Token total supply before the call.-redeem amountredeem amount
The same amount is applied to the PT side and the YT side.

Every successful modeled mint creates the same amount of PT and YT, and every successful modeled pre-expiry redeem burns the same amount from both.

View Lean

Pendle is a yield-trading protocol that splits a yield-bearing asset into a Principal Token and a Yield Token. This case verifies the PT/YT accounting slice in Pendle V2: successful modeled mintPY creates the same amount of PT and YT, and successful modeled pre-expiry redeemPY burns the same amount from both.

Why It Matters

PT and YT are the two halves of the same standardized yield position. If a mint could create more of one side than the other, or a pre-expiry redeem could burn only one side, users would hold mismatched claims on principal and future yield.

The value at risk is the accounting backing Pendle's split yield tokens. Markets can price PT and YT separately, but the tokenization contract must keep their supply movement paired on the successful modeled mintPY and pre-expiry redeemPY paths.

How This Was Modeled and Proven

We modeled the Pendle V2 PY accounting surface around mintPY, _mintPY, redeemPY, and _redeemPY. The paired PT contract is inlined because PT mint and burn entrypoints are gated by onlyYT.

The readable specifications are in Specs.lean. The source-shaped Verity model is in Contract.lean, and the no-sorry reference proofs are in Proofs.lean.

Scope

Covered: single-call mintPY with PT/YT receivers, the single computed amountPYOut, YT and PT supply increments, receiver balance increments, successful pre-expiry redeemPY, the min(PT,YT) redeem amount, and equal PT/YT burns from contract-held balances and total supplies.

Out of scope: post-expiry redeem, reward and interest hooks, SY token transfer behavior, SY reserve updates, redeem-side PY-index storage writes, return-value correctness for amountSyOut, access-control surfaces outside the paired PT trust boundary, events, allowances, and multi-receiver loops. They are outside this proof claim; the proved equalities apply only to the modeled PT/YT accounting state described above.

Proof artifacts

Contract.lean contains the Pendle PY accounting model and simplifications used for this case.
Specs.lean defines ytSupply, ptSupply, mintPYAmountOf, redeemPYAmountOf, and supplyPairing.
Proofs.lean proves exact amount updates first, then derives supply-pairing preservation.
Benchmark case files contain the model, specs, proofs, manifests, and generated task files.

Function	Theorem	Status
mintPY	mint_py_mints_equal_amount	Proven
mintPY	mint_py_preserves_supply_pairing	Proven
redeemPY before expiry	redeem_py_pre_expiry_burns_equal_amount	Proven
redeemPY before expiry	redeem_py_pre_expiry_preserves_supply_pairing	Proven

Verify it yourself

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout fricoben/pendle-invariant-proofs
lake build Benchmark.Cases.Pendle.PySupplyPairing.Proofs

If the build succeeds, Lean has checked the Pendle PY supply-pairing reference proofs for the modeled accounting slice.

Hypotheses

These are the boundaries of the proof. In plain terms: we prove the successful mint and pre-expiry redeem accounting paths, not every possible revert, transfer, reward, or post-expiry behavior.

mint succeeds before expiry
Benchmark/Cases/Pendle/PySupplyPairing/Proofs.lean
We only prove a non-expired mint whose checked arithmetic succeeds: the market has enough SY, the PT and YT receivers are valid, and the arithmetic fits in the expected integer ranges. Strength: moderate. These are mostly Solidity success checks, but failed or reverting mints are not part of this theorem.
redeem succeeds before maturity
Benchmark/Cases/Pendle/PySupplyPairing/Proofs.lean
We only prove a successful redeem before maturity: the contract has enough PT and YT to burn, the current index is nonzero, and the arithmetic does not overflow. Strength: strong. This deliberately excludes post-expiry redeem and failed redeem attempts.
only PT and YT supplies and balances checked
Benchmark/Cases/Pendle/PySupplyPairing/Specs.lean
The proof claims only the PT and YT supplies and the balances involved in the modeled call. It does not claim that amountSyOut, SY token transfers, SY reserves, reward hooks, or the redeem-side PY-index write are correct. Strength: strong scope limit, not a hidden axiom.
only the paired YT can mint or burn PT
contracts/core/YieldContracts/PendlePrincipalToken.sol
The model inlines PT mint and burn and treats the paired PT contract as part of the same accounting system. This relies on PT mint and burn being callable only by the paired YT contract through onlyYT. Strength: reasonable if that access-control boundary holds. If the paired YT relationship were wrong, this proof would not cover that separate access-control bug.

Learn More

Kuru V2 Shared Withdrawal Budget

After any batch of ordinary withdrawals, the withdrawal budget drops by exactly what was paid out, whichever accounts or tokens were used.

for

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