This report represents work and conclusions based on Term Labs using Certora’s Prover tool to formally verify security properties of Term's smart contracts. Term finalized formal verification of the protocol's smart contracts using Certora's Prover solutions with guidance and technical support provided by the Certora team. The work was undertaken from Dec. 1, 2023 to Mar. 23, 2024. Some of these tests were verified using beta and staging versions of Certora's Prover, which are scheduled to be deployed to their production service in the near future. The latest commit that was reviewed and ran through the Certora Prover was 831292726cdc22e9d4d2953d59051fa00fbd4f72.
The scope of this verification includes all Term Servicer contracts within Term Protocol. This includes the following.
TermRepoToken.sol
TermRepoLocker.sol
TermRepoServicer.sol
TermRepoCollateralManager.sol
TermRepoRolloverManager.sol
Auction Contracts within Term Protocol were partially verified, with coverage on all functions except for those related to auction clearing, whose loop complexity is too elevated for formal verification. Runtime Verification was previously engaged to focus specifically on auditing and manually verifying this small but critical part of the codebase, see here. Contracts with partial coverage include:
TermAuction.sol
TermAuctionBidLocker.sol
TermAuctionOfferLocker.sol
The Certora Prover proved the implementation of the protocol is correct with respect to formal specifications written by the Term Labs team.
List of Main Issues Discovered
Severity: Low
Issue:
Zero Max Repayment Allowed in burnCollapseExposure
Description:
In the case where a borrower (i) has an outstanding repurchase exposure that (ii) has also been submitted as an open rollover such that (iii) the amount they are able to collapse is 0, the burnCollapseExposure function nevertheless executes, calling 0 transfers and adding 0 to accounting for a burn collapse exposure . Although there is no harm done, this is a waste of gas for the user.
Mitigation/Fix:
Add a revert condition to burnCollapseExposure to revert execution if the max repayment a borrower can make is 0.
The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification.
We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Term, Certora or any of its or their respective employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here.
Overview of the verification
Description of the system
The Term Finance Protocol enables noncustodial fixed-rate collateralized lending on-chain (Term Repos) modeled on tri-party repo arrangements common in TradFi. Borrowers and lenders are matched through a unique recurring auction process (Term Auctions) where borrowers submit sealed bids and lenders submit sealed offers that are used to determine an interest rate that clears the market for participants of that auction. Participants who bid more than the clearing rate receive loans and participants willing to lend below the clearing rate make loans, in each case at the market-clearing rate. All other participants’ bids and offers are said to be “left on the table.” At the conclusion of an auction, borrowers receive loan proceeds and lenders receive ERC-20 tokens (Term Repo Tokens), which are receipts that lenders will burn to redeem for principal plus interest at maturity. Protocol smart contracts service these transactions by ledgering repayments and monitoring collateral health and liquidations.
Description of the specification files
For each contract, spec rules are divided into separate spec files per business logic function type (separate spec for state variable rules), but during runtime are compiled together in a rules.spec file. For the termRepoCollateralManager, the rules.spec is further divided into a rules.spec and other spec files for liquidations and state variables, due to the nature of high verification fun times for those functions.
Assumptions and Simplifications
Some loops were run with a fixed size of 1 in able to enable formal verification. Verifying beyond a 1st loop would have cause formal verification to time out.
Token prices are fetched from a constant mapping in CVL instead of a live price feed. This enables easier comparison of expected calculations and actual token amounts.
Some of the multiplications and divisions in liquidation functions in the smart contracts inherit a contract called ExponentialNoError, which scales and truncates multiplications and divisions in Solidity in a way that precision is not lost. The calculations in these functions were replaced with CVL equivalents in order to prevent timeouts of FV rules.
Contract Invariants and Rules
Common Rules
Applied to every contract in the protocol.
Rule: pairTermContractsRevertsWhenAlreadyPaired - constrain input space to only include contracts that have already been paired.
requireisTermContractPaired(); pairTermContracts@withrevert(e, args);assert lastReverted,"pairTermContracts(...) should revert when calling it on an already paired contract";assertisTermContractPaired(),"termContractPaired should not change when calling pairTermContracts(...) on an already paired contract";}
Rule: onlyPairTermContractsChangesIsTermContractPairedRule - ensures that only pairTermContracts(...) can change state of termContractPaired
bool isTermContractPairedBefore =isTermContractPaired();f(e, args);bool isTermContractPairedAfter =isTermContractPaired();assert isTermContractPairedBefore == isTermContractPairedAfter,"termContractPaired should not change when calling methods other than pairTermContracts(...)";
TermRepoToken.sol
Invariant totalSupplyIsSumOfBalances - ensures that the total supply of tokens always equals the sum of individual account balances, maintaining the principle of token conservation.
to_mathint(totalSupply()) == sumOfBalances
Rule: totalSupplyNeverOverflow - guarantees that the total supply of tokens cannot exceed the maximum value allowed by the system, preventing overflow errors.
assert totalSupplyBefore <= totalSupplyAfter;
Rule: noMethodChangesMoreThanTwoBalances - ensures that no single operation can alter more than two account balances at once.
Rule: onlyAllowedMethodsMayChangeAllowance - verifies that changes to token allowances are restricted to approved methods, ensuring that delegated spending limits are securely managed.
Rule: onlyAllowedMethodsMayChangeBalance - verifies that token balance changes within accounts can only be done through approved methods, preventing unauthorized modifications.
Rule: onlyAllowedMethodsMayChangeTotalSupply - verifies that changes to the total supply of tokens are conducted only through authorized methods, maintaining supply integrity.
Rule: onlyHolderOfSpenderCanChangeAllowance - verifies that changes to spending allowance, which is the limit set by the token holder for how much another account can spend on their behalf, can only be made by the token holder or a designated spender
Rule: mintRedemptionValueIntegrity - ensures that after minting tokens and returning a value, the balance of the minter and the total supply are correctly increased.
Rule: mintRedemptionValueDoesNotAffectThirdParty - verifies that when one account invokes mintRedemptionValue, this action does not affect third-party balances.
require addr1 != addr2;uint256 before =balanceOf(addr2);mintRedemptionValue(e, addr1, amount);assertbalanceOf(addr2) == before;
Rule: mintTokensDoesNotAffectThirdParty - verifies that when one account invokes mintOpenExposure, this action does not affect third-party balances.
require addr1 != addr2;uint256 before =balanceOf(addr2);mintTokens(e, addr1, amount);assertbalanceOf(addr2) == before;
Rule: burnIntegrity - ensures that after burning tokens, the balance of the burner and the total supply are correctly decreased.
Rule: burnAndReturnValueIntegrity - ensures that after burning tokens and returning a value, the balance of the burner and the total supply are correctly decreased.
Rule: burnRevertingConditions - checks conditions under which a burn operation should revert, such as not having enough balance, the contract being paused, etc.
Rule: burnDoesNotAffectThirdParty - verifies that burning tokens from one account does not affect third party balances.
assertbalanceOf(addr2) == before;
Rule: burnAndReturnValueDoesNotAffectThirdParty - confirms that burning tokens and returning a value from one account does not impact the balance of an unrelated account.
assertbalanceOf(addr2) == before;
Rule: transferIntegrity - asserts that after a transfer, the balances of the sender and recipient are updated correctly, respecting the case when sender and recipient are the same.
Rule: transferIsOneWayAdditive - demonstrates that if a transfer of a combined amount succeeds, individual transfers of the components should also succeed without affecting the final state.
transfer(e, recipient,assert_uint256(sum));storage after1 = lastStorage; transfer@withrevert(e, recipient, amount_a) at init; // restores storageassert!lastReverted; //if the transfer passed with sum, it should pass with both summands individually transfer@withrevert(e, recipient, amount_b);assert!lastReverted;storage after2 = lastStorage;assert after1[currentContract] == after2[currentContract];
Rule: transferRevertingConditions- identifies conditions under which a transfer should revert, such as the sender not having enough balance.
Rule: transferDoesNotAffectThirdParty - ensures that a transfer between two accounts does not affect the balance of a third party.
assertbalanceOf(addr2) == before;
Rule: transferFromIntegrity - confirms that after a transferFrom operation, the balances of the holder and recipient are correctly adjusted, and the allowance is updated appropriately.
Rule: transferFromIsOneWayAdditive - shows that if a transferFrom for a combined amount is successful, then separate transferFrom operations for each component of the amount should also succeed, without altering the final state.
transferFrom(e, owner, recipient,assert_uint256(sum));storage after1 = lastStorage; transferFrom@withrevert(e, owner, recipient, amount_a) at init; // restores storageassert!lastReverted; //if the transfer passed with sum, it should pass with both summands individually transferFrom@withrevert(e, owner, recipient, amount_b);assert!lastReverted;storage after2 = lastStorage;assert after1[currentContract] == after2[currentContract];
Rule: approveIntegrity - ensures that the allowance is correctly set after an approve operation.
assertallowance(holder, spender) == amount;
Rule: approveRevertingConditions - identifies scenarios in which an approve operation should revert, such as when trying to approve from a zero address.
Rule: onlyAllowedMethodsMayChangeMintExposureCap - ensures that only specific methods can modify the mint exposure cap. Methods like minting, burning, or resetting the cap are allowed to change it.
Rule: mintExposureCapNeverOverflow - verifies that when the mint exposure cap is increased, this action does not cause it to overflow, ensuring the cap's value remains within safe limits.
Rule: noMethodChangesRedemptionValue - confirms that the redemption value remains unchanged across transactions, except by methods explicitly intended to modify it. This rule ensures stability in the redemption value.
Rule: onlyRoleCanCallRevert - checks if a method call that is not a view and requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: onlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: onlyAllowedMethodsMayChangeTransfersPaused - ensures that the state of transfers being paused can only be altered by specific methods designated for pausing or unpausing transfers.
Rule: noMethodChangesTermRepoId - confirms that the Term Repo ID remains constant and is not changed by any method calls, ensuring its immutability post-initialization.
Rule: onlyAllowedMethodsMayChangeEmitter - verifies that the emitter's address can only be changed through specific methods, preserving the integrity and security of the emitter identification.
Rule: reachability - verifies that all non-initialization and non-upgrade methods can be executed, ensuring contract functionality is accessible.
f(e,args);satisfy true;
Rule: transferTokenFromWalletIntegrity - validates the integrity of transferring tokens from the wallet, checking the update in treasury and sender balances post-transaction.
Rule: transferTokenToWalletIntegrity - ensures the correct adjustment of balances when tokens are transferred to the wallet, factoring in role permissions and pause status.
Rule: pauseTransfersIntegrity - validates that transfers can be paused correctly by the authorized role, ensuring the state is changed as expected.
pauseTransfers(e);asserttransfersPaused();
Rule: unpauseTransfersIntegrity - confirms that transfers can be unpaused accurately, reverting the paused state and allowing transactions to proceed.
unpauseTransfers(e);assert!transfersPaused();
Rule: onlyRoleCanCallRevert - ensures that methods not related to initialization, upgrade, or role management only revert if the caller lacks the necessary roles. This rule safeguards against unauthorized actions while allowing legitimate operations.
currentContract.f@withrevert(e,args);// Verification if the method didn't revert, the caller must possess one of the specified roles.assert!lastReverted =>hasRole(SERVICER_ROLE(),e.msg.sender)||hasRole(ADMIN_ROLE(),e.msg.sender)||hasRole(DEVOPS_ROLE(),e.msg.sender)||hasRole(INITIALIZER_ROLE(),e.msg.sender);
Rule: onlyRoleCanCallStorage - verifies that storage modifications by non-view methods are properly guarded by role checks, preventing unauthorized changes to the contract's state. This rule enforces role-based access control for sensitive operations.
storage storeBefore = lastStorage;currentContract.f(e,args);storage storeAfter = lastStorage;// Conditionally asserts that if storage was altered, the action must have been performed by an entity with an appropriate role.
assert storeBefore != storeAfter =>hasRole(SERVICER_ROLE(),e.msg.sender)||hasRole(ADMIN_ROLE(),e.msg.sender)||hasRole(DEVOPS_ROLE(),e.msg.sender)||hasRole(INITIALIZER_ROLE(),e.msg.sender);
TermRepoServicer.sol
Invariant: totalOutstandingRepurchaseExposureIsSumOfRepurchases - asserts that the total outstanding repurchase exposure is equal to the sum of all individual repurchase exposures, ensuring consistency within the ledger.
Rule: onlyAllowedMethodsMayChangeTotalOutstandingRepurchaseExposure - specifies that only particular methods can increase or decrease the total outstanding repurchase exposure, aligning changes with expected business logic operations.
Rule: totalOutstandingRepurchaseExposureNeverOverflows - ensures that actions intended to increase the total outstanding repurchase exposure do not result in an overflow, preserving the integrity of financial calculations.
Rule: onlyAllowedMethodsMayChangeTotalRepurchaseCollected - identifies methods permitted to increase or decrease the total repurchase collected, ensuring that financial metrics reflect actual repurchase activity accurately.
Rule: totalRepurchaseCollectedNeverOverflows - verifies that the total repurchase collected metric cannot overflow as a result of any operation, maintaining the system's financial stability.
Rule:shortfallHaircutMantissaAlwaysZeroBeforeRedemptionAndLessThanExpScaleAfter - confirms the shortfall haircut mantissa remains zero before the redemption timestamp and falls within expected bounds after, ensuring fair and predictable financial adjustments.
Rule: totalRepurchaseCollectedLessThanOrEqualToLockerPurchaseTokenBalance - ensures that the total repurchase collected does not exceed the locker's purchase token balance, preventing overestimation of collected repurchases.
require(termRepoLocker() == stateLocker); // bounds for test
require(purchaseToken() == stateToken); // bounds for test
require(totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker)); // starting condition
require(e.msg.sender != stateLocker); // repo locker contract does not have calls to servicer
require(!isTokenCollateral(stateToken)); // token will not be both purchase and collateral token
f(e, args);
assert (totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker));
Rule: noMethodsChangeMaturityTimestamp - validates that no method changes the maturity timestamp, ensuring consistency in the term's length and financial obligations.
Rule: noMethodsChangeEndOfRepurchaseWindow - confirms the end of the repurchase window is immutable across all contract interactions, preserving the predetermined timeframe for repurchases, which is critical for contractual agreements.
Rule: noMethodsChangeRedemptionTimestamp - ensures the redemption timestamp remains constant across all contract interactions, guaranteeing the redemption period's stability and predictability.
Rule: noMethodsChangeServicingFee - verifies that the servicing fee rate is maintained across all transactions, ensuring consistent fee calculations and financial expectations for parties involved.
Rule: onlyAllowedMethodsChangeShortfallHaircutMantissa - restricts adjustments to the shortfall haircut mantissa to specific authorized methods, safeguarding the metric's integrity against unauthorized modifications.
Rule: noMethodChangesPurchaseToken - confirms the purchase token's address remains unaltered through contract operations, ensuring continuity and reliability in financial mechanisms involving the token.
Rule: onlyAllowedMethodsMayChangeTermContracts - specifies that term contract addresses can only be modified through designated methods, preventing unauthorized updates and maintaining contract ecosystem integrity.
Rule: onlyAllowedMethodsMayChangeRepurchaseExposureLedger - limits the conditions under which the repurchase exposure ledger can be altered, ensuring that changes are strictly governed and reflect actual repurchase activities.
Rule: burnCollapseExposureMonotonicBehavior - verifies that burning to collapse exposure reduces the caller's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure monotonically, ensuring systemic risk reduction and individual accountability.
Rule: burnCollapseExposureIntegrity - ensures that burning for exposure collapse adjusts the repo token balance, repurchase obligation, and total outstanding repurchase exposure by the expected amounts, reflecting accurate and fair financial adjustments.
Rule: burnCollapseExposureDoesNotAffectThirdParty - confirms that an individual's action to burn repo tokens to collapse exposure does not impact the financial positions (token balances or repurchase obligations) of unrelated third parties, maintaining isolation of financial activities.
Rule: mintOpenExposureMonotonicBehavior - ensures that minting open exposure increases the minter's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure, as well as the minter's collateral balance, indicating correct operation and accountability in minting activities.
Rule: mintOpenExposureIntegrity - confirms that minting for open exposure results in expected increases in the minter's repo token balance and repurchase obligation, as well as the total outstanding repurchase exposure, demonstrating the transaction's impact aligns with predefined financial mechanisms.
Rule: mintOpenExposureDoesNotAffectThirdParty - verifies that a minter's action to open exposure does not alter the repo token balances of unrelated third parties, ensuring the isolation of minting effects within the financial ecosystem.
Rule: redemptionsMonotonicBehavior - verifies that redemption operations result in expected changes to the balances and obligations involved, ensuring that the redeemer's repo token balance decreases, their purchase token balance increases, and the overall repurchase obligations and available tokens within the locker adjust accordingly.
Rule: redemptionsIntegrity - confirms that the redemption of repo tokens by a redeemer leads to the precise adjustments in the total repurchase collected, the repo token balance of the redeemer, and the purchase token balance in accordance with the redemption value and terms defined, reflecting the accurate financial transaction and impact.
Rule: redemptionsDoesNotAffectThirdParty - ensures that a redemption action taken by one participant does not inadvertently alter the financial position or balances of unrelated third parties, maintaining the integrity and isolation of individual transactions within the ecosystem.
Rule: redemptionsRevertConditions - evaluates whether the operation correctly reverts under the prescribed conditions, ensuring compliance with defined contractual behaviors and protections.
Rule: repaymentsMonotonicBehavior - validates that repayments lead to expected monotonic changes in borrower obligations and system totals, ensuring borrower balances and overall repurchase exposures decrease as payments are made, while the total repurchase collected and potentially the collateral values adjust accordingly.
Rule: repaymentsIntegrity - ensures the integrity of repayments by verifying that the repayments correctly decrease the borrower's obligations and appropriately adjust the system's repurchase exposure and collected totals, with specific attention to the treatment of collateral in the event of complete repayment.
Rule: repaymentsDoesNotAffectThirdParty - confirms that a borrower's repayment activity does not inadvertently affect the financial obligations or collateral standings of any unrelated third parties, preserving the isolation and accuracy of individual account statuses within the system.
Rule: repaymentsRevertingConditions - check if the operation correctly reverts under specified conditions, ensuring adherence to defined contractual behaviors and safeguards.
Rule: liquidatorCoverExposureIntegrity - validates the integrity of a liquidation process where a liquidator covers the exposure of a borrower using purchase tokens. It checks that balances and obligations adjust correctly, reflecting the liquidation payment in system totals and individual accounts.
Rule: liquidatorCoverExposureDoesNotAffectThirdParty - ensures that the liquidation process does not inadvertently impact the financial status or obligations of any third parties, maintaining the precision and isolation of account transactions within the system.
Rule: liquidatorCoverExposureRevertConditions - evaluate if the transaction reverts as expected under identified conditions, ensuring compliance with system rules and safeguards.
Rule: liquidatorCoverExposureWithRepoTokenIntegrity - examines the proper functioning of liquidation via repo tokens, verifying that such transactions correctly reduce borrower obligations and adjust system and participant balances in accordance with the repo tokens used in the liquidation.
Rule: liquidatorCoverExposureWithRepoTokenRevertConditions - define conditions that would lead to a transaction revert; aggregate revert conditions to determine expectation; eliquidation attempt with potential revert and validate against expected outcome; ensure actual revert aligns with expectations based on identified conditions.
Rule: openExposureOnRolloverNewIntegrity - ensures that all relevant balances properly accounted for after opening a repoExposure on account of a successful rollover.
Rule: openExposureOnRolloverNewDoesNotAffectThirdParty - verifies that rolling over loan exposures from one account does not affect third-party balances.
Rule: openExposureOnRolloverNewRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: closeExposureOnRolloverExistingIntegrity - ensures that all relevant balances properly accounted for after closing a repoExposure on account of a successful rollover.
Rule: closeExposureOnRolloverExistingDoesNotAffectThirdParty - verifies that rolling over loan exposures from one account does not affect third-party balances.
Rule: closeExposureOnRolloverExistingRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: onlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: onlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: auctionLockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling auctionLockCollateral
Rule: auctionLockCollateralThirdParty - verifies that locking collateral belonging to one account when calling lockBid does not affect the third party balances
Rule: auctionUnlockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling auctionUnlockCollateral
Rule: auctionUnlockCollateralThirdParty - verifies that unlocking collateral belonging to one account when calling auctionUnlockCollateral does not affect the third party balances
Rule: journalBidCollateralToCollateralManagerIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when fulfilling a bid.
Rule: journalBidCollateralToCollateralManagerThirdParty - verifies that journaling collateral to the lockedCollateralLedger when fulfilling a bid belonging to one account does not affect the third party balances.
Rule: journalBidCollateralToCollateralManagerRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: externalLockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling externalLockCollateral.
Rule: externalLockCollateralThirdParty - verifies that locking collateral belonging to one account when calling externalLockCollateral does not affect the third party balances
Rule: externalUnlockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling externalUnlockCollateral.
Rule: externalUnlockCollateralThirdParty - verifies that unlocking collateral belonging to one account when calling externalUnlockCollateraldoes not affect the third party balances
Rule: lockerCollateralTokenBalanceGreaterThanCollateralLedgerBalance - verifies the assumption that total collateral token balances is always less than or equal to the balance recorded in ledger
Rule: onlyAllowedMethodsMayChangeEncumberedCollateralBalances - verifies that changes to the balances of encumbered collateral to specific methods, ensuring that such modifications are controlled and intentional.
Rule: sumOfCollateralBalancesLessThanEncumberedBalances - verifes the assumption that the total sum of all collateral balances is always less than the encumbered collateral balance.
Rule: batchLiquidationSuccessfullyLiquidates - assert that the locker's balances, the liquidator's balances and protocol reserve's balances have changed by the correct amount after bathLiquidate
// Assert that the locker's balances have changed by the correct amount.
assert(lockerCollateralTokenBalanceBefore - lockerCollateralTokenBalanceAfter == liquidationIncentiveAmount);
assert(lockerPurchaseTokenBalanceAfter - lockerPurchaseTokenBalanceBefore == to_mathint(closureAmount));
// Assert that the liquidator's balances have changed by the correct amount.
assert(liquidatorCollateralTokenBalanceAfter - liquidatorCollateralTokenBalanceBefore == liquidationIncentiveAmount - protocolLiquidatedDamagesAmount);
assert(liquidatorPurchaseTokenBalanceBefore - liquidatorPurchaseTokenBalanceAfter == to_mathint(closureAmount));
// Assert that the reserve's balances have changed by the correct amount.
assert(reserveCollateralTokenBalanceAfter - reserveCollateralTokenBalanceBefore == protocolLiquidatedDamagesAmount);
Rule: batchLiquidateWithRepoTokenSuccessfullyLiquidates - assert that the locker's balances, liquidators balances and protocol reserve blances have changed by the correct amount after calling batchLiquidatedWithRepoToken
// Assert that the locker's balances have changed by the correct amount.
assert(lockerCollateralTokenBalanceBefore - lockerCollateralTokenBalanceAfter == liquidationIncentiveAmount);
// Assert that the liquidator's balances have changed by the correct amount.
assert(liquidatorCollateralTokenBalanceAfter - liquidatorCollateralTokenBalanceBefore == liquidationIncentiveAmount - protocolLiquidatedDamagesAmount);
assert(liquidatorRepoTokenBalanceBefore - liquidatorRepoTokenBalanceAfter == to_mathint(closureRepoTokenAmount));
// Assert that the reserve's balances have changed by the correct amount.
assert(reserveCollateralTokenBalanceAfter - reserveCollateralTokenBalanceBefore == protocolLiquidatedDamagesAmount);
}
Rule: batchDefaultSuccessfullyDefaults - assert that the locker's balances, liquidator's balances and protocol reserve balances have changed by the correct amount after callingbatchDefault
// Assert that the locker's balances have changed by the correct amount.
assert(lockerCollateralTokenBalanceBefore - lockerCollateralTokenBalanceAfter == liquidationIncentiveAmount);
assert(lockerPurchaseTokenBalanceAfter - lockerPurchaseTokenBalanceBefore == to_mathint(closureAmount));
// Assert that the liquidator's balances have changed by the correct amount.
assert(liquidatorCollateralTokenBalanceAfter - liquidatorCollateralTokenBalanceBefore == liquidationIncentiveAmount - protocolLiquidatedDamagesAmount);
assert(liquidatorPurchaseTokenBalanceBefore - liquidatorPurchaseTokenBalanceAfter == to_mathint(closureAmount));
// Assert that the reserve's balances have changed by the correct amount.
assert(reserveCollateralTokenBalanceAfter - reserveCollateralTokenBalanceBefore == protocolLiquidatedDamagesAmount);
// assert(reservePurchaseTokenBalanceAfter == reservePurchaseTokenBalanceBefore);
Rule: batchLiquidationDoesNotAffectThirdParty - verifies that liquidating collateral belonging to one account does not affect the third party balances.
Rule: batchLiquidationWithRepoTokenDoesNotAffectThirdParty - verifies that liquidating collateral using batchLiquidationWithRepoToken belonging to one account does not affect the third party balances.
Rule: batchDefaultDoesNotAffectThirdParty - verifies that liquidating collateral belonging to one account when calling batchDefault does not affect the third party balances.
Rule: onlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: onlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: onlyAllowedMethodsChangeApprovedRolloverAuctionBidLockers - verifies that changes to approved rollover contracts are restricted to certain allowed methods.
// Specifies which methods can change the approval status of rollover auction bid lockers.
env e, method f, calldataarg args, address bidLocker filtered {
f -> !f.isView &&
f.selector != initialize(string,address,address,address,address).selector &&
f.selector != upgradeToAndCall(address,bytes).selector &&
f.selector != upgradeTo(address).selector &&
f.selector != electRollover(TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission).selector &&
f.selector != approveRolloverAuction(address).selector &&
f.selector != revokeRolloverApproval(address).selector
} {
bool isRolloverAuctionApprovedBefore = isRolloverAuctionApproved(bidLocker);
f(e, args);
bool isRolloverAuctionApprovedAfter = isRolloverAuctionApproved(bidLocker);
assert isRolloverAuctionApprovedBefore == isRolloverAuctionApprovedAfter,
"only the approveRolloverAuction method can change the approved rollover auction bid lockers";
}
Rule: onlyAllowedMethodsChangeRolloverElections - verifies that changes to rollover elections are restricted to certain allowed methods.
Rule: electRolloverDoesNotAffectThirdParty - verifies that the action of one account electing to roll over their loan does not impact third-party balances.
Rule: electRolloverRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission submission;
// Define various conditions that lead to reversion (simplified for clarity).
bool isExpectedToRevert = /* conditions leading to revert */;
electRollover@withrevert(e, submission);
assert lastReverted <=> isExpectedToRevert;
Rule: cancelRolloverIntegrity - ensures that all relevant balances are properly reflected when cancelling a roll-over election.
Rule cancelRolloverDoesNotAffectThirdParty - verifies that the action of one account cancelling their roll over election does not impact third-party balances.
Rule: fulfillRolloverIntegrity - ensures that a rollover election is properly marked as processed when fulfilled.
fulfillRollover(e, borrower);
bool rolloverProcessed = getRolloverInstructions(borrower).processed;
assert rolloverProcessed, "The rollover should be marked as processed.";
Rule: fulfillRolloverDoesNotAffectThirdParty - verifies that fulfilling a rollover election submitted by one account does not affect the third party balances
Rule: fulfillRolloverRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
bool payable = e.msg.value > 0;
bool callerNotRolloverBidFulfillerRole = !hasRole(ROLLOVER_BID_FULFILLER_ROLE(), e.msg.sender);
bool isExpectedToRevert = payable || callerNotRolloverBidFulfillerRole;
fulfillRollover@withrevert(e, borrower);
assert lastReverted <=> isExpectedToRevert, "fulfillRollover should only revert under specific conditions.";
Rule: onlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.
assert !lastReverted =>
hasRole(ADMIN_ROLE(),e.msg.sender)
|| hasRole(DEVOPS_ROLE(),e.msg.sender)
|| hasRole(ROLLOVER_BID_FULFILLER_ROLE(),e.msg.sender)
|| hasRole(INITIALIZER_ROLE(),e.msg.sender), "Function should only be callable by specific roles without reverting.";
}
Rule: onlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
assert storeBefore != storeAfter =>
hasRole(ADMIN_ROLE(),e.msg.sender)
|| hasRole(DEVOPS_ROLE(),e.msg.sender)
|| hasRole(ROLLOVER_BID_FULFILLER_ROLE(),e.msg.sender)
|| hasRole(INITIALIZER_ROLE(),e.msg.sender), "Only specific roles should be able to cause state changes.";
TermAuctionBidLocker
Rule: PauseLockingCausesBidLockingToRevert - verifies that pausing locking reverts any attempts at locking bids.
require lockingPaused() == true;
f@withrevert(e, args);
assert lastReverted, "lockBids(...) should revert when bid locking is paused";
Rule: UnpauseLockingAllowsBidLocking - verifies that unpausing locking allows users to lock bids.
require lockingPaused() == false;
f(e, args);
assert !lastReverted, "lockBids(...) should not revert when bid locking is not paused";
Rule: PauseUnlockingCausesBidUnlockingToRevert - verifies that pausing unlocking reverts any attempts at unlocking offers.
require unlockingPaused() == true;
unlockBids@withrevert(e, ids);
assert lastReverted, "unlockBids(...) should revert when bid unlocking is paused";
Rule: UnpauseUnlockingAllowsBidUnlocking - verifies that unpausing locking allows users to unlock bids.
require unlockingPaused() == false;
require harnessGetInternalBids(id).id == id;
unlockBids(e, [id]);
assert !lastReverted, "unlockBids(...) should not revert when bid unlocking is not paused";
Rule: lockerCollateralTokenBalanceGreaterThanCollateralLedgerBalance - verified the assumption that the total amount of collateral locked is always greater than or equal to the amount recorded in ledger.
Invariant: BidCountAlwaysMatchesNumberOfStoredBids - verifies the assumption that the bidCount matches the ledger.
to_mathint(bidCount()) == lockedBidCount;
Rule: LockBidsIntegrity - ensures that collateral token balances are properly transferred to the repo locker when locking bids.
assert
(collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore - collateralOneAmountToLock),
"lockBids should transfer collateral tokens from bidder to contract";
assert
(collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore - collateralTwoAmountToLock),
"lockBids should transfer collateral tokens from bidder to contract";
Rule: LockBidsDoesNotAffectThirdParty - verifies that locking bids belonging to one account does not affect the third party balances.
assert bidIdBefore == bidIdAfter,
"lockBids should not modify bid id";
assert bidderBefore == bidderAfter,
"lockBids should not modify bidder";
assert bidPriceHashBefore == bidPriceHashAfter,
"lockBids should not modify bid price hash";
assert bidRevealedPriceBefore == bidRevealedPriceAfter,
"lockBids should not modify bid revealed price";
assert bidAmountBefore == bidAmountAfter,
"lockBids should not modify bid amount";
assert bidCollateralAmountBefore == bidCollateralAmountAfter,
"lockBids should not modify bid collateral amounts";
assert bidIsRolloverBefore == bidIsRolloverAfter,
"lockBids should not modify bid rollover status";
assert bidRolloverAddressBefore == bidRolloverAddressAfter,
"lockBids should not modify bid rollover address";
assert bidIsRevealedBefore == bidIsRevealedAfter,
"lockBids should not modify bid revealed status";
Rule: lockBidsMonotonicBehavior - verifies that locking a bid is monotonically increasing in the bid count.
uint256 bidCountBefore = bidCount();
lockBids(e, bidSubmissions);
uint256 bidCountAfter = bidCount();
assert bidCountAfter >= bidCountBefore,
"bidCount should either increase or stay the same after lockBids is called";
Rule: LockBidsRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: lockBidsWithReferralIntegrity - ensures that collateral token balances are properly transferred to the repo locker when locking bids with a referral.
assert
(collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore - collateralOneAmountToLock) &&
(collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore - collateralTwoAmountToLock),
"lockBids should transfer collateral tokens from bidder to contract";
Rule: lockBidsWithReferralDoesNotAffectThirdParty - verifies that locking bids belonging to one account when calling lockBidsWithReferral does not affect the third party balances.
assert bidIdBefore == bidIdAfter,
"lockBidsWithReferral should not modify bid id";
assert bidderBefore == bidderAfter,
"lockBidsWithReferral should not modify bidder";
assert bidPriceHashBefore == bidPriceHashAfter,
"lockBidsWithReferral should not modify bid price hash";
assert bidRevealedPriceBefore == bidRevealedPriceAfter,
"lockBidsWithReferral should not modify bid revealed price";
assert bidAmountBefore == bidAmountAfter,
"lockBidsWithReferral should not modify bid amount";
assert bidCollateralAmountBefore == bidCollateralAmountAfter,
"lockBidsWithReferral should not modify bid collateral amounts";
assert bidIsRolloverBefore == bidIsRolloverAfter,
"lockBidsWithReferral should not modify bid rollover status";
assert bidRolloverAddressBefore == bidRolloverAddressAfter,
"lockBidsWithReferral should not modify bid rollover address";
assert bidIsRevealedBefore == bidIsRevealedAfter,
"lockBidsWithReferral should not modify bid revealed status";
Rule: lockBidsWithReferralRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: UnlockBidsMonotonicBehavior - verifies that unlocking a bid is monotonically decreasing in the bid count.
assert bidCountAfter <= bidCountBefore,
"unlockBids should decrease or maintain bid count";
Rule: AuctionUnlockBidIntegrity - ensures that collateral token balances are properly transferred from the repo locker to the user when unlocking bids.
if (bidCollateralTokens.length > 1) {
assert collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore + amounts[1],
"collateral token two balance should increase by the amount of collateral token two";
}
assert bidCollateralTokens.length == 0 || collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore + amounts[0],
"collateral token one balance should increase by the amount of collateral token one";
Rule: AuctionUnlockBidDoesNotAffectThirdParty - verifies that unlocking bids belonging to one account does not affect the third party balances.
assert bidIdBefore == bidIdAfter,
"lockBids should not modify bid id";
assert bidderBefore == bidderAfter,
"lockBids should not modify bidder";
assert bidPriceHashBefore == bidPriceHashAfter,
"lockBids should not modify bid price hash";
assert bidRevealedPriceBefore == bidRevealedPriceAfter,
"lockBids should not modify bid revealed price";
assert bidAmountBefore == bidAmountAfter,
"lockBids should not modify bid amount";
assert bidCollateralAmountBefore == bidCollateralAmountAfter,
"lockBids should not modify bid collateral amounts";
assert bidIsRolloverBefore == bidIsRolloverAfter,
"lockBids should not modify bid rollover status";
assert bidRolloverAddressBefore == bidRolloverAddressAfter,
"lockBids should not modify bid rollover address";
assert bidIsRevealedBefore == bidIsRevealedAfter,
"lockBids should not modify bid revealed status";
Rule: AuctionUnlockBidRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: RevealBidsMonotonicBehavior - verifies that revealBids does not change the bid count.
assert bidCountBefore == bidCountAfter,
"revealBids should not change bid count";
Rule: OnlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: OnlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: PauseLockingCausesOfferLockingToRevert - verifies that pausing locking reverts any attempts at locking offers.
require lockingPaused() == true;
f@withrevert(e, args);
assert lastReverted,
"lockOffers(...) should revert when trying to lock a paused contract";
Rule: UnpauseLockingAllowsOfferLocking - verifies that unpausing locking allows users to lock offers.
require lockingPaused() == false;
f(e, args);
assert !lastReverted, "lockOffers(...) should not revert when trying to lock offers on an unpaused contract";
Rule: PauseUnlockingCausesOfferUnlockingToRevert - verifies that pausing unlocking reverts any attempts at unlocking offers.
require unlockingPaused() == true;
unlockOffers@withrevert(e, ids);
assert lastReverted, "unlockOffers(...) should revert when trying to unlock offers on a paused contract";
Rule: UnpauseUnlockingAllowsOfferUnlocking - verifies that unpausing unlocking allows users to unlock offers.
require unlockingPaused() == false;
require harnessGetInternalOffers(id).id == id;
unlockOffers(e, [id]);
assert !lastReverted, "unlockOffers(...) should not revert when trying to unlock offers on an unpaused contract";
Invariant: LockedOfferIdAlwaysMatchesIndex - verifies the assumption that the offerId matches the ledger.
Invariant: OfferCountAlwaysMatchesNumberOfStoredOffers - verifies the assumption that the offerCount always matches the ledger.
to_mathint(offerCount()) == lockedOfferCount;
Rule: lockerPurchaseTokenBalanceGreaterThanOfferLedgerBalance - verifies the assumption that total purchaseToken balances are always greater than or equal to the amount recorded in ledger.
Rule: LockOffersIntegrity - ensures that purchase token balances are properly transferred to the repo locker when locking offers.
assert (purchaseTokenOneBalanceAfter == purchaseTokenBalanceBefore - amountToLock),
"lockOffers should transfer collateral tokens from offeror to contract";
Rule: LockOffersDoesNotAffectThirdParty - verifies that locking offers belonging to one account does not affect the third party balances.
assert offerIdBefore == offerIdAfter,
"lockRolloverOffer should not modify offer id";
assert offerorBefore == offerorAfter,
"lockRolloverOffer should not modify offeror";
assert offerPriceHashBefore == offerPriceHashAfter,
"lockRolloverOffer should not modify offer price hash";
assert offerRevealedPriceBefore == offerRevealedPriceAfter,
"lockRolloverOffer should not modify offer revealed price";
assert offerAmountBefore == offerAmountAfter,
"lockRolloverOffer should not modify offer amount";
assert offerIsRevealedBefore == offerIsRevealedAfter,
"lockRolloverOffer should not modify offer revealed status";
Rule: LockOffersMonotonicBehavior - verifies that locking offers is monotonically increasing in the offer count.
assert offerCountAfter >= offerCountBefore,
"offerCount should increment or maintain the same value after locking an offer";
Rule: LockOffersRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: LockOffersWithReferralIntegrity - ensures that purchase token balances are properly transferred to the repo locker when locking offers with referral.
assert (purchaseTokenOneBalanceAfter == purchaseTokenBalanceBefore - amountToLock),
"lockOffers should transfer collateral tokens from offeror to contract";
Rule: LockOffersWithReferralDoesNotAffectThirdParty - verifies that locking offers belonging to one account when calling lockOffersWithReferral does not affect the third party balances
assert offerIdBefore == offerIdAfter,
"lockRolloverOffer should not modify offer id";
assert offerorBefore == offerorAfter,
"lockRolloverOffer should not modify offeror";
assert offerPriceHashBefore == offerPriceHashAfter,
"lockRolloverOffer should not modify offer price hash";
assert offerRevealedPriceBefore == offerRevealedPriceAfter,
"lockRolloverOffer should not modify offer revealed price";
assert offerAmountBefore == offerAmountAfter,
"lockRolloverOffer should not modify offer amount";
assert offerIsRevealedBefore == offerIsRevealedAfter,
"lockRolloverOffer should not modify offer revealed status";
Rule: LockOffersWithReferralRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: UnlockOffersMonotonicBehavior - verifies that unlocking offers is monotonically decreasing in the offer count.
assert offerCountAfter == assert_uint256(offerCountBefore - unlockOfferIds.length),
"offerCount should decrement by the number of offer ids submitted to unlock";
Rule: UnlockOfferPartialIntegrity - ensures that purchase token balances are properly transferred to user when partially unlocking offers.
assert purchaseTokenBalancAfter == purchaseTokenBalanceBefore + amount,
"purchase token balance should increase by the provided amount";
Rule: UnlockOfferPartialDoesNotAffectThirdParty - verifies that partially unlocking offers belonging to one account does not affect the third party balances
assert thirdPartyOfferNotAffected,
"unlockOfferPartial should not modify offers that are not in args";
Rule: UnlockOfferPartialRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.
Rule: RevealOffersMonotonicBehavior - verifies that revealing offers does not change the offer count.
assert offerCountBefore == offerCountAfter, "revealOffers should not change the offer count";
Rule: OnlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: OnlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: OnlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: OnlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.
Rule: OnlyRoleCanCallRevertCompleteAuction and OnlyRoleCanCallStorageCompleteAuction - verifies that the completeAuction call where unrevealed bids exists requires specific roles to execute successfully, does not revert if the caller has the necessary role.
Rule: OnlyRoleCanCallStorageCompleteAuction - ensures that changes to storage by the completeAuction call where unrevealed bids exists can only be performed by addresses with the admin role, guarding against unauthorized auction clearing where unrevealed bids exist.
Install certora-cli package with pip install certora-cli. To verify specification files, pass to certoraRun the corresponding configuration file in the [certora/confs](<https://github.com/morpho-org/morpho-blue/blob/2ffb6821815ec542c78e0d0379b5e7094d6fd37a/certora/confs>) folder. It requires having set the CERTORAKEY environment variable to a valid Certora key. You can also pass additional arguments, notably to verify a specific rule. For example, at the root of the repository: