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.

Assumptions

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 success pathNon-expired mint with checked arithmetic success
Benchmark/Cases/Pendle/PySupplyPairing/Proofs.lean
We only prove what happens after a mint is allowed to succeed: 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 they do mean failed or reverting mints are not part of this theorem.
pre-expiry redeem success pathSuccessful redeem before maturity
Benchmark/Cases/Pendle/PySupplyPairing/Proofs.lean
We only prove the pre-expiry redeem branch after the call is allowed to succeed: 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.
observed accounting stateOnly PT/YT supplies and balances are claimed
Benchmark/Cases/Pendle/PySupplyPairing/Specs.lean
The proof watches 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. The result is precise but intentionally narrow.
paired PT trust boundaryPT mint and burn are inlined through onlyYT
contracts/core/YieldContracts/PendlePrincipalToken.sol
The model treats the paired PT contract as part of the same accounting system because PT mint and burn can only be called 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

1inch XYCSwap Curve Safety

Formally verified fee-adjusted constant-product curve safety for 1inch Aqua XYCSwap.

for

StarkGate Bridge Escrow Lower Bound

Formally verified escrow accounting for the StarkGate L1 token bridge deposit, withdrawal, and reclaim paths.

for

KyberSwap Partial-Fill Price Floor

Formally verified helper-level partial-fill price-floor guard for MetaAggregationRouterV2.

for