diff --git a/.gitmodules b/.gitmodules
index caf1ce87..b6bf3105 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -17,6 +17,9 @@
 [submodule "lib/openzeppelin-contracts-upgradeable"]
 	path = lib/openzeppelin-contracts-upgradeable
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts-upgradeable
+[submodule "lib/kontrol-cheatcodes"]
+	path = lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes
 [submodule "lib/yearn-vaults-v3"]
 	path = lib/yearn-vaults-v3
 	url = https://github.com/yearn/yearn-vaults-v3.git
diff --git a/kontrol.toml b/kontrol.toml
new file mode 100644
index 00000000..2c81847d
--- /dev/null
+++ b/kontrol.toml
@@ -0,0 +1,88 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = true
+rekompile                  = true
+verbose                    = false
+debug                      = false
+require                    = 'src/test/kontrol/term-lemmas.k'
+module-import              = 'RepoTokenListInvariantsTest:TERM-LEMMAS'
+ast                        = true
+auxiliary-lemmas           = true
+
+[prove.setup]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 100000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 1
+max-frontier-parallel      = 6
+maintenance-rate           = 24
+assume-defined             = true
+no-log-rewrites            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+auto_abstract              = true
+run-constructor            = false
+bmc-depth                  = 3
+match-test                 = [
+        "RepoTokenListInvariantsTest.setUp",
+        "TermAuctionListInvariantsTest.setUp",
+    ]
+ast                        = true
+
+[prove.tests]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 100000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 1
+max-frontier-parallel      = 6
+maintenance-rate           = 24
+assume-defined             = true
+no-log-rewrites            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+auto_abstract              = true
+run-constructor            = false
+match-test                 = [
+        "RepoTokenListInvariantsTest.testInsertSortedNewToken",
+        "RepoTokenListInvariantsTest.testInsertSortedDuplicateToken",
+        "RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens",
+        "TermAuctionListInvariantsTest.testInsertPendingNewOffer",
+        "TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer",
+        "TermAuctionListInvariantsTest.testRemoveCompleted",
+    ]
+ast                        = true
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = true
+debug                      = false
\ No newline at end of file
diff --git a/lib/kontrol-cheatcodes b/lib/kontrol-cheatcodes
new file mode 160000
index 00000000..c8a62a00
--- /dev/null
+++ b/lib/kontrol-cheatcodes
@@ -0,0 +1 @@
+Subproject commit c8a62a0054532cb9db15a82b6ce25347cccc882c
diff --git a/src/RepoTokenList.sol b/src/RepoTokenList.sol
index 4e0a5670..5d87fb4a 100644
--- a/src/RepoTokenList.sol
+++ b/src/RepoTokenList.sol
@@ -243,7 +243,7 @@ library RepoTokenList {
         address prev = current;
         while (current != NULL_NODE) {
             address next;
-            if (getRepoTokenMaturity(current) < block.timestamp) {
+            if (getRepoTokenMaturity(current) <= block.timestamp) {
                 bool removeMaturedToken;
                 uint256 repoTokenBalance = ITermRepoToken(current).balanceOf(address(this));
 
@@ -337,6 +337,7 @@ library RepoTokenList {
      * @param repoToken The repoToken to validate and insert
      * @param discountRateAdapter The discount rate adapter
      * @param asset The address of the base asset
+     * @return validRepoToken Whether the repoToken is valid
      * @return discountRate The discount rate to be applied to the validated repoToken 
      * @return redemptionTimestamp The redemption timestamp of the validated repoToken     
      */
@@ -345,14 +346,14 @@ library RepoTokenList {
         ITermRepoToken repoToken,
         ITermDiscountRateAdapter discountRateAdapter,
         address asset
-    ) internal returns (uint256 discountRate, uint256 redemptionTimestamp) {
+    ) internal returns (bool validRepoToken, uint256 discountRate, uint256 redemptionTimestamp) {
         discountRate = listData.discountRates[address(repoToken)];
         if (discountRate != INVALID_AUCTION_RATE) {
             (redemptionTimestamp, , ,) = repoToken.config();
 
             // skip matured repoTokens
             if (redemptionTimestamp < block.timestamp) {
-                revert InvalidRepoToken(address(repoToken));
+                return (false, discountRate, redemptionTimestamp); //revert InvalidRepoToken(address(repoToken));
             }
 
             uint256 oracleRate = discountRateAdapter.getDiscountRate(address(repoToken));
@@ -368,11 +369,13 @@ library RepoTokenList {
 
             (isRepoTokenValid, redemptionTimestamp) = validateRepoToken(listData, repoToken, asset);
             if (!isRepoTokenValid) {
-                revert InvalidRepoToken(address(repoToken));
+                return (false, discountRate, redemptionTimestamp);
             }
             insertSorted(listData, address(repoToken));
             listData.discountRates[address(repoToken)] = discountRate;
         }
+
+        return (true, discountRate, redemptionTimestamp);
     }
 
     /**
@@ -394,6 +397,8 @@ library RepoTokenList {
             return;
         }
 
+        uint256 maturityToInsert = getRepoTokenMaturity(repoToken);
+
         address prev;
         while (current != NULL_NODE) {
 
@@ -403,7 +408,6 @@ library RepoTokenList {
             }
 
             uint256 currentMaturity = getRepoTokenMaturity(current);
-            uint256 maturityToInsert = getRepoTokenMaturity(repoToken);
 
             // Insert repoToken before current if its maturity is less than or equal
             if (maturityToInsert < currentMaturity) {
diff --git a/src/Strategy.sol b/src/Strategy.sol
index 41003347..057eb274 100644
--- a/src/Strategy.sol
+++ b/src/Strategy.sol
@@ -999,13 +999,17 @@ contract Strategy is BaseStrategy, Pausable, ReentrancyGuard {
         }
 
         // Validate and insert the repoToken into the list, retrieve auction rate and redemption timestamp
-        (, uint256 redemptionTimestamp) = repoTokenListData
+        (bool isRepoTokenValid , , uint256 redemptionTimestamp) = repoTokenListData
             .validateAndInsertRepoToken(
                 ITermRepoToken(repoToken),
                 discountRateAdapter,
                 address(asset)
             );
 
+        if (!isRepoTokenValid) {
+                revert RepoTokenList.InvalidRepoToken(repoToken);
+        }
+
         // Sweep assets and redeem repoTokens, if needed
         _redeemRepoTokens(0);
 
diff --git a/src/TermAuctionList.sol b/src/TermAuctionList.sol
index 1412d0f9..3cdaf430 100644
--- a/src/TermAuctionList.sol
+++ b/src/TermAuctionList.sol
@@ -13,7 +13,7 @@ struct PendingOffer {
     address repoToken;
     uint256 offerAmount;
     ITermAuction termAuction;
-    ITermAuctionOfferLocker offerLocker;   
+    ITermAuctionOfferLocker offerLocker;
 }
 
 struct TermAuctionListNode {
@@ -33,7 +33,7 @@ struct TermAuctionListData {
 library TermAuctionList {
     using RepoTokenList for RepoTokenListData;
 
-    bytes32 public constant NULL_NODE = bytes32(0);    
+    bytes32 public constant NULL_NODE = bytes32(0);
 
     /*//////////////////////////////////////////////////////////////
                         PRIVATE FUNCTIONS
@@ -84,8 +84,8 @@ library TermAuctionList {
             while (current != NULL_NODE) {
                 offers[i++] = current;
                 current = _getNext(listData, current);
-            } 
-        }   
+            }
+        }
     }
 
     /**
@@ -94,11 +94,12 @@ library TermAuctionList {
      * @param offerId The ID of the offer to be inserted
      * @param pendingOffer The `PendingOffer` struct containing details of the offer to be inserted
      *
-     * @dev This function inserts a new pending offer while maintaining the list sorted by auction address. 
-     * The function iterates through the list to find the correct position for the new `offerId` and updates the pointers accordingly.     
+     * @dev This function inserts a new pending offer while maintaining the list sorted by auction address.
+     * The function iterates through the list to find the correct position for the new `offerId` and updates the pointers accordingly.
      */
     function insertPending(TermAuctionListData storage listData, bytes32 offerId, PendingOffer memory pendingOffer) internal {
         bytes32 current = listData.head;
+        require(!pendingOffer.termAuction.auctionCompleted());
 
         // If the list is empty, set the new repoToken as the head
         if (current == NULL_NODE) {
@@ -119,7 +120,7 @@ library TermAuctionList {
             address currentAuction = address(listData.offers[current].termAuction);
             address auctionToInsert = address(pendingOffer.termAuction);
 
-            // Insert repoToken before current if its maturity is less than or equal
+            // Insert offer before current if the auction address to insert is less than current auction address
             if (auctionToInsert < currentAuction) {
                 if (prev == NULL_NODE) {
                     listData.head = offerId;
@@ -132,7 +133,7 @@ library TermAuctionList {
 
             // Move to the next node
             bytes32 next = _getNext(listData, current);
-            
+
             // If at the end of the list, insert repoToken after current
             if (next == NULL_NODE) {
                 listData.nodes[current].next = offerId;
@@ -158,7 +159,7 @@ library TermAuctionList {
      * the list by clearing out inactive offers and ensuring repoTokens are correctly processed.
      */
     function removeCompleted(
-        TermAuctionListData storage listData, 
+        TermAuctionListData storage listData,
         RepoTokenListData storage repoTokenListData,
         ITermDiscountRateAdapter discountRateAdapter,
         address asset
@@ -172,53 +173,51 @@ library TermAuctionList {
             PendingOffer memory offer = listData.offers[current];
             bytes32 next = _getNext(listData, current);
 
-            uint256 offerAmount = offer.offerLocker.lockedOffer(current).amount;
+            uint256 offerAmount = offer.offerLocker.lockedOfferAmount(current);
             bool removeNode;
             bool insertRepoToken;
 
             if (offer.termAuction.auctionCompleted()) {
                 // If auction is completed and closed, mark for removal and prepare to insert repo token
                 removeNode = true;
-                (insertRepoToken, ) = repoTokenListData.validateRepoToken(ITermRepoToken(offer.repoToken), asset);
+                // Auction still open => include offerAmount in totalValue 
+                // (otherwise locked purchaseToken will be missing from TV)               
+                // Auction completed but not closed => include offer.offerAmount in totalValue 
+                // because the offerLocker will have already removed the offer. 
+                // This applies if the repoToken hasn't been added to the repoTokenList 
+                // (only for new auctions, not reopenings).  
+                repoTokenListData.validateAndInsertRepoToken(
+                    ITermRepoToken(offer.repoToken), discountRateAdapter, asset
+                );
             } else {
-                if (offerAmount == 0) {
-                    // If offer amount is zero, it indicates the auction was canceled or deleted
-                    removeNode = true;
-                } else {
-                    // Otherwise, do nothing if the offer is still pending
-                }
-
                 if (offer.termAuction.auctionCancelledForWithdrawal()) {
                     // If auction was canceled for withdrawal, remove the node and unlock offers manually
-                    removeNode = true;                  
                     bytes32[] memory offerIds = new bytes32[](1);
                     offerIds[0] = current;
-                    offer.offerLocker.unlockOffers(offerIds); // unlocking offer in this scenario withdraws offer amount
+                    try offer.offerLocker.unlockOffers(offerIds) { // unlocking offer in this scenario withdraws offer amount
+                        removeNode = true;
+                    } catch {
+                        removeNode = false;
+                    }
+                } else {
+                    if (offerAmount == 0) {
+                    // If offer amount is zero, it indicates the auction was canceled or deleted
+                    removeNode = true;
+                    }
                 }
             }
 
             if (removeNode) {
                 // Update the list to remove the current node
+                delete listData.nodes[current];
+                delete listData.offers[current];
                 if (current == listData.head) {
                     listData.head = next;
                 }
-                
-                listData.nodes[prev].next = next;
-                delete listData.nodes[current];
-                delete listData.offers[current];
-            }
-
-            if (insertRepoToken) {
-
-                // Auction still open => include offerAmount in totalValue 
-                // (otherwise locked purchaseToken will be missing from TV)               
-                // Auction completed but not closed => include offer.offerAmount in totalValue 
-                // because the offerLocker will have already removed the offer. 
-                // This applies if the repoToken hasn't been added to the repoTokenList 
-                // (only for new auctions, not reopenings).  
-                repoTokenListData.validateAndInsertRepoToken(
-                    ITermRepoToken(offer.repoToken), discountRateAdapter, asset
-                );
+                else {
+                    listData.nodes[prev].next = next;
+                    current = prev;
+                }
             }
 
             // Move to the next node
@@ -239,10 +238,10 @@ library TermAuctionList {
      * @dev This function calculates the present value of offers in the list. If `repoTokenToMatch` is provided,
      * it will filter the calculations to include only the specified repoToken. If `repoTokenToMatch` is not provided,
      * it will aggregate the present value of all repoTokens in the list. This provides flexibility for both aggregate
-     * and specific token evaluations.     
+     * and specific token evaluations.
      */
     function getPresentValue(
-        TermAuctionListData storage listData, 
+        TermAuctionListData storage listData,
         RepoTokenListData storage repoTokenListData,
         ITermDiscountRateAdapter discountRateAdapter,
         uint256 purchaseTokenPrecision,
@@ -264,7 +263,7 @@ library TermAuctionList {
                 continue;
             }
 
-            uint256 offerAmount = offer.offerLocker.lockedOffer(current).amount;            
+            uint256 offerAmount = offer.offerLocker.lockedOfferAmount(current);
 
             // Handle new or unseen repo tokens
             /// @dev offer processed, but auctionClosed not yet called and auction is new so repoToken not on List and wont be picked up
@@ -272,15 +271,15 @@ library TermAuctionList {
             if (repoTokenListData.discountRates[offer.repoToken] == 0 && offer.termAuction.auctionCompleted()) {
                 if (edgeCaseAuction != address(offer.termAuction)) {
                     uint256 repoTokenAmountInBaseAssetPrecision = RepoTokenUtils.getNormalizedRepoTokenAmount(
-                        offer.repoToken, 
+                        offer.repoToken,
                         ITermRepoToken(offer.repoToken).balanceOf(address(this)),
                         purchaseTokenPrecision,
                         discountRateAdapter.repoRedemptionHaircut(offer.repoToken)
                     );
                     totalValue += RepoTokenUtils.calculatePresentValue(
-                        repoTokenAmountInBaseAssetPrecision, 
-                        purchaseTokenPrecision, 
-                        RepoTokenList.getRepoTokenMaturity(offer.repoToken), 
+                        repoTokenAmountInBaseAssetPrecision,
+                        purchaseTokenPrecision,
+                        RepoTokenList.getRepoTokenMaturity(offer.repoToken),
                         discountRateAdapter.getDiscountRate(offer.repoToken)
                     );
 
@@ -296,7 +295,7 @@ library TermAuctionList {
 
             // Move to the next token in the list
             current = _getNext(listData, current);
-        }        
+        }
     }
 
     /**
@@ -305,7 +304,7 @@ library TermAuctionList {
      * @param repoTokenListData The repoToken list data
      * @param discountRateAdapter The discount rate adapter
      * @param repoToken The address of the repoToken (optional)
-     * @param newOfferAmount The new offer amount for the specified repoToken 
+     * @param newOfferAmount The new offer amount for the specified repoToken
      * @param purchaseTokenPrecision The precision of the purchase token
      * @return cumulativeWeightedTimeToMaturity The cumulative weighted time to maturity
      * @return cumulativeOfferAmount The cumulative repoToken amount
@@ -314,13 +313,13 @@ library TermAuctionList {
      * @dev This function calculates cumulative data for all offers in the list. The `repoToken` and `newOfferAmount`
      * parameters are optional and provide flexibility to include the newOfferAmount for a specified repoToken in the calculation.
      * If `repoToken` is set to `address(0)` or `newOfferAmount` is `0`, the function calculates the cumulative data
-     * without adjustments. 
+     * without adjustments.
      */
     function getCumulativeOfferData(
         TermAuctionListData storage listData,
         RepoTokenListData storage repoTokenListData,
         ITermDiscountRateAdapter discountRateAdapter,
-        address repoToken, 
+        address repoToken,
         uint256 newOfferAmount,
         uint256 purchaseTokenPrecision
     ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount, bool found) {
@@ -339,16 +338,16 @@ library TermAuctionList {
                 found = true;
             } else {
                 // Retrieve the current offer amount from the offer locker
-                offerAmount = offer.offerLocker.lockedOffer(current).amount;
+                offerAmount = offer.offerLocker.lockedOfferAmount(current);
 
                 // Handle new repo tokens or reopening auctions
                 /// @dev offer processed, but auctionClosed not yet called and auction is new so repoToken not on List and wont be picked up
                 /// checking repoTokendiscountRates to make sure we are not double counting on re-openings
                 if (repoTokenListData.discountRates[offer.repoToken] == 0 && offer.termAuction.auctionCompleted()) {
                     // use normalized repoToken amount if repoToken is not in the list
-                    if (edgeCaseAuction != address(offer.termAuction)) {                    
+                    if (edgeCaseAuction != address(offer.termAuction)) {
                         offerAmount = RepoTokenUtils.getNormalizedRepoTokenAmount(
-                            offer.repoToken, 
+                            offer.repoToken,
                             ITermRepoToken(offer.repoToken).balanceOf(address(this)),
                             purchaseTokenPrecision,
                             discountRateAdapter.repoRedemptionHaircut(offer.repoToken)
@@ -367,12 +366,12 @@ library TermAuctionList {
                 // Calculate weighted time to maturity
                 uint256 weightedTimeToMaturity = RepoTokenList.getRepoTokenWeightedTimeToMaturity(
                     offer.repoToken, offerAmount
-                );            
+                );
 
                 cumulativeWeightedTimeToMaturity += weightedTimeToMaturity;
                 cumulativeOfferAmount += offerAmount;
             }
-            
+
             // Move to the next token in the list
             current = _getNext(listData, current);
         }
diff --git a/src/interfaces/term/ITermAuctionOfferLocker.sol b/src/interfaces/term/ITermAuctionOfferLocker.sol
index 64343d3c..208b2404 100644
--- a/src/interfaces/term/ITermAuctionOfferLocker.sol
+++ b/src/interfaces/term/ITermAuctionOfferLocker.sol
@@ -50,6 +50,8 @@ interface ITermAuctionOfferLocker {
 
     function lockedOffer(bytes32 id) external view returns (TermAuctionOffer memory);
 
+    function lockedOfferAmount(bytes32 id) external view returns (uint256);
+
     /// @param offerSubmissions An array of offer submissions
     /// @return A bytes32 array of unique on chain offer ids.
     function lockOffers(
diff --git a/src/test/kontrol/Constants.sol b/src/test/kontrol/Constants.sol
new file mode 100644
index 00000000..e675d5c6
--- /dev/null
+++ b/src/test/kontrol/Constants.sol
@@ -0,0 +1,4 @@
+pragma solidity 0.8.23;
+
+uint256 constant ETH_UPPER_BOUND = 2 ** 95;
+uint256 constant TIME_UPPER_BOUND = 2 ** 35;
diff --git a/src/test/kontrol/Counterexamples.t.sol b/src/test/kontrol/Counterexamples.t.sol
new file mode 100644
index 00000000..070db6b3
--- /dev/null
+++ b/src/test/kontrol/Counterexamples.t.sol
@@ -0,0 +1,68 @@
+pragma solidity 0.8.23;
+
+import "forge-std/Vm.sol";
+import "forge-std/Test.sol";
+
+import {ERC20Mock} from "@openzeppelin/contracts/mocks/ERC20Mock.sol";
+
+import "src/RepoTokenList.sol";
+
+import {MockTermRepoToken} from "src/test/mocks/MockTermRepoToken.sol";
+import {MockUSDC} from "src/test/mocks/MockUSDC.sol";
+
+/**
+ * Unit tests testing counterexamples for list invariants and other properties
+ * found during formal verification. These tests would fail before the issues
+ * were fixed, but should be passing after.
+ */
+contract CounterexamplesTest is Test {
+    using RepoTokenList for RepoTokenListData;
+
+    RepoTokenListData _listData;
+
+    /**
+     * Scenario: RepoTokenList is repoToken1 -> repoToken2 -> NULL_NODE, where
+     * both tokens have the same maturity. We try to insert repoToken2 again.
+     *
+     * Before: repoToken2 was being inserted before the first token found with the
+     * same maturity, making the list repoToken2 -> repoToken1 -> repoToken2 ->
+     * repoToken1 -> ... and creating a cycle.
+     *
+     * After: A token is inserted only after all other tokens with the same
+     * maturity. Therefore, the function continues past repoToken1 and sees that
+     * repoToken2 is already in the list, avoiding inserting it again.
+     */
+    function testInsertSortedNoCycleCounterexample() external {
+        MockUSDC mockUSDC = new MockUSDC();
+        ERC20Mock mockCollateral = new ERC20Mock();
+
+        // Deploy two repo tokens with the same maturity date
+        MockTermRepoToken repoToken1 = new MockTermRepoToken(
+            bytes32("test repo token 1"), address(mockUSDC), address(mockCollateral), 1e18, block.timestamp + 1 weeks
+        );
+        MockTermRepoToken repoToken2 = new MockTermRepoToken(
+            bytes32("test repo token 2"), address(mockUSDC), address(mockCollateral), 1e18, block.timestamp + 1 weeks
+        );
+
+        // Initialize list to repoToken1 -> repoToken2 -> NULL_NODE
+        _listData.head = address(repoToken1);
+        _listData.nodes[address(repoToken1)].next = address(repoToken2);
+        _listData.nodes[address(repoToken2)].next = RepoTokenList.NULL_NODE;
+
+        // Try to insert repoToken2 again, shouldn't change the list
+        _listData.insertSorted(address(repoToken2));
+
+        address previous = RepoTokenList.NULL_NODE;
+        address current = _listData.head;
+
+        // Check that no next pointers point to the previous node
+        while (current != RepoTokenList.NULL_NODE) {
+            address next = _listData.nodes[current].next;
+
+            assert(next != previous);
+
+            previous = current;
+            current = next;
+        }
+    }
+}
diff --git a/src/test/kontrol/KontrolTest.sol b/src/test/kontrol/KontrolTest.sol
new file mode 100644
index 00000000..1cb57cba
--- /dev/null
+++ b/src/test/kontrol/KontrolTest.sol
@@ -0,0 +1,63 @@
+pragma solidity 0.8.23;
+
+import "forge-std/Vm.sol";
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+contract KontrolTest is Test, KontrolCheats {
+    // Note: there are lemmas dependent on `ethUpperBound`
+    uint256 constant ethMaxWidth = 96;
+    uint256 constant ethUpperBound = 2 ** ethMaxWidth;
+    // Note: 2 ** 35 takes us to year 3058
+    uint256 constant timeUpperBound = 2 ** 35;
+
+    function infoAssert(bool condition, string memory message) external {
+        if (!condition) {
+            revert(message);
+        }
+    }
+
+    enum Mode {
+        Assume,
+        Try,
+        Assert
+    }
+
+    function _establish(Mode mode, bool condition) internal pure returns (bool) {
+        if (mode == Mode.Assume) {
+            vm.assume(condition);
+            return true;
+        } else if (mode == Mode.Try) {
+            return condition;
+        } else {
+            assert(condition);
+            return true;
+        }
+    }
+
+    function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) {
+        return uint256(vm.load(contractAddress, bytes32(slot)));
+    }
+
+    function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) {
+        return address(uint160(uint256(vm.load(contractAddress, bytes32(slot)))));
+    }
+
+    function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal {
+        vm.store(contractAddress, bytes32(slot), value);
+    }
+
+    function _storeUInt256(address contractAddress, uint256 slot, uint256 value) internal {
+        vm.store(contractAddress, bytes32(slot), bytes32(value));
+    }
+
+    function _storeAddress(address contractAddress, uint256 slot, address value) internal {
+        vm.store(contractAddress, bytes32(slot), bytes32(uint256(uint160(value))));
+    }
+
+    function _assumeNoOverflow(uint256 augend, uint256 addend) internal {
+        unchecked {
+            vm.assume(augend < augend + addend);
+        }
+    }
+}
diff --git a/src/test/kontrol/RepoToken.sol b/src/test/kontrol/RepoToken.sol
new file mode 100644
index 00000000..a5d09a85
--- /dev/null
+++ b/src/test/kontrol/RepoToken.sol
@@ -0,0 +1,98 @@
+pragma solidity 0.8.23;
+
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+import "src/interfaces/term/ITermRepoServicer.sol";
+import "src/interfaces/term/ITermRepoToken.sol";
+
+import "src/test/kontrol/Constants.sol";
+import "src/test/kontrol/TermRepoCollateralManager.sol";
+import "src/test/kontrol/TermRepoServicer.sol";
+
+contract RepoToken is ITermRepoToken, KontrolTest {
+    mapping(address => uint256) _balance;
+    uint256 _redemptionTimestamp;
+    uint256 _redemptionValue;
+    TermRepoServicer _termRepoServicer;
+    TermRepoCollateralManager _termRepoCollateralManager;
+    address _purchaseToken;
+
+    uint256 private constant termRepoServicerSlot = 30;
+    uint256 private constant termRepoCollateralManagerSlot = 31;
+
+    function initializeSymbolic() public {
+        kevm.symbolicStorage(address(this));
+
+        uint256 senderBalance = freshUInt256();
+        vm.assume(senderBalance < ETH_UPPER_BOUND);
+        _balance[msg.sender] = senderBalance;
+
+        _redemptionTimestamp = freshUInt256();
+        vm.assume(_redemptionTimestamp < TIME_UPPER_BOUND);
+
+        _purchaseToken = kevm.freshAddress();
+
+        _redemptionValue = freshUInt256();
+        vm.assume(_redemptionValue < ETH_UPPER_BOUND);
+
+        TermRepoServicer termRepoServicer = new TermRepoServicer();
+        termRepoServicer.initializeSymbolic(address(this));
+        _storeUInt256(address(this), termRepoServicerSlot, uint256(uint160(address(termRepoServicer))));
+
+        TermRepoCollateralManager termRepoCollateralManager = new TermRepoCollateralManager();
+        termRepoCollateralManager.initializeSymbolic();
+        _storeUInt256(address(this), termRepoCollateralManagerSlot, uint256(uint160(address(termRepoCollateralManager))));
+    }
+
+    function decimals() public view returns (uint8) {
+        return 18;
+    }
+
+    function balanceOf(address account) public view returns (uint256) {
+        return _balance[account];
+    }
+
+    function redemptionValue() external view returns (uint256) {
+        return _redemptionValue;
+    }
+
+    function config() external view returns (
+        uint256 redemptionTimestamp,
+        address purchaseToken,
+        address termRepoServicer,
+        address termRepoCollateralManager
+    ) {
+        redemptionTimestamp = _redemptionTimestamp;
+        purchaseToken = _purchaseToken;
+        termRepoServicer = address(_termRepoServicer);
+        termRepoCollateralManager = address(_termRepoCollateralManager);
+    }
+
+    function termRepoId() external view returns (bytes32) {
+        return bytes32(freshUInt256());
+    }
+
+    function allowance(address owner, address spender) external view returns (uint256) {
+        return freshUInt256();
+    }
+
+    function approve(address spender, uint256 amount) external returns (bool) {
+        kevm.symbolicStorage(address(this));
+        return kevm.freshBool() > 0;
+    }
+
+    function totalSupply() external view returns (uint256) {
+        return freshUInt256();
+    }
+
+    function transfer(address to, uint256 amount) external returns (bool) {
+        kevm.symbolicStorage(address(this));
+        return kevm.freshBool() > 0;
+    }
+
+    function transferFrom(address from, address to, uint256 amount) external returns (bool) {
+        kevm.symbolicStorage(address(this));
+        return kevm.freshBool() > 0;
+    }
+}
diff --git a/src/test/kontrol/RepoTokenListInvariants.t.sol b/src/test/kontrol/RepoTokenListInvariants.t.sol
new file mode 100644
index 00000000..d753dc28
--- /dev/null
+++ b/src/test/kontrol/RepoTokenListInvariants.t.sol
@@ -0,0 +1,328 @@
+pragma solidity 0.8.23;
+
+import "forge-std/Vm.sol";
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+import "src/RepoTokenList.sol";
+
+import "src/test/kontrol/Constants.sol";
+import "src/test/kontrol/RepoToken.sol";
+
+contract RepoTokenListInvariantsTest is KontrolTest {
+    using RepoTokenList for RepoTokenListData;
+
+    RepoTokenListData _repoTokenList;
+
+    function setUp() public {
+        // Make storage of this contract completely symbolic
+        kevm.symbolicStorage(address(this));
+
+        // Initialize RepoTokenList of arbitrary size
+        _initializeRepoTokenList();
+    }
+
+    /**
+     * Deploy a new RepoToken with symbolic storage.
+     */
+    function _newRepoToken() internal returns (address) {
+        RepoToken repoToken = new RepoToken();
+        repoToken.initializeSymbolic();
+
+        return address(repoToken);
+    }
+
+    /**
+     * Return the maturity timestamp of the given RepoToken.
+     */
+    function _getRepoTokenMaturity(address repoToken) internal returns (uint256 redemptionTimestamp) {
+        (redemptionTimestamp, , ,) = ITermRepoToken(repoToken).config();
+    }
+
+    /**
+     * Return the this contract's balance in the given RepoToken.
+     */
+    function _getRepoTokenBalance(address repoToken) internal returns (uint256) {
+        return ITermRepoToken(repoToken).balanceOf(address(this));
+    }
+
+    /**
+     * Initialize _repoTokenList to a RepoTokenList of arbitrary size, where all
+     * items are distinct RepoTokens with symbolic storage.
+     */
+    function _initializeRepoTokenList() internal {
+        address previous = RepoTokenList.NULL_NODE;
+
+        while (kevm.freshBool() != 0) {
+            address current = _newRepoToken();
+
+            if (previous == RepoTokenList.NULL_NODE) {
+                _repoTokenList.head = current;
+            } else {
+                _repoTokenList.nodes[previous].next = current;
+            }
+
+            previous = current;
+        }
+
+        if (previous == RepoTokenList.NULL_NODE) {
+            _repoTokenList.head = RepoTokenList.NULL_NODE;
+        } else {
+            _repoTokenList.nodes[previous].next = RepoTokenList.NULL_NODE;
+        }
+    }
+
+    /**
+     * Assume or assert that the tokens in the list are sorted by maturity.
+     */
+    function _establishSortedByMaturity(Mode mode) internal {
+        address previous = RepoTokenList.NULL_NODE;
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            if (previous != RepoTokenList.NULL_NODE) {
+                uint256 previousMaturity = _getRepoTokenMaturity(previous);
+                uint256 currentMaturity = _getRepoTokenMaturity(current);
+                _establish(mode, previousMaturity <= currentMaturity);
+            }
+
+            previous = current;
+            current = _repoTokenList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that there are no duplicate tokens in the list.
+     */
+    function _establishNoDuplicateTokens(Mode mode) internal {
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            address other = _repoTokenList.nodes[current].next;
+
+            while (other != RepoTokenList.NULL_NODE) {
+                _establish(mode, current != other);
+                other = _repoTokenList.nodes[other].next;
+            }
+
+            current = _repoTokenList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that there are no tokens in the list have matured
+     * (i.e. all token maturities are greater than the current timestamp).
+     */
+    function _establishNoMaturedTokens(Mode mode) internal {
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            uint256 currentMaturity = _getRepoTokenMaturity(current);
+
+            _establish(mode, block.timestamp < currentMaturity);
+
+            current = _repoTokenList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that all tokens in the list have balance > 0.
+     */
+    function _establishPositiveBalance(Mode mode) internal {
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            uint256 repoTokenBalance = _getRepoTokenBalance(current);
+
+            _establish(mode, 0 < repoTokenBalance);
+
+            current = _repoTokenList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Weaker version of the above invariant that allows matured tokens to have
+     * a balance of 0.
+     *
+     * Note: This is equivalent to the above invariant if the NoMaturedTokens
+     * invariant also holds.
+     */
+    function _establishPositiveBalanceForNonMaturedTokens(Mode mode) internal {
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            uint256 currentMaturity = _getRepoTokenMaturity(current);
+            uint256 repoTokenBalance = _getRepoTokenBalance(current);
+
+            if (block.timestamp < currentMaturity) {
+                _establish(mode, 0 < repoTokenBalance);
+            }
+
+            current = _repoTokenList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Count the number of nodes in the list.
+     *
+     * Note that this function guarantees the following postconditions:
+     * - The head of the list is NULL_NODE iff the count is 0.
+     * - If the count is N, the Nth node in the list is followed by NULL_NODE.
+     */
+    function _countNodesInList() internal returns (uint256) {
+        uint256 count = 0;
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            ++count;
+            current = _repoTokenList.nodes[current].next;
+        }
+
+        return count;
+    }
+
+    /**
+     * Return true if the given RepoToken is in the list, and false otherwise.
+     */
+    function _repoTokenInList(address repoToken) internal returns (bool) {
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            if (current == repoToken) {
+                return true;
+            }
+
+            current = _repoTokenList.nodes[current].next;
+        }
+
+        return false;
+    }
+
+    /**
+     * Test that insertSorted preserves the list invariants when a new RepoToken
+     * is added (that was not present in the list before).
+     */
+    function testInsertSortedNewToken() external {
+        // Our initialization procedure guarantees this invariant,
+        // so we assert instead of assuming
+        _establishNoDuplicateTokens(Mode.Assert);
+
+        // Assume that the invariants are satisfied before the function is called
+        _establishSortedByMaturity(Mode.Assume);
+        _establishNoMaturedTokens(Mode.Assume);
+        _establishPositiveBalance(Mode.Assume);
+
+        // Save the number of tokens in the list before the function is called
+        uint256 count = _countNodesInList();
+
+        // Generate a new RepoToken with symbolic storage
+        address repoToken = _newRepoToken();
+        uint256 maturity = _getRepoTokenMaturity(repoToken);
+        uint256 balance = _getRepoTokenBalance(repoToken);
+        vm.assume(block.timestamp < maturity);
+        vm.assume(0 < balance);
+
+        // Call the function being tested
+        _repoTokenList.insertSorted(repoToken);
+
+
+        // Assert that the size of the list increased by 1
+        assert(_countNodesInList() == count + 1);
+
+        // Assert that the new RepoToken is in the list
+        assert(_repoTokenInList(repoToken));
+
+        // Assert that the invariants are preserved
+        _establishSortedByMaturity(Mode.Assert);
+        _establishNoDuplicateTokens(Mode.Assert);
+        _establishNoMaturedTokens(Mode.Assert);
+        _establishPositiveBalance(Mode.Assert);
+    }
+
+    /**
+     * Test that insertSorted preserves the list invariants when trying to
+     * insert a RepoToken that is already in the list.
+     */
+    function testInsertSortedDuplicateToken(
+        address repoToken
+    ) external {
+        // Our initialization procedure guarantees this invariant,
+        // so we assert instead of assuming
+        _establishNoDuplicateTokens(Mode.Assert);
+
+        // Assume that the invariants are satisfied before the function is called
+        _establishSortedByMaturity(Mode.Assume);
+        _establishNoMaturedTokens(Mode.Assume);
+        _establishPositiveBalance(Mode.Assume);
+
+        // Save the number of tokens in the list before the function is called
+        uint256 count = _countNodesInList();
+
+        // Assume that the RepoToken is already in the list
+        vm.assume(_repoTokenInList(repoToken));
+
+        // Call the function being tested
+        _repoTokenList.insertSorted(repoToken);
+
+        // Assert that the size of the list didn't change
+        assert(_countNodesInList() == count);
+
+        // Assert that the RepoToken is still in the list
+        assert(_repoTokenInList(repoToken));
+
+        // Assert that the invariants are preserved
+        _establishSortedByMaturity(Mode.Assert);
+        _establishNoDuplicateTokens(Mode.Assert);
+        _establishNoMaturedTokens(Mode.Assert);
+        _establishPositiveBalance(Mode.Assert);
+    }
+
+    /**
+     * Configure the model of the RepoServicer for every token in the list to
+     * follow the assumption that redeemTermRepoTokens will not revert.
+     */
+    function _guaranteeRedeemAlwaysSucceeds() internal {
+        address current = _repoTokenList.head;
+
+        while (current != RepoTokenList.NULL_NODE) {
+            (, , address repoServicer,) = ITermRepoToken(current).config();
+            TermRepoServicer(repoServicer).guaranteeRedeemAlwaysSucceeds();
+
+            current = _repoTokenList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Test that removeAndRedeemMaturedTokens preserves the list invariants.
+     */
+    function testRemoveAndRedeemMaturedTokens() external {
+        // Save the number of tokens in the list before the function is called
+        uint256 count = _countNodesInList();
+
+        // Our initialization procedure guarantees this invariant,
+        // so we assert instead of assuming
+        _establishNoDuplicateTokens(Mode.Assert);
+
+        // Assume that the invariants are satisfied before the function is called
+        _establishSortedByMaturity(Mode.Assume);
+        _establishNoDuplicateTokens(Mode.Assume);
+        _establishPositiveBalanceForNonMaturedTokens(Mode.Assume);
+
+        // Assume that the call to redeemTermRepoTokens will not revert
+        _guaranteeRedeemAlwaysSucceeds();
+
+        // Call the function being tested
+        _repoTokenList.removeAndRedeemMaturedTokens();
+
+        // Assert that the size of the list is less than or equal to before
+        assert(_countNodesInList() <= count);
+
+        // Assert that the invariants are preserved
+        _establishSortedByMaturity(Mode.Assert);
+        _establishNoDuplicateTokens(Mode.Assert);
+
+        // Now the following invariants should hold as well
+        _establishNoMaturedTokens(Mode.Assert);
+        _establishPositiveBalance(Mode.Assert);
+    }
+}
diff --git a/src/test/kontrol/TermAuction.sol b/src/test/kontrol/TermAuction.sol
new file mode 100644
index 00000000..ed38062b
--- /dev/null
+++ b/src/test/kontrol/TermAuction.sol
@@ -0,0 +1,41 @@
+pragma solidity 0.8.23;
+
+import "src/interfaces/term/ITermAuction.sol";
+
+import "src/test/kontrol/Constants.sol";
+import "src/test/kontrol/KontrolTest.sol";
+
+contract TermAuction is ITermAuction, KontrolTest {
+    bool _auctionCompleted;
+    bool _auctionCancelledForWithdrawal;
+
+    uint256 private constant auctionSlot = 27;
+
+    function initializeSymbolic() public {
+        kevm.symbolicStorage(address(this));
+        // Clear the slot that holds two contract fields
+        _storeUInt256(address(this), auctionSlot, 0);
+        _auctionCompleted = kevm.freshBool() != 0;
+        _auctionCancelledForWithdrawal = kevm.freshBool() != 0;
+    }
+
+    function termAuctionOfferLocker() external view returns (address) {
+        return kevm.freshAddress();
+    }
+
+    function termRepoId() external view returns (bytes32) {
+        return bytes32(freshUInt256());
+    }
+
+    function auctionEndTime() external view returns (uint256) {
+        return freshUInt256();
+    }
+
+    function auctionCompleted() external view returns (bool) {
+        return _auctionCompleted;
+    }
+
+    function auctionCancelledForWithdrawal() external view returns (bool) {
+        return _auctionCancelledForWithdrawal;
+    }
+}
diff --git a/src/test/kontrol/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol
new file mode 100644
index 00000000..5df500ff
--- /dev/null
+++ b/src/test/kontrol/TermAuctionListInvariants.t.sol
@@ -0,0 +1,552 @@
+pragma solidity 0.8.23;
+
+import "forge-std/Vm.sol";
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+import "src/RepoTokenList.sol";
+import "src/TermAuctionList.sol";
+
+import "src/test/kontrol/Constants.sol";
+import "src/test/kontrol/RepoToken.sol";
+import "src/test/kontrol/RepoTokenListInvariants.t.sol";
+import "src/test/kontrol/TermAuction.sol";
+import "src/test/kontrol/TermAuctionOfferLocker.sol";
+import "src/test/kontrol/TermDiscountRateAdapter.sol";
+
+contract TermAuctionListInvariantsTest is KontrolTest {
+    using TermAuctionList for TermAuctionListData;
+
+    TermAuctionListData _termAuctionList;
+    address _referenceAuction;
+    RepoTokenListData _repoTokenList;
+
+    uint256 private constant auctionListSlot = 27;
+    uint256 private constant referenceAuctionSlot = 30;
+
+    function setUp() public {
+        // Make storage of this contract completely symbolic
+        kevm.symbolicStorage(address(this));
+
+        // We will copy the code of this deployed auction contract
+        // into all auctions in the list
+        _storeUInt256(address(this), referenceAuctionSlot, uint256(uint160(address(new TermAuction()))));
+
+        // Initialize TermAuctionList of arbitrary size
+        _initializeTermAuctionList();
+    }
+
+    function auctionListOfferSlot(bytes32 offerId) internal view returns (uint256) {
+        return uint256(keccak256(abi.encodePacked(uint256(offerId), uint256(auctionListSlot + 2))));
+    }
+
+    /**
+     * Set pending offer using slot manipulation directly
+     */
+    function setPendingOffer(bytes32 offerId, address repoToken, uint256 offerAmount, address auction, address offerLocker) internal {
+        uint256 offerSlot = auctionListOfferSlot(offerId);
+        _storeUInt256(address(this), offerSlot, uint256(uint160(repoToken)));
+        _storeUInt256(address(this), offerSlot + 1, offerAmount);
+        _storeUInt256(address(this), offerSlot + 2, uint256(uint160(auction)));
+        _storeUInt256(address(this), offerSlot + 3, uint256(uint160(offerLocker)));
+    }
+
+    /**
+     * Return the auction for a given offer in the list.
+     */
+    function _getAuction(bytes32 offerId) internal returns(address) {
+        return address(_termAuctionList.offers[offerId].termAuction);
+    }
+
+    /**
+     * Deploy & initialize RepoToken and OfferLocker with the same RepoServicer
+     */
+    function newRepoTokenAndOfferLocker() public returns (
+        RepoToken repoToken,
+        TermAuctionOfferLocker offerLocker
+    ) {
+        repoToken = new RepoToken();
+        repoToken.initializeSymbolic();
+        (, , address termRepoServicer,) = repoToken.config();
+
+        offerLocker = new TermAuctionOfferLocker();
+        offerLocker.initializeSymbolic(termRepoServicer);
+    }
+
+    /**
+     * Initialize _termAuctionList to a TermAuctionList of arbitrary size,
+     * comprised of offers with distinct ids.
+     */
+    function _initializeTermAuctionList() internal {
+        bytes32 previous = TermAuctionList.NULL_NODE;
+        uint256 count = 0;
+
+        while (kevm.freshBool() != 0) {
+            (RepoToken repoToken, TermAuctionOfferLocker offerLocker) =
+                this.newRepoTokenAndOfferLocker();
+
+            // Assign each offer an ID based on Strategy._generateOfferId()
+            bytes32 current = keccak256(
+                abi.encodePacked(count, address(this), address(offerLocker))
+            );
+            // Register offer in offer locker
+            offerLocker.initializeSymbolicLockedOfferFor(current);
+
+            if (previous == TermAuctionList.NULL_NODE) {
+                _termAuctionList.head = current;
+            } else {
+                _termAuctionList.nodes[previous].next = current;
+            }
+
+            // Create sequential addresses to ensure that list is sorted
+            address auction = address(uint160(1000 + 2 * count));
+            // Etch the code of the auction contract into this address
+            this.etch(auction, _referenceAuction);
+            TermAuction(auction).initializeSymbolic();
+
+            // Build PendingOffer
+            setPendingOffer(current, address(repoToken), freshUInt256(), auction, address(offerLocker));
+
+            previous = current;
+            ++count;
+        }
+
+        if (previous == TermAuctionList.NULL_NODE) {
+            _termAuctionList.head = TermAuctionList.NULL_NODE;
+        } else {
+            _termAuctionList.nodes[previous].next = TermAuctionList.NULL_NODE;
+        }
+    }
+
+    /**
+     * Initialize the TermDiscountRateAdapter to a symbolic state, ensuring that
+     * it has a symbolic discount rate for every token in the PendingOffers.
+     */
+    function _initializeDiscountRateAdapter(
+        TermDiscountRateAdapter discountRateAdapter
+    ) internal {
+        discountRateAdapter.initializeSymbolic();
+
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            address repoToken = _termAuctionList.offers[current].repoToken;
+            discountRateAdapter.initializeSymbolicParamsFor(repoToken);
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that the offers in the list are sorted by auction.
+     */
+    function _establishSortedByAuctionId(Mode mode) internal {
+        bytes32 previous = TermAuctionList.NULL_NODE;
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            if (previous != TermAuctionList.NULL_NODE) {
+                address previousAuction = _getAuction(previous);
+                address currentAuction = _getAuction(current);
+                _establish(mode, previousAuction <= currentAuction);
+            }
+
+            previous = current;
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that there are no duplicate offers in the list.
+     */
+    function _establishNoDuplicateOffers(Mode mode) internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            bytes32 other = _termAuctionList.nodes[current].next;
+
+            while (other != TermAuctionList.NULL_NODE) {
+                _establish(mode, current != other);
+                other = _termAuctionList.nodes[other].next;
+            }
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that there are no completed auctions in the list.
+     */
+    function _establishNoCompletedAuctions(Mode mode) internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            PendingOffer storage offer = _termAuctionList.offers[current];
+            _establish(mode, !offer.termAuction.auctionCompleted());
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that all offer amounts are > 0.
+     */
+    function _establishPositiveOfferAmounts(Mode mode) internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            PendingOffer storage offer = _termAuctionList.offers[current];
+            _establish(mode, 0 < offer.offerAmount);
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume or assert that the offer amounts recorded in the list are the same
+     * as the offer amounts in the offer locker.
+     */
+    function _establishOfferAmountMatchesAmountLocked(Mode mode, bytes32 offerId) internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            if(offerId == 0 || offerId != current) {
+                PendingOffer storage offer = _termAuctionList.offers[current];
+                uint256 offerAmount = offer.offerLocker.lockedOfferAmount(current);
+                _establish(mode, offer.offerAmount == offerAmount);
+            }
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Count the number of offers in the list.
+     *
+     * Note that this function guarantees the following postconditions:
+     * - The head of the list is NULL_NODE iff the count is 0.
+     * - If the count is N, the Nth node in the list is followed by NULL_NODE.
+     */
+    function _countOffersInList() internal returns (uint256) {
+        uint256 count = 0;
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            ++count;
+            current = _termAuctionList.nodes[current].next;
+        }
+
+        return count;
+    }
+
+    /**
+     * Return true if the given offer id is in the list, and false otherwise.
+     */
+    function _offerInList(bytes32 offerId) internal returns (bool) {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            if (current == offerId) {
+                return true;
+            }
+
+            current = _termAuctionList.nodes[current].next;
+        }
+
+        return false;
+    }
+
+    /**
+     * Assume that the address doesn't overlap with any preexisting addresses.
+     * This is necessary in order to use cheatcodes on a symbolic address that
+     * change its code or storage.
+     */
+    function _assumeNewAddress(address freshAddress) internal {
+        vm.assume(10 <= uint160(freshAddress));
+
+        vm.assume(freshAddress != address(this));
+        vm.assume(freshAddress != address(vm));
+        vm.assume(freshAddress != address(kevm));
+
+        vm.assume(freshAddress != address(_referenceAuction));
+
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            PendingOffer storage offer = _termAuctionList.offers[current];
+            (,, address termRepoServicer, address termRepoCollateralManager) =
+                ITermRepoToken(offer.repoToken).config();
+
+            vm.assume(freshAddress != offer.repoToken);
+            vm.assume(freshAddress != address(offer.termAuction));
+            vm.assume(freshAddress != address(offer.offerLocker));
+            vm.assume(freshAddress != termRepoServicer);
+            vm.assume(freshAddress != termRepoCollateralManager);
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Etch the code at a given address to a given address in an external call,
+     * reducing memory consumption in the caller function
+     */
+    function etch(address dest, address src) public {
+      vm.etch(dest, src.code);
+    }
+
+    /**
+     * Test that insertPending preserves the list invariants when a new offer
+     * is added (that was not present in the list before).
+     */
+    function testInsertPendingNewOffer(
+        bytes32 offerId
+    ) external {
+        // offerId must not equal zero, otherwise the linked list breaks
+        // TODO: Does the code protect against this?
+        vm.assume(offerId != TermAuctionList.NULL_NODE);
+
+        // Our initialization procedure guarantees these invariants,
+        // so we assert instead of assuming
+        _establishSortedByAuctionId(Mode.Assert);
+        _establishNoDuplicateOffers(Mode.Assert);
+
+        // Assume that the invariants hold before the function is called
+        _establishOfferAmountMatchesAmountLocked(Mode.Assume, bytes32(0));
+        _establishNoCompletedAuctions(Mode.Assume);
+        _establishPositiveOfferAmounts(Mode.Assume);
+
+        // Save the number of offers in the list before the function is called
+        uint256 count = _countOffersInList();
+
+        // Assume that the auction is a fresh address that doesn't overlap with
+        // any others, then initialize it to contain TermAuction code
+        //
+        // NOTE: The auction address needs to remain symbolic, otherwise its
+        // place in the list will be predetermined and the test won't be general
+        address auction = freshAddress();
+        _assumeNewAddress(auction);
+
+        // Initialize RepoToken and OfferLocker, making sure that the addresses
+        // also don't overlap with the symbolic auction
+        (RepoToken repoToken, TermAuctionOfferLocker offerLocker) =
+            this.newRepoTokenAndOfferLocker();
+        offerLocker.initializeSymbolicLockedOfferFor(offerId);
+        (,, address termRepoServicer, address termRepoCollateralManager) =
+            repoToken.config();
+        vm.assume(0 < offerLocker.lockedOfferAmount(offerId));
+        vm.assume(auction != address(repoToken));
+        vm.assume(auction != address(offerLocker));
+        vm.assume(auction != termRepoServicer);
+        vm.assume(auction != termRepoCollateralManager);
+
+        // Now we can etch the auction in, when all other addresses have been created
+        this.etch(auction, _referenceAuction);
+        TermAuction(auction).initializeSymbolic();
+        vm.assume(!TermAuction(auction).auctionCompleted());
+
+        // Build new PendingOffer
+        PendingOffer memory pendingOffer;
+        pendingOffer.repoToken = address(repoToken);
+        pendingOffer.offerAmount = offerLocker.lockedOfferAmount(offerId);
+        pendingOffer.termAuction = ITermAuction(auction);
+        pendingOffer.offerLocker = ITermAuctionOfferLocker(offerLocker);
+
+        // Assume that the offer is not already in the list
+        vm.assume(!_offerInList(offerId));
+
+        // Call the function being tested
+        _termAuctionList.insertPending(offerId, pendingOffer);
+
+        // Assert that the size of the list increased by 1
+        // NOTE: This assertion breaks if offerId equals zero
+        assert(_countOffersInList() == count + 1);
+
+        // Assert that the new offer is in the list
+        assert(_offerInList(offerId));
+
+        // Assert that the invariants are preserved
+        _establishSortedByAuctionId(Mode.Assert);
+        _establishNoDuplicateOffers(Mode.Assert);
+        _establishNoCompletedAuctions(Mode.Assert);
+        _establishPositiveOfferAmounts(Mode.Assert);
+        _establishOfferAmountMatchesAmountLocked(Mode.Assert, bytes32(0));
+    }
+
+
+    /**
+     * Test that insertPending preserves the list invariants when trying to
+     * insert an offer that is already in the list.
+     */
+    function testInsertPendingDuplicateOffer(
+        bytes32 offerId,
+        PendingOffer memory pendingOffer
+    ) external {
+        // offerId must not equal zero, otherwise the linked list breaks
+        // TODO: Does the code protect against this?
+        vm.assume(offerId != TermAuctionList.NULL_NODE);
+
+        // Save the number of offers in the list before the function is called
+        uint256 count = _countOffersInList();
+
+        // Assume that the offer is already in the list
+        vm.assume(_offerInList(offerId));
+
+        // Our initialization procedure guarantees these invariants,
+        // so we assert instead of assuming
+        _establishSortedByAuctionId(Mode.Assert);
+        _establishNoDuplicateOffers(Mode.Assert);
+
+        // Assume that the invariants hold before the function is called
+        _establishOfferAmountMatchesAmountLocked(Mode.Assume, offerId);
+        _establishNoCompletedAuctions(Mode.Assume);
+        _establishPositiveOfferAmounts(Mode.Assume);
+
+        PendingOffer memory offer = _termAuctionList.offers[offerId];
+        // Calls to the Strategy.submitAuctionOffer need to ensure that the following 2 assumptions hold before the call
+        vm.assume(offer.termAuction == pendingOffer.termAuction);
+        vm.assume(offer.repoToken == address(pendingOffer.repoToken));
+        // This is ensured by the _validateAndGetOfferLocker if the above assumptions hold
+        vm.assume(offer.offerLocker == pendingOffer.offerLocker);
+        // This is being checked by Strategy.submitAuctionOffer
+        vm.assume(pendingOffer.offerAmount > 0);
+        vm.assume(pendingOffer.offerAmount == pendingOffer.offerLocker.lockedOfferAmount(offerId));
+
+        // Call the function being tested
+        _termAuctionList.insertPending(offerId, pendingOffer);
+
+        // Assert that the size of the list didn't change
+        assert(_countOffersInList() == count);
+
+        // Assert that the new offer is in the list
+        assert(_offerInList(offerId));
+
+        // Assert that the invariants are preserved
+        _establishSortedByAuctionId(Mode.Assert);
+        _establishNoDuplicateOffers(Mode.Assert);
+        _establishNoCompletedAuctions(Mode.Assert);
+        _establishPositiveOfferAmounts(Mode.Assert);
+        _establishOfferAmountMatchesAmountLocked(Mode.Assert, bytes32(0));
+    }
+
+    /**
+     * Configure the model of the OfferLocker for every offer in the list to
+     * follow the assumption that unlockOffers will not revert.
+     */
+    function _guaranteeUnlockAlwaysSucceeds() internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            PendingOffer storage offer = _termAuctionList.offers[current];
+            TermAuctionOfferLocker offerLocker =
+                TermAuctionOfferLocker(address(offer.offerLocker));
+
+            offerLocker.guaranteeUnlockAlwaysSucceeds();
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume that all RepoTokens in the PendingOffers have no discount rate
+     * set in the RepoTokenList.
+     */
+    function _assumeNoDiscountRatesSet() internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+            address repoToken = _termAuctionList.offers[current].repoToken;
+            uint256 discountRate = _repoTokenList.discountRates[repoToken];
+            vm.assume(discountRate == RepoTokenList.INVALID_AUCTION_RATE);
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Assume that all RepoTokens in the PendingOffers pass the checks performed
+     * in validateRepoToken, to ensure the function won't revert if they need to
+     * be inserted in the RepoTokenList.
+     */
+    function _assumeRepoTokensValidate(address asset) internal {
+        bytes32 current = _termAuctionList.head;
+
+        while (current != TermAuctionList.NULL_NODE) {
+                address repoToken = _termAuctionList.offers[current].repoToken;
+                (
+                 uint256 redemptionTimestamp,
+                 address purchaseToken,
+                 ,
+                 address collateralManager
+                ) = ITermRepoToken(repoToken).config();
+
+                vm.assume(purchaseToken == asset);
+
+                uint256 numTokens = ITermRepoCollateralManager(collateralManager).numOfAcceptedCollateralTokens();
+
+                for (uint256 i; i < numTokens; i++) {
+                    address currentToken = ITermRepoCollateralManager(collateralManager).collateralTokens(i);
+                    uint256 minCollateralRatio = _repoTokenList.collateralTokenParams[currentToken];
+
+                    vm.assume(minCollateralRatio != 0);
+                    vm.assume(
+                        ITermRepoCollateralManager(collateralManager).maintenanceCollateralRatios(currentToken) >= minCollateralRatio
+                    );
+                }
+
+            current = _termAuctionList.nodes[current].next;
+        }
+    }
+
+    /**
+     * Test that removeCompleted preserves the list invariants.
+     */
+    function testRemoveCompleted(address asset) external {
+        // For simplicity, assume that the RepoTokenList is empty
+        _repoTokenList.head = RepoTokenList.NULL_NODE;
+
+        // Initialize a DiscountRateAdapter with symbolic storage
+        TermDiscountRateAdapter discountRateAdapter =
+            new TermDiscountRateAdapter();
+        _initializeDiscountRateAdapter(discountRateAdapter);
+
+        // Our initialization procedure guarantees these invariants,
+        // so we assert instead of assuming
+        _establishSortedByAuctionId(Mode.Assert);
+        _establishNoDuplicateOffers(Mode.Assert);
+
+        // Assume that the invariants hold before the function is called
+        _establishOfferAmountMatchesAmountLocked(Mode.Assume, bytes32(0));
+
+        // Assume that the calls to unlockOffers will not revert
+        _guaranteeUnlockAlwaysSucceeds();
+
+        // Assume that the RepoTokens in PendingOffers have no discount rate set
+        _assumeNoDiscountRatesSet();
+
+        // Assume that the RepoTokens in PendingOffers pass validation
+        _assumeRepoTokensValidate(asset);
+
+        // Save the number of tokens in the list before the function is called
+        uint256 count = _countOffersInList();
+
+        // Call the function being tested
+        _termAuctionList.removeCompleted(
+            _repoTokenList,
+            discountRateAdapter,
+            asset
+        );
+
+        // Assert that the size of the list is less than or equal to before
+        assert(_countOffersInList() <= count);
+
+        // Assert that the invariants are preserved
+        _establishSortedByAuctionId(Mode.Assert);
+        _establishNoDuplicateOffers(Mode.Assert);
+        _establishOfferAmountMatchesAmountLocked(Mode.Assert, bytes32(0));
+
+        // Now the following invariants should hold as well
+        _establishNoCompletedAuctions(Mode.Assert);
+        _establishPositiveOfferAmounts(Mode.Assert);
+    }
+}
diff --git a/src/test/kontrol/TermAuctionOfferLocker.sol b/src/test/kontrol/TermAuctionOfferLocker.sol
new file mode 100644
index 00000000..b2fd9d8c
--- /dev/null
+++ b/src/test/kontrol/TermAuctionOfferLocker.sol
@@ -0,0 +1,107 @@
+pragma solidity 0.8.23;
+
+import "src/interfaces/term/ITermAuctionOfferLocker.sol";
+
+import "src/test/kontrol/Constants.sol";
+import "src/test/kontrol/KontrolTest.sol";
+
+contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest {
+    mapping(bytes32 => TermAuctionOffer) _lockedOffers;
+    address _termRepoServicer;
+    bool _unlockAlwaysSucceeds;
+
+    uint256 private constant lockedOffersSlot = 27;
+    uint256 private constant repoServicerAndUnlockSlot = 28;
+
+    function lockedOfferSlot(bytes32 offerId) internal view returns (uint256) {
+        return uint256(keccak256(abi.encodePacked(uint256(offerId), uint256(lockedOffersSlot))));
+    }
+
+    function initializeSymbolic(address termRepoServicer) public {
+        kevm.symbolicStorage(address(this));
+        // Clear slot which holds two contract fields
+        _storeUInt256(address(this), repoServicerAndUnlockSlot, 0);
+        _termRepoServicer = termRepoServicer;
+        _unlockAlwaysSucceeds = false;
+    }
+
+    function initializeSymbolicLockedOfferFor(bytes32 offerId) public {
+        TermAuctionOffer storage offer = _lockedOffers[offerId];
+        offer.amount = freshUInt256();
+        vm.assume(offer.amount < ETH_UPPER_BOUND);
+
+        uint256 _purchaseToken = uint160(kevm.freshAddress());
+        uint256 _isRevealed = uint96(kevm.freshBool());
+        bytes memory offerLastSlotAbi = abi.encodePacked(uint96(_isRevealed), uint160(_purchaseToken));
+        bytes32 offerLastSlot;
+        assembly {
+            offerLastSlot := mload(add(offerLastSlotAbi, 0x20))
+        }
+        _storeBytes32(address(this), lockedOfferSlot(offerId) + 5, offerLastSlot);
+    }
+
+    function guaranteeUnlockAlwaysSucceeds() external {
+        _unlockAlwaysSucceeds = true;
+    }
+
+    function termRepoId() external view returns (bytes32) {
+        return bytes32(freshUInt256());
+    }
+
+    function termAuctionId() external view returns (bytes32) {
+        return bytes32(freshUInt256());
+    }
+
+    function auctionStartTime() external view returns (uint256) {
+        return freshUInt256();
+    }
+
+    function auctionEndTime() external view returns (uint256) {
+        return freshUInt256();
+    }
+
+    function revealTime() external view returns (uint256) {
+        return freshUInt256();
+    }
+
+    function purchaseToken() external view returns (address) {
+        return kevm.freshAddress();
+    }
+
+    function termRepoServicer() external view returns (address) {
+        return _termRepoServicer;
+    }
+
+    function lockedOffer(bytes32 id) external view returns (TermAuctionOffer memory) {
+        return _lockedOffers[id];
+    }
+
+    function lockedOfferAmount(bytes32 id) external view returns (uint256) {
+        return _lockedOffers[id].amount;
+    }
+
+    function lockOffers(
+        TermAuctionOfferSubmission[] calldata offerSubmissions
+    ) external returns (bytes32[] memory) {
+        kevm.symbolicStorage(address(this));
+
+        uint256 length = freshUInt256();
+        bytes32[] memory offers = new bytes32[](length);
+
+        for (uint256 i = 0; i < length; ++i) {
+            offers[i] = bytes32(freshUInt256());
+        }
+
+        return offers;
+    }
+
+    function unlockOffers(bytes32[] calldata offerIds) external {
+        // Function might revert in some cases
+        if (!_unlockAlwaysSucceeds) {
+            require(kevm.freshBool() != 0);
+        }
+
+        kevm.symbolicStorage(_termRepoServicer);
+        kevm.symbolicStorage(address(this));
+    }
+}
diff --git a/src/test/kontrol/TermDiscountRateAdapter.sol b/src/test/kontrol/TermDiscountRateAdapter.sol
new file mode 100644
index 00000000..6226df6b
--- /dev/null
+++ b/src/test/kontrol/TermDiscountRateAdapter.sol
@@ -0,0 +1,37 @@
+pragma solidity 0.8.23;
+
+import "src/interfaces/term/ITermDiscountRateAdapter.sol";
+
+import "src/test/kontrol/Constants.sol";
+import "src/test/kontrol/KontrolTest.sol";
+
+contract TermDiscountRateAdapter is ITermDiscountRateAdapter, KontrolTest {
+    mapping(address => uint256) _repoRedemptionHaircut;
+    mapping(address => uint256) _discountRate;
+
+    function initializeSymbolic() public {
+        kevm.symbolicStorage(address(this));
+    }
+
+    function initializeSymbolicParamsFor(address repoToken) public {
+        uint256 repoRedemptionHaircut = freshUInt256();
+        vm.assume(repoRedemptionHaircut <= 1e18);
+        _repoRedemptionHaircut[repoToken] = repoRedemptionHaircut;
+
+        uint256 discountRate = freshUInt256();
+        vm.assume(discountRate < ETH_UPPER_BOUND);
+        _discountRate[repoToken] = discountRate;
+    }
+
+    function repoRedemptionHaircut(address repoToken) external view returns (uint256) {
+        return _repoRedemptionHaircut[repoToken];
+    }
+
+    function getDiscountRate(address repoToken) external view returns (uint256) {
+        return _discountRate[repoToken];
+    }
+
+    function TERM_CONTROLLER() external view returns (ITermController) {
+        return ITermController(kevm.freshAddress());
+    }
+}
diff --git a/src/test/kontrol/TermRepoCollateralManager.sol b/src/test/kontrol/TermRepoCollateralManager.sol
new file mode 100644
index 00000000..4b1d518d
--- /dev/null
+++ b/src/test/kontrol/TermRepoCollateralManager.sol
@@ -0,0 +1,47 @@
+pragma solidity 0.8.23;
+
+import "src/interfaces/term/ITermRepoCollateralManager.sol";
+import "src/test/kontrol/KontrolTest.sol";
+
+contract TermRepoCollateralManager is ITermRepoCollateralManager, KontrolTest {
+    mapping(address => uint256) _maintenanceCollateralRatios;
+    address[] _collateralTokens;
+
+    uint256 private constant collateralTokensSlot = 28;
+
+    function collateralTokensDataSlot(uint256 i) internal view returns (uint256) {
+        return uint256(keccak256(abi.encodePacked(collateralTokensSlot))) + i;
+    }
+
+    function initializeSymbolic() public {
+        kevm.symbolicStorage(address(this));
+
+        // For simplicity, choose an arbitrary number of collateral tokens: 3
+        _storeUInt256(address(this), collateralTokensSlot, 2);
+
+        for (uint256 i = 0; i < _collateralTokens.length; ++i) {
+            // Generate an arbitrary concrete address for each token
+            // All repoTokens in the list will share the same colllateral tokens
+            address currentToken = address(
+                uint160(uint256(keccak256(abi.encodePacked("collateral", i))))
+            );
+
+            _storeUInt256(address(this), collateralTokensDataSlot(i), uint256(uint160(currentToken)));
+            _maintenanceCollateralRatios[currentToken] = freshUInt256();
+        }
+    }
+
+    function maintenanceCollateralRatios(
+        address collateralToken
+    ) external view returns (uint256) {
+        return _maintenanceCollateralRatios[collateralToken];
+    }
+
+    function numOfAcceptedCollateralTokens() external view returns (uint8) {
+        return uint8(_collateralTokens.length);
+    }
+
+    function collateralTokens(uint256 index) external view returns (address) {
+        return _collateralTokens[index];
+    }
+}
diff --git a/src/test/kontrol/TermRepoServicer.sol b/src/test/kontrol/TermRepoServicer.sol
new file mode 100644
index 00000000..964cef40
--- /dev/null
+++ b/src/test/kontrol/TermRepoServicer.sol
@@ -0,0 +1,48 @@
+pragma solidity ^0.8.23;
+
+import "src/interfaces/term/ITermRepoServicer.sol";
+import "src/test/kontrol/KontrolTest.sol";
+
+contract TermRepoServicer is ITermRepoServicer, KontrolTest {
+    address _termRepoToken;
+    bool _redeemAlwaysSucceeds;
+
+    uint256 private constant repoTokenAndRedeemSlot = 27;
+
+    function initializeSymbolic(address termRepoToken) public {
+        kevm.symbolicStorage(address(this));
+        // Clear slot which holds two contract fields
+        _storeUInt256(address(this), repoTokenAndRedeemSlot, 0);
+        _termRepoToken = termRepoToken;
+        _redeemAlwaysSucceeds = false;
+    }
+
+    function guaranteeRedeemAlwaysSucceeds() external {
+        _redeemAlwaysSucceeds = true;
+    }
+
+    function redeemTermRepoTokens(
+        address redeemer,
+        uint256 amountToRedeem
+    ) external {
+        // Function might revert in some cases
+        if (!_redeemAlwaysSucceeds) {
+            require(kevm.freshBool() != 0);
+        }
+
+        kevm.symbolicStorage(_termRepoToken);
+        kevm.symbolicStorage(address(this));
+    }
+
+    function termRepoToken() external view returns (address) {
+        return _termRepoToken;
+    }
+
+    function termRepoLocker() external view returns (address) {
+        return kevm.freshAddress();
+    }
+
+    function purchaseToken() external view returns (address) {
+        return kevm.freshAddress();
+    }
+}
diff --git a/src/test/kontrol/term-lemmas.k b/src/test/kontrol/term-lemmas.k
new file mode 100644
index 00000000..6dabe3bd
--- /dev/null
+++ b/src/test/kontrol/term-lemmas.k
@@ -0,0 +1,257 @@
+requires "evm.md"
+requires "foundry.md"
+// requires "keccak.md"
+
+module TERM-LEMMAS
+    imports EVM
+    imports FOUNDRY
+    imports INT-SYMBOLIC
+    imports MAP-SYMBOLIC
+    imports SET-SYMBOLIC
+    // imports KECCAK-LEMMAS
+
+    syntax StepSort ::= Int
+                      | Bool
+                      | Bytes
+                      | Map
+                      | Set
+ // -------------------------
+
+    syntax KItem ::= runLemma ( StepSort )
+                   | doneLemma( StepSort )
+ // --------------------------------------
+    rule <k> runLemma(T) => doneLemma(T) ... </k>
+
+    // Instantiation of the Kontrol lemma
+    // rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+    // when Y is of the form Y *Int Z, because then the `Y ==Int 0` condition gets simplified to a different form
+    rule ( X ==Int ( X *Int (Y *Int Z) ) /Word (Y *Int Z) ) orBool (Y ==Int 0 orBool Z ==Int 0) => true [simplification, preserves-definedness]
+
+    // Instantiation of the Kontrol lemma
+    // rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+    // when Y is of the form Y *Int ( Z *Int T ), because then the `Y ==Int 0` condition gets simplified to a different form
+    rule ( X ==Int ( X *Int (Y *Int (Z *Int T)) ) /Word (Y *Int (Z *Int T)) ) orBool (Y ==Int 0 orBool (Z ==Int 0 orBool T ==Int 0)) => true [simplification, preserves-definedness]
+
+    // Instantiation of the Kontrol lemma
+    // rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+    // when Y is of the form Y /Int Z, because then the `Y ==Int 0` condition gets simplified to a different form
+    rule ( X ==Int ( X *Int (Y /Int Z) ) /Word (Y /Int Z) ) orBool Y <Int Z => true
+      requires notBool ( Z ==Int 0 )
+      [simplification, preserves-definedness]
+
+    rule [chop-sub]:
+      chop ( Y -Int X:Int ) ==Int 0 => X ==Int Y
+      requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
+      [simplification, concrete(Y), comm]
+
+    rule [keccak-slots-disjoint]:
+      keccak ( A ) ==Int keccak ( B ) +Int C => false
+      requires notBool 0 ==Int C
+      [simplification, concrete(C), comm]
+
+    rule [keccak-slots-disjoint-ml-l]:
+      { keccak ( A ) #Equals keccak ( B ) +Int C } => #Bottom
+      requires notBool 0 ==Int C
+      [simplification, concrete(C)]
+
+    rule [keccak-slots-disjoint-ml-r]:
+      { keccak ( B ) +Int C #Equals keccak ( A ) } => #Bottom
+      requires notBool 0 ==Int C
+      [simplification, concrete(C)]
+
+    // 2a. |Int and +Bytes, update to be done in left
+    rule [bor-update-to-left-2]:
+      #asWord ( B1 +Bytes B2 ) |Int A =>
+        #asWord ( #buf ( 32 -Int lengthBytes(B2), (A /Int (2 ^Int (8 *Int lengthBytes(B2)))) |Int #asWord ( B1 ) ) +Bytes B2 )
+        requires #rangeUInt(256, A) andBool A modInt (2 ^Int (8 *Int lengthBytes(B2))) ==Int 0 andBool lengthBytes(B1 +Bytes B2) <=Int 32
+        [simplification, preserves-definedness]
+
+    // 2b. |Int of +Bytes, update to be done in right
+    rule [bor-update-to-right-2]:
+      #asWord ( B1 +Bytes B2 ) |Int A =>
+        #asWord ( B1 +Bytes #buf ( lengthBytes(B2), A |Int #asWord ( B2 ) ) )
+        requires 0 <=Int A andBool A <Int 2 ^Int (8 *Int lengthBytes(B2)) andBool lengthBytes(B2) <=Int 32
+        [simplification, preserves-definedness]
+
+    rule ( SetItem(X:Int) S:Set ) |Set SetItem(Y:Int) => SetItem(X) ( S |Set SetItem (Y) ) requires notBool X ==Int Y [simplification, preserves-definedness]
+    rule ( SetItem(X:Int) S:Set ) |Set SetItem(Y:Int) => SetItem(X) S                      requires         X ==Int Y [simplification, preserves-definedness]
+    rule                     .Set |Set SetItem(X:Int) => SetItem(X)                                                   [simplification, preserves-definedness]
+
+    rule K1 in_keys((K2 |-> _ ) M) => K1 ==Int K2 orBool K1 in_keys(M) [simplification]
+
+    rule [transferFunds-hp-neq]:
+      <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k>
+      <account>
+        <acctID> ACCTFROM </acctID>
+        <balance> ORIGFROM => ORIGFROM -Word VALUE </balance>
+        ...
+      </account>
+      <account>
+        <acctID> ACCTTO </acctID>
+        <balance> ORIGTO => ORIGTO +Word VALUE </balance>
+        ...
+      </account>
+      requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
+      [priority(30), preserves-definedness]
+
+    rule [accounts-in-keys]:
+      `AccountCellMap:in_keys`(
+        <acctID> (X:Int) </acctID>,
+        (`_AccountCellMap_`(AccountCellMapItem(<acctID> Y:Int </acctID>, _:AccountCell):AccountCellMap, ACCOUNTS_REST:AccountCellMap)):AccountCellMap
+      ) => X ==Int Y orBool `AccountCellMap:in_keys`(<acctID> (X:Int) </acctID>, ACCOUNTS_REST)
+      [simplification, preserves-definedness]
+
+endmodule
+
+module TERM-LEMMAS-SPEC
+    imports TERM-LEMMAS
+
+    claim [storage-offset]: <k> runLemma ( ( #lookup ( STORAGE3:Map , 2 ) /Int pow160 ) ) => doneLemma ( #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE3:Map , 2 ) ) , 0 , 12 ) ) ) ... </k>
+
+    claim [chop-simplify]: <k> runLemma (
+                                 notBool chop ( WORD7:Int +Int ( WORD12:Int *Int ( ( WORD5:Int -Int WORD6:Int ) /Int WORD11:Int ) ) ) ==Int
+                                 chop ( chop ( WORD7:Int +Int ( WORD12:Int *Int ( ( WORD5:Int -Int WORD6:Int ) /Int WORD11:Int ) ) ) *Int 1000000000000000000 ) /Int 1000000000000000000
+                               ) => runLemma ( false ) ... </k>
+      requires 0 <=Int WORD5:Int
+       andBool 0 <=Int WORD6:Int
+       andBool 0 <=Int WORD7:Int
+       andBool 0 <=Int WORD11:Int
+       andBool 0 <=Int WORD12:Int
+       andBool WORD11:Int =/=Int 0
+       andBool WORD12:Int =/=Int 0
+       andBool WORD6:Int <=Int WORD5:Int
+       andBool WORD5:Int <Int pow96
+       andBool WORD6:Int <Int pow96
+       andBool WORD7:Int <Int pow96
+       andBool WORD11:Int <Int pow96
+       andBool WORD12:Int <Int pow96
+
+    claim [storage-simplification]:
+      <k> runLemma (
+            STORAGE0:Map
+            [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD4:Int ) +Bytes #buf ( 5 , WORD3:Int ) +Bytes b"\x00" ) ]
+            [ 6 <- #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ]
+            [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD4:Int ) +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes b"\x01" ) ]
+            [ 6 <- ( ( TIMESTAMP_CELL:Int *Int pow40 ) |Int ( 115792089237316195423570985008687907853269984665640562830531764394383466561535 &Int #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) ) ]
+            [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes b"\x01" ) ]
+          ) => doneLemma (
+            STORAGE0:Map
+            [ 6 <- #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ]
+            [ 5 <- #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes b"\x01" ) ]
+          ) ... </k>
+          requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int pow40
+
+    claim [slot-update-01]:
+      <k> runLemma(
+        ( maxUInt8 &Int ( ( TIMESTAMP_CELL:Int *Int pow48 ) |Int ( 115792089237316195423570985008687907853269984665640254554447762944319381569535 &Int ( ( TIMESTAMP_CELL:Int *Int 256 ) |Int ( 115792089237316195423570985008687907853269984665640564039457583726438152929535 &Int ( 1 |Int #asWord ( b"\x00E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , _WORD4:Int ) +Bytes #buf ( 5 , _WORD3:Int ) +Bytes b"\x00" ) ) ) ) ) ) )
+      ) => doneLemma(
+        1
+      ) ... </k>
+      requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int 2 ^Int 40
+
+    claim [slot-update-02]:
+      <k> runLemma (
+            ( ( maxUInt40 &Int ( ( 115341543235797707419527244145998463631733976271937281205136574426583511597055 &Int #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , TIMESTAMP_CELL:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) /Int pow40 ) ) )
+          ) => doneLemma (
+            TIMESTAMP_CELL
+          ) ... </k>
+          requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int 2 ^Int 35
+
+    claim [slot-update-03]:
+      <k> runLemma (
+            ( maxUInt40 &Int ( ( TIMESTAMP_CELL:Int |Int ( 115792089237316195423570985008687907853269984665640564039457584006813618012160 &Int #asWord ( #buf ( 1 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) ) /Int pow40 ) ) <=Int TIMESTAMP_CELL:Int
+          ) => doneLemma (
+            true
+          ) ... </k>
+          requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int 2 ^Int 35
+
+    claim [slot-update-04]:
+      <k> runLemma (
+            #asWord ( #range ( #buf ( 10 , ( ( ( TIMESTAMP_CELL:Int *Int pow48 ) /Int 256 ) |Int TIMESTAMP_CELL:Int ) ) , 5 , 5 ) ) <=Int TIMESTAMP_CELL:Int
+          ) => doneLemma (
+            true
+          ) ... </k>
+          requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int 2 ^Int 35
+
+    claim [slot-update-05]:
+      <k> runLemma (
+            #asWord ( #range ( #buf ( 6 , TIMESTAMP_CELL:Int *Int 256 ) , 5 , 1 ) )
+          ) => doneLemma (
+            false
+          ) ... </k>
+          requires 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int 2 ^Int 35
+
+    claim [slot-update-06]:
+      <k> runLemma (
+            #asWord ( #range ( #buf ( 26 , 960911443338137442927181681227604902095826437272264907948032 |Int WORD4:Int ) , 21 , 5 ) ) <=Int TIMESTAMP_CELL:Int
+          ) => doneLemma (
+            WORD4 <=Int TIMESTAMP_CELL
+          ) ... </k>
+          requires 0 <=Int WORD4 andBool WORD4 <Int 2 ^Int 40
+
+    claim [slot-update-07]:
+      <k> runLemma (
+            #asWord ( #range ( #buf ( 25 , ( ( ( WORD7:Int +Int 1 ) *Int pow200 ) |Int #asWord ( #buf ( 25 , ( 438052756531465687819472504520361015472122898704787692322816 |Int WORD6:Int ) ) ) ) ) , 20 , 5 ) ) <=Int TIMESTAMP_CELL:Int
+          ) => doneLemma (
+            WORD6 <=Int TIMESTAMP_CELL
+          ) ... </k>
+          requires 0 <=Int WORD6 andBool WORD6 <Int 2 ^Int 40
+           andBool 0 <=Int WORD7 andBool WORD7 <Int 256
+
+    claim [slot-update-08]:
+      <k> runLemma (
+            #asWord ( #buf ( 20 , 770621190285571058874329108704665103402425909248 |Int ( ( WORD7:Int +Int 1 ) *Int pow160 ) ) )
+          ) => doneLemma (
+            770621190285571058874329108704665103402425909248
+          ) ... </k>
+          requires 0 <=Int WORD7 andBool WORD7 <Int 256
+
+    claim [slot-update-09]:
+      <k> runLemma (
+            ( 481644099385675654177479669474857658256926169505224677670350078624137216 |Int ( 115790322390251417039241401711187164934754157181743689629425282016341011726335 &Int #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"\xa4\xadOh\xd0\xb9\x1c\xfd\x19h|\x88\x1eP\xf3\xa0\x02B\x82\x8c" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) ) ) )
+          ) => doneLemma (
+            #asWord ( #buf ( 2 , WORD7:Int ) +Bytes b"E\xc9,,\xd0\xdf{-p^\xf1,\xffw\xcb\x0b\xc5W\xed\"" +Bytes #buf ( 5 , WORD6:Int ) +Bytes #buf ( 5 , WORD5:Int ) )
+          ) ... </k>
+          requires 0 <=Int WORD5 andBool WORD5 <Int 2 ^Int 35
+           andBool 0 <=Int WORD6 andBool WORD6 <Int 2 ^Int 35
+           andBool 0 <=Int WORD7 andBool WORD7 <Int 256
+
+    claim [length-bytestack]: <k> runLemma ( lengthBytes ( #padToWidth ( 32 , #asByteStack ( ( ( ( ( ( WORD0:Int *Int VV0_amount_114b9705:Int ) /Int WORD:Int ) +Int WORD8:Int ) |Int #asWord ( #buf ( 16 , WORD9:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) ) /Int pow128 ) ) ) ) ) => doneLemma ( 32 ) ... </k>
+
+    claim [add-not-eq-zero]: <k> runLemma ( 0 ==Int ( ( ( ( ( VV0_purchaseTokenPrecision_114b9705:Int *Int ( WORD0:Int -Int TIMESTAMP_CELL:Int ) ) /Int 31104000 ) *Int WORD:Int ) /Int 1000000000000000000 ) +Int VV0_purchaseTokenPrecision_114b9705:Int ) ) => doneLemma ( false ) ... </k>
+        requires 0 <Int VV0_purchaseTokenPrecision_114b9705
+         andBool 0 <=Int WORD
+         andBool 0 <=Int TIMESTAMP_CELL
+         andBool TIMESTAMP_CELL <=Int WORD0
+
+    claim [chop-comparison]: <k> runLemma ( 0 ==Int chop ( ( 491460923342184218035706888008750043977755113263 -Int VV0_repoToken_114b9705 ) ) ) => doneLemma ( 491460923342184218035706888008750043977755113263 ==Int VV0_repoToken_114b9705 ) ... </k>
+        requires 0 <=Int VV0_repoToken_114b9705:Int
+         andBool VV0_repoToken_114b9705:Int <Int pow160
+
+    claim [keccak-lookup]: <k> runLemma ( #lookup ( STORAGE:Map [ maxUInt5 <- WORD:Int ] [ keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) <- 491460923342184218035706888008750043977755113263 ] [ ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 1 ) <- WORD0:Int ] [ ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) <- 263400868551549723330807389252719309078400616203 ] [ ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) <- 1405310203571408291950365054053061012934685786634 ] , keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) ) ) => doneLemma ( #lookup ( STORAGE:Map , keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) ) ) ... </k>
+
+    claim [keccak-lookup-2]: <k> runLemma ( #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map [ maxUInt5 <- WORD:Int ] [ keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) <- 491460923342184218035706888008750043977755113263 ] [ ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 1 ) <- WORD0:Int ] [ ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) <- 263400868551549723330807389252719309078400616203 ] [ ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) <- 1405310203571408291950365054053061012934685786634 ] [ keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) <- WORD1:Int ] [ keccak ( #buf ( 32 , WORD1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) <- 511347974759188522659820409854212399244223280809 ] [ ( keccak ( #buf ( 32 , WORD1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 1 ) <- WORD2:Int ] [ ( keccak ( #buf ( 32 , WORD1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) <- 1136628940260574992893479910319181283093952727985 ] , ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) ) ) , 12 , 20 ) ) ) => doneLemma ( 1405310203571408291950365054053061012934685786634 ) ... </k>
+
+    claim [keccak-comparison-1]: <k> runLemma ( ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) ==Int ( keccak ( #buf ( 32 , WORD1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) ) => doneLemma ( false ) ... </k>
+
+    claim [keccak-comparison-2]: <k> runLemma ( ( keccak ( #buf ( 32 , WORD:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) ==Int ( keccak ( #buf ( 32 , WORD1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) ) => doneLemma ( false ) ... </k>
+
+    claim [chop-check]: <k> runLemma ( chop ( ( VV2_purchaseTokenPrecision_114b9705:Int *Int WORD8:Int *Int WORD10:Int /Int 1000000000000000000000000000000000000 ) *Int ( WORD11:Int -Int TIMESTAMP_CELL:Int ) +Int ( VV2_purchaseTokenPrecision_114b9705:Int *Int WORD1:Int *Int WORD3:Int /Int 1000000000000000000000000000000000000 ) *Int ( WORD4:Int -Int TIMESTAMP_CELL:Int ) ) ) => doneLemma ( true ) ... </k>
+    requires 0 <=Int VV2_purchaseTokenPrecision_114b9705 andBool VV2_purchaseTokenPrecision_114b9705 <Int 18
+     andBool 0 <=Int WORD1 andBool WORD1 <Int 2 ^Int 95
+     andBool 0 <=Int WORD3 andBool WORD3 <Int 2 ^Int 95
+     andBool 0 <=Int WORD4 andBool WORD4 <Int 34359738368
+     andBool 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int WORD4
+     andBool 0 <=Int TIMESTAMP_CELL andBool TIMESTAMP_CELL <Int WORD11
+     andBool 0 <=Int WORD8 andBool WORD8 <Int 2 ^Int 95
+     andBool 0 <=Int WORD10 andBool WORD10 <Int 2 ^Int 95
+     andBool 0 <=Int WORD11 andBool WORD11 <Int 34359738368
+
+    claim [keccak-comparison-3]: <k> runLemma ( #lookup ( STORAGE:Map [ 34 <- #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map , 34 ) ) , 0 , 12 ) +Bytes b"V\x15\xde\xb7\x98\xbb>M\xfa\x019\xdf\xa1\xb3\xd43\xcc#\xb7/" ) ] [ maxUInt5 <- VV0_offerId_114b9705:Int ] [ keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) <- 0 ] [ keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) <- #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map , keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) ) ) , 0 , 12 ) +Bytes b".#M\xaeu\xc7\x93\xf6z5\x08\x9c\x9d\x99$^\x1cXG\x0b" ) ] [ ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 1 ) <- #lookup ( STORAGE3:Map , ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1b" ) +Int 4 ) ) ] [ ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) <- #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map [ 34 <- #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map , 34 ) ) , 0 , 12 ) +Bytes b"V\x15\xde\xb7\x98\xbb>M\xfa\x019\xdf\xa1\xb3\xd43\xcc#\xb7/" ) ] [ maxUInt5 <- VV0_offerId_114b9705:Int ] [ keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) <- 0 ] , ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) ) ) , 0 , 12 ) +Bytes #buf ( 20 , WORD:Int ) ) ] [ ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) <- #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map [ 34 <- #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map , 34 ) ) , 0 , 12 ) +Bytes b"V\x15\xde\xb7\x98\xbb>M\xfa\x019\xdf\xa1\xb3\xd43\xcc#\xb7/" ) ] [ maxUInt5 <- VV0_offerId_114b9705:Int ] [ keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) <- 0 ] , ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 3 ) ) ) , 0 , 12 ) +Bytes b"\xf6(I\xf9\xa0\xb5\xbf)\x13\xb3\x96\t\x8f|p\x19\xb5\x1a\x82\n" ) ] , keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) ) )
+                                  => doneLemma ( 0 ) ... </k>
+
+    claim [slot-update-10]: <k> runLemma ( #asWord ( #range ( #buf ( 32 , ( #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE:Map , ( keccak ( #buf ( 32 , VV0_offerId_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00!" ) +Int 2 ) ) ) , 0 , 12 ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) |Int WORD:Int ) ) , 12 , 20 ) )  )
+                                => doneLemma ( WORD:Int ) ... </k>
+                                requires #rangeUInt(160, WORD)
+
+endmodule
\ No newline at end of file
diff --git a/src/test/mocks/MockTermAuctionOfferLocker.sol b/src/test/mocks/MockTermAuctionOfferLocker.sol
index 7748ea37..cba9968d 100644
--- a/src/test/mocks/MockTermAuctionOfferLocker.sol
+++ b/src/test/mocks/MockTermAuctionOfferLocker.sol
@@ -14,11 +14,11 @@ contract MockTermAuctionOfferLocker is ITermAuctionOfferLocker {
     MockTermRepoLocker internal repoLocker;
     ITermAuction internal auction;
     mapping(bytes32 => TermAuctionOffer) internal lockedOffers;
-    
+
     constructor(
-        ITermAuction _auction, 
-        address _repoLocker, 
-        address _repoServicer, 
+        ITermAuction _auction,
+        address _repoLocker,
+        address _repoServicer,
         address _purchaseToken
     ) {
         auction = _auction;
@@ -48,6 +48,10 @@ contract MockTermAuctionOfferLocker is ITermAuctionOfferLocker {
         return lockedOffers[id];
     }
 
+    function lockedOfferAmount(bytes32 id) external view returns (uint256) {
+        return lockedOffers[id].amount;
+    }
+
     function lockOffers(
         TermAuctionOfferSubmission[] calldata offerSubmissions
     ) external returns (bytes32[] memory offerIds) {
@@ -77,7 +81,7 @@ contract MockTermAuctionOfferLocker is ITermAuctionOfferLocker {
                 offer.purchaseToken = submission.purchaseToken;
 
                 repoLocker.lockPurchaseTokens(msg.sender, offer.amount);
-            }            
+            }
             lockedOffers[offer.id] = offer;
             offerIds[i] = offer.id;
         }