diff --git a/.python-version b/.python-version
new file mode 100644
index 000000000..24ee5b1be
--- /dev/null
+++ b/.python-version
@@ -0,0 +1 @@
+3.13
diff --git a/pyproject.toml b/pyproject.toml
new file mode 100644
index 000000000..f548bf5d2
--- /dev/null
+++ b/pyproject.toml
@@ -0,0 +1,12 @@
+[project]
+name = "aave-v4"
+version = "0.1.0"
+readme = "README.md"
+requires-python = ">=3.13"
+dependencies = ["z3-solver>=4.15.7.0"]
+
+[dependency-groups]
+dev = ["ruff>=0.15.0"]
+
+[tool.ruff.format]
+quote-style = "single"
diff --git a/tests/misc/calculate_linear_interest.py b/tests/misc/calculate_linear_interest.py
deleted file mode 100644
index 2e69ccad9..000000000
--- a/tests/misc/calculate_linear_interest.py
+++ /dev/null
@@ -1,22 +0,0 @@
-from z3 import *
-
-s = Optimize()
-
-UINT256_MAX = IntVal(2**256 - 1)
-RAY = IntVal(10**27)
-SECONDS_PER_YEAR = IntVal(365 * 24 * 60 * 60)
-
-rate = IntVal(2**96 - 1)
-lastUpdateTimestamp = IntVal(1)
-currentTimestamp = Int("currentTimestamp")
-elapsed = currentTimestamp - lastUpdateTimestamp
-
-s.add(elapsed >= 0)
-s.add(rate * elapsed <= UINT256_MAX)
-s.add(RAY + ((rate * elapsed) / SECONDS_PER_YEAR) <= UINT256_MAX)
-
-s.maximize(currentTimestamp)
-
-assert s.check() == sat
-m = s.model()
-print("currentTimestamp max =", m[currentTimestamp])
diff --git a/tests/misc/liquidity_growth.py b/tests/misc/liquidity_growth.py
deleted file mode 100644
index 376943b47..000000000
--- a/tests/misc/liquidity_growth.py
+++ /dev/null
@@ -1,29 +0,0 @@
-# Highlights the fact that liquidity growth cannot be calculated accurately using the index delta.
-from z3 import *
-
-base = Int('base')
-premium = Int('premium')
-index1 = Int('index1')
-index2 = Int('index2')
-
-RAY = IntVal(10**27)
-
-s = Solver()
-
-s.add(RAY <= index1, index1 < index2, index2 <= 100 * RAY)
-s.add(0 <= base, base <= 10**30)
-s.add(0 <= premium, premium <= 10**30)
-
-rayMulUp = lambda a, b: (a * b + RAY - 1) / RAY
-rayMulDown = lambda a, b: (a * b) / RAY
-
-trueLiquidityGrowth = rayMulUp(base, index2) - rayMulUp(base, index1) + rayMulUp(premium, index2) - rayMulUp(premium, index1)
-x = rayMulDown(base, index2 - index1) + rayMulDown(premium, index2 - index1) # incorrect -- it underestimates the liquidity growth
-# x = rayMulDown(base + premium, index2 - index1) # incorrect -- it overestimates the liquidity growth
-
-s.add(Not(trueLiquidityGrowth == x))
-
-if s.check() == sat:
-    print("counterexample:", s.model())
-else:
-    print("no counterexample found")
diff --git a/tests/misc/share_assets_conversion.py b/tests/misc/share_assets_conversion.py
deleted file mode 100644
index 956f9b62d..000000000
--- a/tests/misc/share_assets_conversion.py
+++ /dev/null
@@ -1,44 +0,0 @@
-# Highlights the fact that supplies shares are always equal to removed shares (after doing the conversion to assets and back to shares).
-from z3 import *
-
-WAD = IntVal(10**18)
-VIRTUAL_SHARES = IntVal(10**6)
-VIRTUAL_ASSETS = IntVal(10**6)
-
-def mulDivDown(a, num, den):
-    return (a * num) / den
-
-def mulDivUp(a, num, den):
-    return (a * num + den - 1) / den
-
-def previewRemoveByShares(shares, totalAddedAssets, totalAddedShares):
-    return mulDivDown(shares, totalAddedAssets + VIRTUAL_ASSETS, totalAddedShares + VIRTUAL_SHARES)
-
-def previewRemoveByAssets(assets, totalAddedAssets, totalAddedShares):
-    return mulDivUp(assets, totalAddedShares + VIRTUAL_SHARES, totalAddedAssets + VIRTUAL_ASSETS)
-
-def check(propertyDescription):
-    print(f"\n-- {propertyDescription} --")
-    result = s.check()
-    if result == sat:
-        print("Counterexample found:")
-        print(s.model())
-    elif result == unsat:
-        print(f"Property holds.")
-    elif result == unknown:
-        print("Timed out or unknown.")
-
-s = Solver()
-
-totalAddedAssets = Int('totalAddedAssets')
-s.add(0 <= totalAddedAssets, totalAddedAssets <= 10**30)
-totalAddedShares = Int('totalAddedShares')
-s.add(totalAddedAssets >= totalAddedShares, totalAddedAssets + VIRTUAL_ASSETS < (totalAddedShares + VIRTUAL_SHARES) * 100)
-suppliedShares = Int('suppliedShares')
-s.add(0 <= suppliedShares, suppliedShares <= totalAddedShares)
-
-withdrawableAssets = previewRemoveByShares(suppliedShares, totalAddedAssets, totalAddedShares)
-removedShares = previewRemoveByAssets(withdrawableAssets, totalAddedAssets, totalAddedShares)
-
-s.add(removedShares != suppliedShares)
-check("Supplies shares are always equal to removed shares (after doing the conversion to assets and back to shares).")
\ No newline at end of file
diff --git a/tests/misc/supply_share_price_deficit.py b/tests/misc/supply_share_price_deficit.py
deleted file mode 100644
index 53335a4f6..000000000
--- a/tests/misc/supply_share_price_deficit.py
+++ /dev/null
@@ -1,58 +0,0 @@
-# Highlights the fact that totalAddedAssets does not decrease when a deficit is reported (hence the share price does not decrease).
-from z3 import *
-
-RAY = IntVal(10**27)
-
-def divUp(a, b):
-    return (a + b - 1) / b
-
-def fromRayUp(a):
-    return divUp(a, RAY)
-
-def fromRayDown(a):
-    return a / RAY
-
-def rayMulUp(a, b):
-    return (a * b + RAY - 1) / RAY
-
-def rayMulDown(a, b):
-    return (a * b) / RAY
-
-def totalAddedAssets(drawnShares, premiumDebtRay, deficitRay, drawnIndex):
-  # return rayMulUp(drawnShares, drawnIndex) + fromRayUp(premiumDebtRay) + fromRayUp(deficitRay)          # this is wrong
-  # return rayMulDown(drawnShares, drawnIndex) + fromRayDown(premiumDebtRay) + fromRayDown(deficitRay)    # this is wrong
-  return fromRayUp(drawnShares * drawnIndex + premiumDebtRay + deficitRay)
-
-def check(propertyDescription):
-    print(f"\n-- {propertyDescription} --")
-    result = s.check()
-    if result == sat:
-        print("Counterexample found:")
-        print(s.model())
-    elif result == unsat:
-        print(f"Property holds.")
-    elif result == unknown:
-        print("Timed out or unknown.")
-
-s = Solver()
-
-drawnShares = Int('drawnShares')
-s.add(1 <= drawnShares, drawnShares <= 10**30)
-drawnIndex = Int('drawnIndex')
-s.add(RAY <= drawnIndex, drawnIndex < 100 * RAY)
-premiumDebtRay = Int('premiumDebtRay')
-s.add(0 <= premiumDebtRay, premiumDebtRay <= 10**30)
-deficitRay = Int('deficitRay')
-s.add(0 <= deficitRay, deficitRay <= 10**30)
-
-deficitDrawnShares = Int('deficitDrawnShares')
-s.add(0 <= deficitDrawnShares, deficitDrawnShares <= drawnShares)
-deficitPremiumDebtRay = Int('deficitPremiumDebtRay')
-s.add(0 <= deficitPremiumDebtRay, deficitPremiumDebtRay <= premiumDebtRay)
-
-totalAddedAssetsBefore = totalAddedAssets(drawnShares, premiumDebtRay, deficitRay, drawnIndex)
-totalAddedAssetsAfter = totalAddedAssets(drawnShares - deficitDrawnShares, premiumDebtRay - deficitPremiumDebtRay, deficitRay + deficitDrawnShares * drawnIndex + deficitPremiumDebtRay, drawnIndex)
-
-s.push()
-s.add(totalAddedAssetsBefore > totalAddedAssetsAfter)
-check("Total added assets does not decrease after deficit is reported")
\ No newline at end of file
diff --git a/tests/misc/supply_share_price_fees.py b/tests/misc/supply_share_price_fees.py
deleted file mode 100644
index 113479d10..000000000
--- a/tests/misc/supply_share_price_fees.py
+++ /dev/null
@@ -1,87 +0,0 @@
-# Highlights the fact that the supply share price does not decrease between accruals/previews due to fees. 
-# Note that minting fee shares is equivalent to an add operation, which is known to not decrease the share price.
-from z3 import *
-
-RAY = IntVal(10**27)
-PERCENTAGE_FACTOR = IntVal(10**4)
-
-def percentMulDown(a, b):
-    return (a * b) / PERCENTAGE_FACTOR
-
-def divUp(a, b):
-    return (a + b - 1) / b
-
-def fromRayUp(a):
-    return divUp(a, RAY)
-
-def premiumDebtRay(realizedPremiumRay, premiumShares, drawnIndex, premiumOffsetRay):
-    return realizedPremiumRay + premiumShares * drawnIndex - premiumOffsetRay
-
-def totalDebt(drawnShares, drawnIndex, realizedPremiumRay, premiumShares, premiumOffsetRay, deficitRay):
-    return fromRayUp(drawnShares * drawnIndex + premiumDebtRay(realizedPremiumRay, premiumShares, drawnIndex, premiumOffsetRay) + deficitRay)
-
-def unrealizedFeeAmount(drawnShares, previousIndex, drawnIndex, realizedPremiumRay, premiumShares, premiumOffsetRay, deficitRay, liquidityFee):
-    totalDebtAfter = totalDebt(drawnShares, drawnIndex, realizedPremiumRay, premiumShares, premiumOffsetRay, deficitRay)
-    totalDebtBefore = totalDebt(drawnShares, previousIndex, realizedPremiumRay, premiumShares, premiumOffsetRay, deficitRay)
-    return percentMulDown(totalDebtAfter - totalDebtBefore, liquidityFee)
-
-def check(propertyDescription):
-    print(f"\n-- {propertyDescription} --")
-    result = s.check()
-    if result == sat:
-        print("Counterexample found:")
-        print(s.model())
-    elif result == unsat:
-        print(f"Property holds.")
-    elif result == unknown:
-        print("Timed out or unknown.")
-
-s = Solver()
-
-liquidityFee = Int('liquidityFee')
-s.add(0 <= liquidityFee, liquidityFee <= PERCENTAGE_FACTOR)
-
-drawnIndex1 = Int('drawnIndex1')
-s.add(RAY <= drawnIndex1, drawnIndex1 < 100 * RAY)
-drawnIndex2 = Int('drawnIndex2')
-s.add(drawnIndex1 <= drawnIndex2, drawnIndex2 < 100 * RAY)
-drawnIndex3 = Int('drawnIndex3')
-s.add(drawnIndex2 <= drawnIndex3, drawnIndex3 < 100 * RAY)
-
-drawnShares = Int('drawnShares')
-s.add(1 <= drawnShares, drawnShares <= 10**30)
-premiumShares = Int('premiumShares')
-s.add(0 <= premiumShares, premiumShares <= 10**30)
-premiumOffsetRay = premiumShares * RAY
-realizedPremiumRay = Int('realizedPremiumRay')
-s.add(0 <= realizedPremiumRay, realizedPremiumRay <= 10**30)
-liquiditySwept = Int('liquiditySwept')
-s.add(0 <= liquiditySwept, liquiditySwept <= 10**30)
-deficitRay = Int('deficitRay')
-s.add(0 <= deficitRay, deficitRay <= 10**30)
-
-# T1: accrue
-feeAmount1 = unrealizedFeeAmount(drawnShares, RAY, drawnIndex1, realizedPremiumRay, premiumShares, premiumOffsetRay, deficitRay, liquidityFee)
-totalAddedAssets1 = liquiditySwept + totalDebt(drawnShares, drawnIndex1, realizedPremiumRay, premiumShares, premiumOffsetRay, deficitRay) - feeAmount1
-newRealizedPremiumRay = realizedPremiumRay + premiumShares * drawnIndex1 - premiumOffsetRay
-newPremiumOffsetRay = premiumShares * drawnIndex1
-
-# T2: preview
-feeAmount2 = feeAmount1 + unrealizedFeeAmount(drawnShares, drawnIndex1, drawnIndex2, newRealizedPremiumRay, premiumShares, newPremiumOffsetRay, deficitRay, liquidityFee)
-totalAddedAssets2 = liquiditySwept + totalDebt(drawnShares, drawnIndex2, newRealizedPremiumRay, premiumShares, newPremiumOffsetRay, deficitRay) - feeAmount2
-
-# T3: preview
-feeAmount3 = feeAmount1 + unrealizedFeeAmount(drawnShares, drawnIndex1, drawnIndex3, newRealizedPremiumRay, premiumShares, newPremiumOffsetRay, deficitRay, liquidityFee)
-totalAddedAssets3 = liquiditySwept + totalDebt(drawnShares, drawnIndex3, newRealizedPremiumRay, premiumShares, newPremiumOffsetRay, deficitRay) - feeAmount3
-
-s.push()
-# Shares remain constant
-s.add(simplify(totalAddedAssets1 > totalAddedAssets2))
-check("Share price does not decrease from T1 to T2")
-s.pop()
-
-s.push()
-# Shares remain constant
-s.add(simplify(totalAddedAssets2 > totalAddedAssets3))
-check("Share price does not decrease from T2 to T3")
-s.pop()
\ No newline at end of file
diff --git a/tests/misc/supply_share_price_repay.py b/tests/misc/supply_share_price_repay.py
deleted file mode 100644
index 9fc527d69..000000000
--- a/tests/misc/supply_share_price_repay.py
+++ /dev/null
@@ -1,37 +0,0 @@
-# Highlights the fact that the supply share price does not decrease after a repay operation.
-from z3 import *
-
-RAY = IntVal(10**27)
-PERCENTAGE_FACTOR = IntVal(10**4)
-VIRTUAL_SHARES = IntVal(10**6)
-VIRTUAL_ASSETS = IntVal(10**6)
-
-def divUp(a, b):
-    return (a + b - 1) / b
-
-def check(propertyDescription):
-    print(f"\n-- {propertyDescription} --")
-    result = s.check()
-    if result == sat:
-        print("Counterexample found:")
-        print(s.model())
-    elif result == unsat:
-        print(f"Property holds.")
-    elif result == unknown:
-        print("Timed out or unknown.")
-
-s = Solver()
-
-premiumRayBefore = Int('premiumRayBefore')
-s.add(0 <= premiumRayBefore, premiumRayBefore <= 10**30)
-premiumRestoredRay = Int('premiumRestoredRay')
-s.add(0 <= premiumRestoredRay, premiumRestoredRay <= premiumRayBefore)
-
-premiumRayAfter = premiumRayBefore - premiumRestoredRay
-liquidityIncrease = divUp(premiumRestoredRay, RAY)
-actualPremiumDebtDecrease = divUp(premiumRayBefore, RAY) - divUp(premiumRayAfter, RAY)
-
-s.push()
-# Supply share price does not decrease
-s.add(simplify(actualPremiumDebtDecrease > liquidityIncrease))
-check("Share price does not decrease after repay")
\ No newline at end of file
diff --git a/tests/misc/z3/README.md b/tests/misc/z3/README.md
new file mode 100644
index 000000000..be7518c58
--- /dev/null
+++ b/tests/misc/z3/README.md
@@ -0,0 +1,165 @@
+# Z3 Symbolic Proofs
+
+Symbolic property proofs for Aave v4 math using the [Z3 SMT solver](https://github.com/Z3Prover/z3).
+
+## Dependencies
+
+### Required
+
+- **[uv](https://docs.astral.sh/uv/)** - Python package manager
+
+  ```bash
+  curl -LsSf https://astral.sh/uv/install.sh | sh
+  ```
+
+- **[Python](https://www.python.org/downloads/)** >= 3.13
+
+  ```bash
+  # Verify installation
+  python3 --version
+  ```
+
+### Install Dependencies
+
+```bash
+uv sync
+```
+
+## Usage
+
+Run a proof:
+
+```bash
+uv run tests/misc/z3/max_deposit_property.py
+```
+
+Format code:
+
+```bash
+uv run ruff format tests/misc/z3
+```
+
+## Commons API
+
+All proof scripts import shared constants, math helpers, and proof utilities from `commons.py` via `from commons import *`.
+
+### Proof Utilities
+
+#### `proveValid(s, propertyDescription, property, assumptions=[], variables=[])`
+
+Proves a property holds for **all** variable assignments satisfying the solver's constraints. Internally checks that `Not(property)` is unsatisfiable — if no counterexample exists, the property is universally valid.
+
+**Parameters:**
+
+- `s` — a `Solver()` instance with constraints already added
+- `propertyDescription` — string label printed in output
+- `property` — Z3 boolean expression to prove
+- `assumptions` — optional list of extra Z3 assumptions passed to `s.check()`
+- `variables` — optional list of `(expression, name)` tuples printed if a counterexample is found
+
+```python
+from commons import *
+
+s = Solver()
+
+x = Int('x')
+s.add(x >= 0, x <= 10)
+
+proveValid(s, 'x + 1 > x', x + 1 > x)
+# ✅ Property is valid.
+
+proveValid(s, 'x < 5', x < 5)
+# ❌ Property is not valid:
+# [x = 5]
+```
+
+#### `proveSatisfiable(s, propertyDescription, property, assumptions=[], variables=[])`
+
+Checks that a property **can** hold — i.e. at least one satisfying assignment exists. Useful for finding edge cases or demonstrating that a scenario is reachable.
+
+**Parameters:** same as `proveValid`.
+
+```python
+from commons import *
+
+s = Solver()
+
+x = Int('x')
+s.add(x >= 0, x <= 10)
+
+proveSatisfiable(s, 'x == 7 is reachable', x == 7)
+# ✅ Property is satisfiable
+# [x = 7]
+```
+
+#### `maximise(expression, propertyDescription, assumptions=[], variables=[])`
+
+Finds the **maximum** value of an expression under the given constraints using Z3's `Optimize` solver. Unlike `proveValid`/`proveSatisfiable`, this creates its own solver internally — constraints are passed via `assumptions`.
+
+**Parameters:**
+
+- `expression` — Z3 expression to maximise
+- `propertyDescription` — string label printed in output
+- `assumptions` — list of Z3 constraints
+- `variables` — optional list of `(expression, name)` tuples printed alongside the result
+
+```python
+from commons import *
+
+t = Int('t')
+rate = IntVal(100)
+
+maximise(
+    t,
+    'Maximum t such that rate * t <= 1000',
+    assumptions=[t >= 0, rate * t <= 1000],
+    variables=[(t, 't')],
+)
+# ✅ Maximum found: 10
+# t: 10
+```
+
+### Constants
+
+| Constant                              | Value            | Description                               |
+| ------------------------------------- | ---------------- | ----------------------------------------- |
+| `WAD`                                 | 10^18            | Standard decimal precision                |
+| `RAY`                                 | 10^27            | Ray precision (interest math)             |
+| `PERCENTAGE_FACTOR`                   | 10^4             | Basis points (1 = 0.01%)                  |
+| `VIRTUAL_SHARES`                      | 10^6             | Virtual shares (hub inflation protection) |
+| `VIRTUAL_ASSETS`                      | 10^6             | Virtual assets (hub inflation protection) |
+| `MAX_PRICE`                           | 10^16            | Maximum oracle price                      |
+| `MAX_SUPPLY_AMOUNT`                   | 10^30            | Maximum supply amount bound               |
+| `MAX_SUPPLY_PRICE`                    | 100              | Maximum supply share price                |
+| `MAX_COLLATERAL_RISK`                 | 100,000          | Maximum per-collateral risk premium       |
+| `MIN_DRAWN_INDEX` / `MAX_DRAWN_INDEX` | RAY / 100 \* RAY | Drawn index range                         |
+| `MIN_DECIMALS` / `MAX_DECIMALS`       | 6 / 18           | Token decimal range                       |
+| `UINT256_MAX`                         | 2^256 - 1        | Solidity uint256 max value                |
+| `SECONDS_PER_YEAR`                    | 31,536,000       | Seconds in a year (365 days)              |
+
+### Math Helpers
+
+All math helpers operate on Z3 symbolic expressions and mirror the Solidity implementations.
+
+| Function                                                  | Description                               |
+| --------------------------------------------------------- | ----------------------------------------- |
+| `mulDivDown(a, num, den)`                                 | `(a * num) / den` (rounds down)           |
+| `mulDivUp(a, num, den)`                                   | `(a * num + den - 1) / den` (rounds up)   |
+| `divUp(a, b)`                                             | `(a + b - 1) / b`                         |
+| `rayMulUp(a, b)` / `rayMulDown(a, b)`                     | Multiply in ray precision                 |
+| `fromRayDown(a)` / `fromRayUp(a)`                         | Convert from ray to wad                   |
+| `toRay(a)`                                                | Convert to ray                            |
+| `percentMulUp(value, pct)` / `percentMulDown(value, pct)` | Percentage multiplication in basis points |
+| `zeroFloorSub(a, b)`                                      | `max(a - b, 0)`                           |
+| `min(a, b)`                                               | Z3-safe minimum via `If`                  |
+
+### Share/Asset Conversion Helpers
+
+| Function                                          | Rounding  | Use case                          |
+| ------------------------------------------------- | --------- | --------------------------------- |
+| `toAddedSharesDown(assets, totalAssets, shares)`  | Down      | Deposit: assets to shares         |
+| `toAddedAssetsDown(shares, totalAssets, shares)`  | Down      | Redeem: shares to assets          |
+| `toAddedSharesUp(assets, totalAssets, shares)`    | Up        | Withdraw: assets to shares burned |
+| `toAddedAssetsUp(shares, totalAssets, shares)`    | Up        | Mint: shares to assets required   |
+| `previewAddByAssets` / `previewAddByShares`       | Down / Up | Preview deposit/mint              |
+| `previewRemoveByAssets` / `previewRemoveByShares` | Up / Down | Preview withdraw/redeem           |
diff --git a/tests/misc/z3/calculate_linear_interest.py b/tests/misc/z3/calculate_linear_interest.py
new file mode 100644
index 000000000..b699bb42c
--- /dev/null
+++ b/tests/misc/z3/calculate_linear_interest.py
@@ -0,0 +1,17 @@
+from commons import *
+
+rate = IntVal(2**96 - 1)
+lastUpdateTimestamp = IntVal(1)
+currentTimestamp = Int('currentTimestamp')
+elapsed = currentTimestamp - lastUpdateTimestamp
+
+maximise(
+    currentTimestamp,
+    'Maximum currentTimestamp for calculateLinearInterest',
+    assumptions=[
+        elapsed >= 0,
+        rate * elapsed <= UINT256_MAX,
+        RAY + ((rate * elapsed) / SECONDS_PER_YEAR) <= UINT256_MAX,
+    ],
+    variables=[(currentTimestamp, 'currentTimestamp')],
+)
diff --git a/tests/misc/z3/commons.py b/tests/misc/z3/commons.py
index a2617772d..881f864c0 100644
--- a/tests/misc/z3/commons.py
+++ b/tests/misc/z3/commons.py
@@ -16,11 +16,15 @@
 MIN_DRAWN_INDEX = RAY
 MAX_DRAWN_INDEX = 100 * RAY
 MAX_SUPPLY_PRICE = IntVal(100)
+MAX_COLLATERAL_RISK = IntVal(1000_00)
 
 MIN_LIQUIDATION_BONUS = PERCENTAGE_FACTOR
 MAX_LIQUIDATION_BONUS = PERCENTAGE_FACTOR * PERCENTAGE_FACTOR - 1
 DUST_LIQUIDATION_THRESHOLD = IntVal(1000 * 10**26)
 
+UINT256_MAX = IntVal(2**256 - 1)
+SECONDS_PER_YEAR = IntVal(365 * 24 * 60 * 60)
+
 
 def mulDivDown(a, num, den):
     return (a * num) / den
@@ -53,12 +57,23 @@ def fromRayUp(a):
 def toRay(a):
     return a * RAY
 
+
 def min(a, b):
     return If(a <= b, a, b)
 
+
+def percentMulUp(value, percentage):
+    return (value * percentage + PERCENTAGE_FACTOR - 1) / PERCENTAGE_FACTOR
+
+
+def percentMulDown(value, percentage):
+    return (value * percentage) / PERCENTAGE_FACTOR
+
+
 def zeroFloorSub(a, b):
     return If(a > b, a - b, 0)
 
+
 def toAddedSharesDown(assets, totalAddedAssets, addedShares):
     return mulDivDown(
         assets, addedShares + VIRTUAL_SHARES, totalAddedAssets + VIRTUAL_ASSETS
@@ -105,39 +120,64 @@ def toValue(amount, decimals, price):
 
 
 def proveValid(s, propertyDescription, property, assumptions=[], variables=[]):
-    propertyDescriptionOutput = f"-- VALID Property: {propertyDescription} --"
-    print("=" * len(propertyDescriptionOutput))
+    propertyDescriptionOutput = f'-- VALID Property: {propertyDescription} --'
+    print('=' * len(propertyDescriptionOutput))
     print(propertyDescriptionOutput)
 
     result = s.check(Not(property), *assumptions)
     if result == sat:
-        print("❌ Property is not valid:")
+        print('❌ Property is not valid:')
         print(s.model())
         for variable, variableName in variables:
-            print(f"{variableName}: {s.model().eval(variable)}")
+            print(f'{variableName}: {s.model().eval(variable)}')
     elif result == unsat:
-        print(f"✅ Property is valid.")
+        print(f'✅ Property is valid.')
     elif result == unknown:
-        print("❓ Timed out or unknown.")
+        print('❓ Timed out or unknown.')
 
-    print("=" * len(propertyDescriptionOutput))
+    print('=' * len(propertyDescriptionOutput))
 
 
 def proveSatisfiable(s, propertyDescription, property, assumptions=[], variables=[]):
-    propertyDescriptionOutput = f"-- SATISFIABLE Property: {propertyDescription} --"
-    print("=" * len(propertyDescriptionOutput))
+    propertyDescriptionOutput = f'-- SATISFIABLE Property: {propertyDescription} --'
+    print('=' * len(propertyDescriptionOutput))
     print(propertyDescriptionOutput)
 
     result = s.check(property, *assumptions)
     if result == sat:
-        print("✅ Property is satisfiable")
+        print('✅ Property is satisfiable')
         m = s.model()
         print(m)
         for variable, variableName in variables:
-            print(f"{variableName}: {m.eval(variable)}")
+            print(f'{variableName}: {m.eval(variable)}')
+    elif result == unsat:
+        print('❌ Property is unsatisfiable.')
+    elif result == unknown:
+        print('❓ Timed out or unknown.')
+
+    print('=' * len(propertyDescriptionOutput))
+
+
+def maximise(expression, propertyDescription, assumptions=[], variables=[]):
+    propertyDescriptionOutput = f'-- MAXIMISE: {propertyDescription} --'
+    print('=' * len(propertyDescriptionOutput))
+    print(propertyDescriptionOutput)
+
+    s = Optimize()
+    for assumption in assumptions:
+        s.add(assumption)
+
+    s.maximize(expression)
+
+    result = s.check()
+    if result == sat:
+        m = s.model()
+        print(f'✅ Maximum found: {m.eval(expression)}')
+        for variable, variableName in variables:
+            print(f'{variableName}: {m.eval(variable)}')
     elif result == unsat:
-        print("❌ Property is unsatisfiable.")
+        print('❌ Unsatisfiable (no maximum).')
     elif result == unknown:
-        print("❓ Timed out or unknown.")
+        print('❓ Timed out or unknown.')
 
-    print("=" * len(propertyDescriptionOutput))
+    print('=' * len(propertyDescriptionOutput))
diff --git a/tests/misc/z3/debt_to_liquidate.py b/tests/misc/z3/debt_to_liquidate.py
index 5b5583dd8..cfabbaa1d 100644
--- a/tests/misc/z3/debt_to_liquidate.py
+++ b/tests/misc/z3/debt_to_liquidate.py
@@ -3,10 +3,10 @@
 
 s = Solver()
 
-debtToCover = Int("debtToCover")
+debtToCover = Int('debtToCover')
 s.add(0 <= debtToCover, debtToCover <= MAX_SUPPLY_AMOUNT)
 
-rawPremiumDebtRayToLiquidate = Int("rawPremiumDebtRayToLiquidate")
+rawPremiumDebtRayToLiquidate = Int('rawPremiumDebtRayToLiquidate')
 s.add(
     0 <= rawPremiumDebtRayToLiquidate, rawPremiumDebtRayToLiquidate <= MAX_SUPPLY_AMOUNT
 )
@@ -25,7 +25,7 @@
 
 proveValid(
     s,
-    "debtToCover is enforced correctly when premiumDebtRayToLiquidate is calculated",
+    'debtToCover is enforced correctly when premiumDebtRayToLiquidate is calculated',
     actualPremiumDebtRayToLiquidate == expectedPremiumDebtRayToLiquidate,
 )
 
@@ -37,6 +37,6 @@
 
 proveValid(
     s,
-    "debtToCover is enforced correctly when premiumDebtRayToLiquidate is calculated",
+    'debtToCover is enforced correctly when premiumDebtRayToLiquidate is calculated',
     actualPremiumDebtRayToLiquidate2 == expectedPremiumDebtRayToLiquidate,
 )
diff --git a/tests/misc/z3/liquidation_logic.py b/tests/misc/z3/liquidation_logic.py
index f72171e0a..35517a50b 100644
--- a/tests/misc/z3/liquidation_logic.py
+++ b/tests/misc/z3/liquidation_logic.py
@@ -4,46 +4,46 @@
 s = Solver()
 
 # Pricing of collateral asset
-addedShares = Int("addedShares")
+addedShares = Int('addedShares')
 s.add(0 <= addedShares, addedShares <= MAX_SUPPLY_AMOUNT)
-totalAddedAssets = Int("totalAddedAssets")
+totalAddedAssets = Int('totalAddedAssets')
 s.add(
     (addedShares + VIRTUAL_SHARES) <= (totalAddedAssets + VIRTUAL_ASSETS),
     (totalAddedAssets + VIRTUAL_ASSETS)
     <= MAX_SUPPLY_PRICE * (addedShares + VIRTUAL_SHARES),
 )
-collateralAssetPrice = Int("collateralAssetPrice")
+collateralAssetPrice = Int('collateralAssetPrice')
 s.add(1 <= collateralAssetPrice, collateralAssetPrice <= MAX_PRICE)
-collateralAssetDecimals = Int("collateralAssetDecimals")
+collateralAssetDecimals = Int('collateralAssetDecimals')
 s.add(MIN_DECIMALS <= collateralAssetDecimals, collateralAssetDecimals <= MAX_DECIMALS)
 collateralAssetUnit = ToInt(10**collateralAssetDecimals)
 
 # Pricing of debt asset
-drawnIndex = Int("drawnIndex")
+drawnIndex = Int('drawnIndex')
 s.add(MIN_DRAWN_INDEX <= drawnIndex, drawnIndex <= MAX_DRAWN_INDEX)
-debtAssetPrice = Int("debtAssetPrice")
+debtAssetPrice = Int('debtAssetPrice')
 s.add(1 <= debtAssetPrice, debtAssetPrice <= MAX_PRICE)
-debtAssetDecimals = Int("debtAssetDecimals")
+debtAssetDecimals = Int('debtAssetDecimals')
 s.add(MIN_DECIMALS <= debtAssetDecimals, debtAssetDecimals <= MAX_DECIMALS)
 debtAssetUnit = ToInt(10**debtAssetDecimals)
 
 # Liquidatable user position
-suppliedShares = Int("suppliedShares")
+suppliedShares = Int('suppliedShares')
 s.add(1 <= suppliedShares, suppliedShares <= addedShares)
-drawnShares = Int("drawnShares")
+drawnShares = Int('drawnShares')
 s.add(1 <= drawnShares, drawnShares <= MAX_SUPPLY_AMOUNT)
-premiumDebtRay = Int("premiumDebtRay")
+premiumDebtRay = Int('premiumDebtRay')
 s.add(0 <= premiumDebtRay, premiumDebtRay <= MAX_SUPPLY_AMOUNT)
 
 # Liquidation parameters
-liquidationBonus = Int("liquidationBonus")
+liquidationBonus = Int('liquidationBonus')
 s.add(
     MIN_LIQUIDATION_BONUS <= liquidationBonus,
     liquidationBonus <= MAX_LIQUIDATION_BONUS,
 )
-premiumDebtRayToLiquidate = Int("premiumDebtRayToLiquidate")
+premiumDebtRayToLiquidate = Int('premiumDebtRayToLiquidate')
 s.add(0 <= premiumDebtRayToLiquidate, premiumDebtRayToLiquidate <= premiumDebtRay)
-rawDrawnSharesToLiquidate = Int("rawDrawnSharesToLiquidate")
+rawDrawnSharesToLiquidate = Int('rawDrawnSharesToLiquidate')
 s.add(0 <= rawDrawnSharesToLiquidate, rawDrawnSharesToLiquidate <= drawnShares)
 s.add(Or(rawDrawnSharesToLiquidate == 0, premiumDebtRayToLiquidate == premiumDebtRay))
 
@@ -62,7 +62,7 @@
     )
     < DUST_LIQUIDATION_THRESHOLD * RAY,
 )
-drawnSharesToLiquidate = Int("drawnSharesToLiquidate")
+drawnSharesToLiquidate = Int('drawnSharesToLiquidate')
 s.add(
     Or(
         And(Not(leavesDebtDust), drawnSharesToLiquidate == rawDrawnSharesToLiquidate),
diff --git a/tests/misc/z3/liquidity_growth.py b/tests/misc/z3/liquidity_growth.py
new file mode 100644
index 000000000..5f99e36ef
--- /dev/null
+++ b/tests/misc/z3/liquidity_growth.py
@@ -0,0 +1,30 @@
+# Highlights the fact that liquidity growth cannot be calculated accurately using the index delta.
+from commons import *
+
+base = Int('base')
+premium = Int('premium')
+index1 = Int('index1')
+index2 = Int('index2')
+
+s = Solver()
+
+s.add(RAY <= index1, index1 < index2, index2 <= 100 * RAY)
+s.add(0 <= base, base <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= premium, premium <= MAX_SUPPLY_AMOUNT)
+
+trueLiquidityGrowth = (
+    rayMulUp(base, index2)
+    - rayMulUp(base, index1)
+    + rayMulUp(premium, index2)
+    - rayMulUp(premium, index1)
+)
+x = rayMulDown(base, index2 - index1) + rayMulDown(
+    premium, index2 - index1
+)  # incorrect -- it underestimates the liquidity growth
+# x = rayMulDown(base + premium, index2 - index1) # incorrect -- it overestimates the liquidity growth
+
+proveValid(
+    s,
+    'Liquidity growth via index delta equals true liquidity growth (expected: invalid)',
+    trueLiquidityGrowth == x,
+)
diff --git a/tests/misc/z3/max_deposit_property.py b/tests/misc/z3/max_deposit_property.py
index 9fdf6afdb..cfcb9174b 100644
--- a/tests/misc/z3/max_deposit_property.py
+++ b/tests/misc/z3/max_deposit_property.py
@@ -2,16 +2,16 @@
 # _validateAdd checks: allowed >= toAddedAssetsUp(spokeShares) + depositAmount
 from commons import *
 
-totalAddedAssets = Int("totalAddedAssets")
-totalAddedShares = Int("totalAddedShares")
-spokeShares = Int("spokeShares")
-allowed = Int("allowed")
+totalAddedAssets = Int('totalAddedAssets')
+totalAddedShares = Int('totalAddedShares')
+spokeShares = Int('spokeShares')
+allowed = Int('allowed')
 
 s = Solver()
-s.add(0 <= totalAddedAssets, totalAddedAssets <= 10**30)
-s.add(0 <= totalAddedShares, totalAddedShares <= 10**30)
+s.add(0 <= totalAddedAssets, totalAddedAssets <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= totalAddedShares, totalAddedShares <= MAX_SUPPLY_AMOUNT)
 s.add(0 <= spokeShares, spokeShares <= totalAddedShares)
-s.add(0 < allowed, allowed <= 10**30)
+s.add(0 < allowed, allowed <= MAX_SUPPLY_AMOUNT)
 
 balance = toAddedAssetsUp(spokeShares, totalAddedAssets, totalAddedShares)
 depositAmount = zeroFloorSub(allowed, balance)
@@ -20,4 +20,4 @@
 )
 s.add(depositAmount > 0)
 
-proveValid(s, "deposit(maxDeposit()) satisfies _validateAdd", allowed >= hubCheck)
+proveValid(s, 'deposit(maxDeposit()) satisfies _validateAdd', allowed >= hubCheck)
diff --git a/tests/misc/z3/max_mint_property.py b/tests/misc/z3/max_mint_property.py
index eaf816971..db4bff604 100644
--- a/tests/misc/z3/max_mint_property.py
+++ b/tests/misc/z3/max_mint_property.py
@@ -4,30 +4,33 @@
 # _validateAdd checks: allowed >= toAddedAssetsUp(spokeShares) + assets
 from commons import *
 
+
 def previewMint(shares, totalAddedAssets, totalAddedShares):
     """Converts shares to assets, rounding up (previewAddByShares)"""
     return previewAddByShares(shares, totalAddedAssets, totalAddedShares)
 
+
 def convertToShares(assets, totalAddedAssets, totalAddedShares):
     """Converts assets to shares, rounding down (previewAddByAssets)"""
     return previewAddByAssets(assets, totalAddedAssets, totalAddedShares)
 
-totalAddedAssets = Int("totalAddedAssets")
-totalAddedShares = Int("totalAddedShares")
-spokeShares = Int("spokeShares")
-allowed = Int("allowed")
+
+totalAddedAssets = Int('totalAddedAssets')
+totalAddedShares = Int('totalAddedShares')
+spokeShares = Int('spokeShares')
+allowed = Int('allowed')
 
 s = Solver()
-s.add(0 <= totalAddedAssets, totalAddedAssets <= 10**30)
-s.add(0 <= totalAddedShares, totalAddedShares <= 10**30)
+s.add(0 <= totalAddedAssets, totalAddedAssets <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= totalAddedShares, totalAddedShares <= MAX_SUPPLY_AMOUNT)
 s.add(0 <= spokeShares, spokeShares <= totalAddedShares)
-s.add(0 < allowed, allowed <= 10**30)
+s.add(0 < allowed, allowed <= MAX_SUPPLY_AMOUNT)
 
 # maxDeposit
 balance = previewMint(spokeShares, totalAddedAssets, totalAddedShares)
 maxDepositAmount = zeroFloorSub(allowed, balance)
 
-# maxMint = convertToShares(maxDeposit) 
+# maxMint = convertToShares(maxDeposit)
 maxMintShares = convertToShares(maxDepositAmount, totalAddedAssets, totalAddedShares)
 
 # _validateAdd: allowed >= toAddedAssetsUp(spokeShares) + mintAssets
@@ -35,4 +38,4 @@ def convertToShares(assets, totalAddedAssets, totalAddedShares):
 s.add(mintAssets > 0)
 hubCheck = toAddedAssetsUp(spokeShares, totalAddedAssets, totalAddedShares) + mintAssets
 
-proveValid(s, "mint(maxMint()) satisfies _validateAdd", allowed >= hubCheck)
+proveValid(s, 'mint(maxMint()) satisfies _validateAdd', allowed >= hubCheck)
diff --git a/tests/misc/z3/max_redeem_property.py b/tests/misc/z3/max_redeem_property.py
index 65af1e90b..1b54e5b72 100644
--- a/tests/misc/z3/max_redeem_property.py
+++ b/tests/misc/z3/max_redeem_property.py
@@ -6,25 +6,28 @@
 # toAddedSharesUp(previewRedeem(result)) <= balance — Hub.remove share deduction doesn't exceed spoke shares
 from commons import *
 
+
 def previewRedeem(shares, totalAddedAssets, totalAddedShares):
     """Converts shares to assets, rounding down (previewRemoveByShares)"""
     return previewRemoveByShares(shares, totalAddedAssets, totalAddedShares)
 
+
 def convertToShares(assets, totalAddedAssets, totalAddedShares):
     """Converts assets to shares, rounding down (previewAddByAssets)"""
     return previewAddByAssets(assets, totalAddedAssets, totalAddedShares)
 
+
 s = Solver()
 
-totalAddedAssets = Int("totalAddedAssets")
-totalAddedShares = Int("totalAddedShares")
-maxRemovableAssets = Int("maxRemovableAssets")
-balance = Int("balance")  # balanceOf(owner) in shares
+totalAddedAssets = Int('totalAddedAssets')
+totalAddedShares = Int('totalAddedShares')
+maxRemovableAssets = Int('maxRemovableAssets')
+balance = Int('balance')  # balanceOf(owner) in shares
 
-s.add(0 <= totalAddedAssets, totalAddedAssets <= 10**30)
-s.add(0 <= totalAddedShares, totalAddedShares <= 10**30)
-s.add(0 <= maxRemovableAssets, maxRemovableAssets <= 10**30)
-s.add(0 <= balance, balance <= 10**30)
+s.add(0 <= totalAddedAssets, totalAddedAssets <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= totalAddedShares, totalAddedShares <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= maxRemovableAssets, maxRemovableAssets <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= balance, balance <= MAX_SUPPLY_AMOUNT)
 # maxRemovableAssets is just liquidity, which is part of totalAddedAssets
 s.add(maxRemovableAssets <= totalAddedAssets)
 
@@ -37,7 +40,15 @@ def convertToShares(assets, totalAddedAssets, totalAddedShares):
 hubRemoveShares = toAddedSharesUp(resultAssets, totalAddedAssets, totalAddedShares)
 
 # redeemed assets don't exceed liquidity
-proveValid(s, "previewRedeem(balance.min(maxRemovableShares)) <= _maxRemovableAssets()", resultAssets <= maxRemovableAssets)
+proveValid(
+    s,
+    'previewRedeem(balance.min(maxRemovableShares)) <= _maxRemovableAssets()',
+    resultAssets <= maxRemovableAssets,
+)
 
 # redeem(maxRedeem()) — Hub.remove share deduction doesn't exceed spoke shares
-proveValid(s, "toAddedSharesUp(previewRedeem(maxRedeem())) <= balance", hubRemoveShares <= balance)
+proveValid(
+    s,
+    'toAddedSharesUp(previewRedeem(maxRedeem())) <= balance',
+    hubRemoveShares <= balance,
+)
diff --git a/tests/misc/z3/max_withdraw_property.py b/tests/misc/z3/max_withdraw_property.py
index 7ed6c6737..3d2d77a4e 100644
--- a/tests/misc/z3/max_withdraw_property.py
+++ b/tests/misc/z3/max_withdraw_property.py
@@ -6,34 +6,43 @@
 # previewWithdraw(result) <= balanceShares — shares burned don't exceed owner's balance
 from commons import *
 
+
 def previewRedeem(shares, totalAddedAssets, totalAddedShares):
     """Converts shares to assets, rounding down (previewRemoveByShares)"""
     return previewRemoveByShares(shares, totalAddedAssets, totalAddedShares)
 
+
 def previewWithdraw(assets, totalAddedAssets, totalAddedShares):
     """Converts assets to shares, rounding up (previewRemoveByAssets)"""
     return previewRemoveByAssets(assets, totalAddedAssets, totalAddedShares)
 
+
 s = Solver()
 
-totalAddedAssets = Int("totalAddedAssets")
-totalAddedShares = Int("totalAddedShares")
-maxRemovableAssets = Int("maxRemovableAssets")
-balanceShares = Int("balanceShares")  # balanceOf(owner) in shares
+totalAddedAssets = Int('totalAddedAssets')
+totalAddedShares = Int('totalAddedShares')
+maxRemovableAssets = Int('maxRemovableAssets')
+balanceShares = Int('balanceShares')  # balanceOf(owner) in shares
 
 balanceAssets = previewRedeem(balanceShares, totalAddedAssets, totalAddedShares)
 result = min(balanceAssets, maxRemovableAssets)
 sharesBurned = previewWithdraw(result, totalAddedAssets, totalAddedShares)
 
-s.add(0 <= totalAddedAssets, totalAddedAssets <= 10**30)
-s.add(0 <= totalAddedShares, totalAddedShares <= 10**30)
-s.add(0 <= maxRemovableAssets, maxRemovableAssets <= 10**30)
-s.add(0 <= balanceShares, balanceShares <= 10**30)
+s.add(0 <= totalAddedAssets, totalAddedAssets <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= totalAddedShares, totalAddedShares <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= maxRemovableAssets, maxRemovableAssets <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= balanceShares, balanceShares <= MAX_SUPPLY_AMOUNT)
 # maxRemovableAssets is just liquidity, which is part of totalAddedAssets
 s.add(maxRemovableAssets <= totalAddedAssets)
 
 # maxWithdraw result does not exceed liquidity
-proveValid(s, "min(previewRedeem(balanceShares), maxRemovableAssets) <= _maxRemovableAssets()", result <= maxRemovableAssets)
+proveValid(
+    s,
+    'min(previewRedeem(balanceShares), maxRemovableAssets) <= _maxRemovableAssets()',
+    result <= maxRemovableAssets,
+)
 
 # withdraw(maxWithdraw()) — shares burned don't exceed owner's balance
-proveValid(s, "previewWithdraw(maxWithdraw()) <= balanceShares", sharesBurned <= balanceShares)
+proveValid(
+    s, 'previewWithdraw(maxWithdraw()) <= balanceShares', sharesBurned <= balanceShares
+)
diff --git a/tests/misc/premium.py b/tests/misc/z3/premium.py
similarity index 52%
rename from tests/misc/premium.py
rename to tests/misc/z3/premium.py
index 7ccc92d62..e68227370 100644
--- a/tests/misc/premium.py
+++ b/tests/misc/z3/premium.py
@@ -1,37 +1,34 @@
-from z3 import *
+from commons import *
 
-RAY = IntVal(10**27)
-rayMulUp = lambda a, b: (a * b + RAY - 1) / RAY
-rayMulDown = lambda a, b: (a * b) / RAY
-premiumDebt = (
-    lambda shares, offset, realized: rayMulUp(shares, index) - offset + realized
+premiumDebt = lambda shares, offset, realized: (
+    rayMulUp(shares, index) - offset + realized
 )
 
 # global asset state
-index = Int("index")
-premiumShares = Int("premiumShares")
-premiumOffset = Int("premiumOffset")
-realizedPremium = Int("realizedPremium")
+index = Int('index')
+premiumShares = Int('premiumShares')
+premiumOffset = Int('premiumOffset')
+realizedPremium = Int('realizedPremium')
 
 s = Solver()
 
 s.add(RAY <= index, index <= 100 * RAY)
-s.add(0 <= premiumShares, premiumShares <= 10**30)
-s.add(0 <= premiumOffset, premiumOffset <= 10**30)
-s.add(0 <= realizedPremium, realizedPremium <= 10**30)
+s.add(0 <= premiumShares, premiumShares <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= premiumOffset, premiumOffset <= MAX_SUPPLY_AMOUNT)
+s.add(0 <= realizedPremium, realizedPremium <= MAX_SUPPLY_AMOUNT)
 s.add(rayMulDown(premiumShares, index) >= premiumOffset)
 
 # choose user's old position
-ps_old = Int("ps_old")
-po_old = Int("po_old")
+ps_old = Int('ps_old')
+po_old = Int('po_old')
 s.add(0 <= ps_old, ps_old <= premiumShares)
 s.add(0 <= po_old, po_old <= premiumOffset)
 accrued = rayMulUp(ps_old, index) - po_old
 s.add(0 <= accrued, accrued <= rayMulUp(premiumShares, index) - premiumOffset)
 
 # user's new position
-ps_new = Int("ps_new")
-s.add(0 <= ps_new, ps_new <= 10**30)
+ps_new = Int('ps_new')
+s.add(0 <= ps_new, ps_new <= MAX_SUPPLY_AMOUNT)
 po_new = rayMulDown(ps_new, index)
 
 # replace user's old position with the new one
@@ -46,6 +43,8 @@
     realizedPremium + realizedPremiumDelta,
 )
 
-s.add(Not(And(after >= before, after - before <= 2)))
-
-print(s.model() if s.check() == sat else "no counterexample")
\ No newline at end of file
+proveValid(
+    s,
+    'Premium debt change bounded by [0, 2] after position replacement',
+    And(after >= before, after - before <= 2),
+)
diff --git a/tests/misc/risk_premium_threshold_overshoot.py b/tests/misc/z3/risk_premium_threshold_overshoot.py
similarity index 81%
rename from tests/misc/risk_premium_threshold_overshoot.py
rename to tests/misc/z3/risk_premium_threshold_overshoot.py
index ed8183842..c4f8d14f6 100644
--- a/tests/misc/risk_premium_threshold_overshoot.py
+++ b/tests/misc/z3/risk_premium_threshold_overshoot.py
@@ -1,12 +1,6 @@
 # Proves that the proposed RiskPremiumThreshold formula strictly bounds the aggregate risk premium
 # for any number of users, given any individual risk premium <= MAX_COLLATERAL_RISK.
-from z3 import *
-
-PERCENTAGE_FACTOR = IntVal(100_00)
-MAX_COLLATERAL_RISK = IntVal(1000_00)
-
-def percentMulUp(value, percentage):
-    return (value * percentage + PERCENTAGE_FACTOR - 1) / PERCENTAGE_FACTOR
+from commons import *
 
 # ∀ drawnShares_i ≥ 1, ∀ riskPremium_i ≤ MAX_COLLATERAL_RISK,
 # we want to minimize RISK_PREMIUM_THRESHOLD such that:
@@ -35,11 +29,14 @@ def percentMulUp(value, percentage):
 s = Solver()
 
 s.add(1 <= N)
-s.add(0 <= drawnShares, drawnShares <= 10 ** 30)
+s.add(0 <= drawnShares, drawnShares <= MAX_SUPPLY_AMOUNT)
 s.add(0 <= riskPremium, riskPremium <= MAX_COLLATERAL_RISK)
 
 totalDrawn = N * drawnShares
 premiumShares = percentMulUp(drawnShares, riskPremium)
-s.add(Not(N * premiumShares <= percentMulUp(totalDrawn, RISK_PREMIUM_THRESHOLD)))
 
-print(s.model() if s.check() == sat else 'no counterexample')
+proveValid(
+    s,
+    'Risk premium threshold bounds aggregate risk premium for any number of users',
+    N * premiumShares <= percentMulUp(totalDrawn, RISK_PREMIUM_THRESHOLD),
+)
diff --git a/tests/misc/risk_premium_weighted_average_bound.py b/tests/misc/z3/risk_premium_weighted_average_bound.py
similarity index 56%
rename from tests/misc/risk_premium_weighted_average_bound.py
rename to tests/misc/z3/risk_premium_weighted_average_bound.py
index 086bb5432..887f37eba 100644
--- a/tests/misc/risk_premium_weighted_average_bound.py
+++ b/tests/misc/z3/risk_premium_weighted_average_bound.py
@@ -1,15 +1,6 @@
 # Proves the maximum risk premium for a user computed by a spoke is bounded to MAX_ALLOWED_COLLATERAL_RISK
 # divUp(sum(percentMulUp(w_i, rp_i)), sum(w_i)) <= rp_max when rp_i <= rp_max for all i.
-from z3 import *
-
-MAX_RP = IntVal(1000_00) # MAX_ALLOWED_COLLATERAL_RISK
-PERCENTAGE_FACTOR = IntVal(100_00)
-
-def divUp(numerator, denominator):
-    return (numerator + denominator - 1) / denominator
-
-def percentMulUp(value, percentage):
-    return (value * percentage + PERCENTAGE_FACTOR - 1) / PERCENTAGE_FACTOR
+from commons import *
 
 s = Solver()
 
@@ -22,7 +13,10 @@ def percentMulUp(value, percentage):
 # rp_i <= rp_max
 # implies; percentMulUp(w_i * rp_i) <= percentMulUp(w_i * rp_max)
 # implies; sum(percentMulUp(w_i * rp_i)) <= sum(percentMulUp(w_i * rp_max)) <= percentMulUp(sum(w_i) * rp_max) <= sum(w_i) * rp_max
-s.add(weightedSum <= percentMulUp(sumOfWeights, MAX_RP))
+s.add(weightedSum <= percentMulUp(sumOfWeights, MAX_COLLATERAL_RISK))
 
-s.add(Not(divUp(weightedSum, sumOfWeights) <= MAX_RP))
-print(s.model() if s.check() == sat else 'no counterexample')
+proveValid(
+    s,
+    'Weighted average risk premium is bounded by MAX_COLLATERAL_RISK',
+    divUp(weightedSum, sumOfWeights) <= MAX_COLLATERAL_RISK,
+)
diff --git a/tests/misc/z3/share_assets_conversion.py b/tests/misc/z3/share_assets_conversion.py
new file mode 100644
index 000000000..25fadc6a3
--- /dev/null
+++ b/tests/misc/z3/share_assets_conversion.py
@@ -0,0 +1,28 @@
+# Highlights the fact that supplies shares are always equal to removed shares (after doing the conversion to assets and back to shares).
+from commons import *
+
+s = Solver()
+
+totalAddedAssets = Int('totalAddedAssets')
+s.add(0 <= totalAddedAssets, totalAddedAssets <= MAX_SUPPLY_AMOUNT)
+totalAddedShares = Int('totalAddedShares')
+s.add(
+    totalAddedAssets >= totalAddedShares,
+    totalAddedAssets + VIRTUAL_ASSETS
+    < (totalAddedShares + VIRTUAL_SHARES) * MAX_SUPPLY_PRICE,
+)
+suppliedShares = Int('suppliedShares')
+s.add(0 <= suppliedShares, suppliedShares <= totalAddedShares)
+
+withdrawableAssets = previewRemoveByShares(
+    suppliedShares, totalAddedAssets, totalAddedShares
+)
+removedShares = previewRemoveByAssets(
+    withdrawableAssets, totalAddedAssets, totalAddedShares
+)
+
+proveValid(
+    s,
+    'Supplied shares are always equal to removed shares (after conversion to assets and back to shares)',
+    removedShares == suppliedShares,
+)
diff --git a/tests/misc/z3/supply_share_price_deficit.py b/tests/misc/z3/supply_share_price_deficit.py
new file mode 100644
index 000000000..16db759e3
--- /dev/null
+++ b/tests/misc/z3/supply_share_price_deficit.py
@@ -0,0 +1,41 @@
+# Highlights the fact that totalAddedAssets does not decrease when a deficit is reported (hence the share price does not decrease).
+from commons import *
+
+
+def totalAddedAssets(drawnShares, premiumDebtRay, deficitRay, drawnIndex):
+    # return rayMulUp(drawnShares, drawnIndex) + fromRayUp(premiumDebtRay) + fromRayUp(deficitRay)          # this is wrong
+    # return rayMulDown(drawnShares, drawnIndex) + fromRayDown(premiumDebtRay) + fromRayDown(deficitRay)    # this is wrong
+    return fromRayUp(drawnShares * drawnIndex + premiumDebtRay + deficitRay)
+
+
+s = Solver()
+
+drawnShares = Int('drawnShares')
+s.add(1 <= drawnShares, drawnShares <= MAX_SUPPLY_AMOUNT)
+drawnIndex = Int('drawnIndex')
+s.add(RAY <= drawnIndex, drawnIndex < 100 * RAY)
+premiumDebtRay = Int('premiumDebtRay')
+s.add(0 <= premiumDebtRay, premiumDebtRay <= MAX_SUPPLY_AMOUNT)
+deficitRay = Int('deficitRay')
+s.add(0 <= deficitRay, deficitRay <= MAX_SUPPLY_AMOUNT)
+
+deficitDrawnShares = Int('deficitDrawnShares')
+s.add(0 <= deficitDrawnShares, deficitDrawnShares <= drawnShares)
+deficitPremiumDebtRay = Int('deficitPremiumDebtRay')
+s.add(0 <= deficitPremiumDebtRay, deficitPremiumDebtRay <= premiumDebtRay)
+
+totalAddedAssetsBefore = totalAddedAssets(
+    drawnShares, premiumDebtRay, deficitRay, drawnIndex
+)
+totalAddedAssetsAfter = totalAddedAssets(
+    drawnShares - deficitDrawnShares,
+    premiumDebtRay - deficitPremiumDebtRay,
+    deficitRay + deficitDrawnShares * drawnIndex + deficitPremiumDebtRay,
+    drawnIndex,
+)
+
+proveValid(
+    s,
+    'Total added assets does not decrease after deficit is reported',
+    totalAddedAssetsAfter >= totalAddedAssetsBefore,
+)
diff --git a/tests/misc/z3/supply_share_price_fees.py b/tests/misc/z3/supply_share_price_fees.py
new file mode 100644
index 000000000..506c1e81c
--- /dev/null
+++ b/tests/misc/z3/supply_share_price_fees.py
@@ -0,0 +1,166 @@
+# Highlights the fact that the supply share price does not decrease between accruals/previews due to fees.
+# Note that minting fee shares is equivalent to an add operation, which is known to not decrease the share price.
+from commons import *
+
+
+def premiumDebtRay(realizedPremiumRay, premiumShares, drawnIndex, premiumOffsetRay):
+    return realizedPremiumRay + premiumShares * drawnIndex - premiumOffsetRay
+
+
+def totalDebt(
+    drawnShares,
+    drawnIndex,
+    realizedPremiumRay,
+    premiumShares,
+    premiumOffsetRay,
+    deficitRay,
+):
+    return fromRayUp(
+        drawnShares * drawnIndex
+        + premiumDebtRay(
+            realizedPremiumRay, premiumShares, drawnIndex, premiumOffsetRay
+        )
+        + deficitRay
+    )
+
+
+def unrealizedFeeAmount(
+    drawnShares,
+    previousIndex,
+    drawnIndex,
+    realizedPremiumRay,
+    premiumShares,
+    premiumOffsetRay,
+    deficitRay,
+    liquidityFee,
+):
+    totalDebtAfter = totalDebt(
+        drawnShares,
+        drawnIndex,
+        realizedPremiumRay,
+        premiumShares,
+        premiumOffsetRay,
+        deficitRay,
+    )
+    totalDebtBefore = totalDebt(
+        drawnShares,
+        previousIndex,
+        realizedPremiumRay,
+        premiumShares,
+        premiumOffsetRay,
+        deficitRay,
+    )
+    return percentMulDown(totalDebtAfter - totalDebtBefore, liquidityFee)
+
+
+s = Solver()
+
+liquidityFee = Int('liquidityFee')
+s.add(0 <= liquidityFee, liquidityFee <= PERCENTAGE_FACTOR)
+
+drawnIndex1 = Int('drawnIndex1')
+s.add(RAY <= drawnIndex1, drawnIndex1 < 100 * RAY)
+drawnIndex2 = Int('drawnIndex2')
+s.add(drawnIndex1 <= drawnIndex2, drawnIndex2 < 100 * RAY)
+drawnIndex3 = Int('drawnIndex3')
+s.add(drawnIndex2 <= drawnIndex3, drawnIndex3 < 100 * RAY)
+
+drawnShares = Int('drawnShares')
+s.add(1 <= drawnShares, drawnShares <= MAX_SUPPLY_AMOUNT)
+premiumShares = Int('premiumShares')
+s.add(0 <= premiumShares, premiumShares <= MAX_SUPPLY_AMOUNT)
+premiumOffsetRay = premiumShares * RAY
+realizedPremiumRay = Int('realizedPremiumRay')
+s.add(0 <= realizedPremiumRay, realizedPremiumRay <= MAX_SUPPLY_AMOUNT)
+liquiditySwept = Int('liquiditySwept')
+s.add(0 <= liquiditySwept, liquiditySwept <= MAX_SUPPLY_AMOUNT)
+deficitRay = Int('deficitRay')
+s.add(0 <= deficitRay, deficitRay <= MAX_SUPPLY_AMOUNT)
+
+# T1: accrue
+feeAmount1 = unrealizedFeeAmount(
+    drawnShares,
+    RAY,
+    drawnIndex1,
+    realizedPremiumRay,
+    premiumShares,
+    premiumOffsetRay,
+    deficitRay,
+    liquidityFee,
+)
+totalAddedAssets1 = (
+    liquiditySwept
+    + totalDebt(
+        drawnShares,
+        drawnIndex1,
+        realizedPremiumRay,
+        premiumShares,
+        premiumOffsetRay,
+        deficitRay,
+    )
+    - feeAmount1
+)
+newRealizedPremiumRay = (
+    realizedPremiumRay + premiumShares * drawnIndex1 - premiumOffsetRay
+)
+newPremiumOffsetRay = premiumShares * drawnIndex1
+
+# T2: preview
+feeAmount2 = feeAmount1 + unrealizedFeeAmount(
+    drawnShares,
+    drawnIndex1,
+    drawnIndex2,
+    newRealizedPremiumRay,
+    premiumShares,
+    newPremiumOffsetRay,
+    deficitRay,
+    liquidityFee,
+)
+totalAddedAssets2 = (
+    liquiditySwept
+    + totalDebt(
+        drawnShares,
+        drawnIndex2,
+        newRealizedPremiumRay,
+        premiumShares,
+        newPremiumOffsetRay,
+        deficitRay,
+    )
+    - feeAmount2
+)
+
+# T3: preview
+feeAmount3 = feeAmount1 + unrealizedFeeAmount(
+    drawnShares,
+    drawnIndex1,
+    drawnIndex3,
+    newRealizedPremiumRay,
+    premiumShares,
+    newPremiumOffsetRay,
+    deficitRay,
+    liquidityFee,
+)
+totalAddedAssets3 = (
+    liquiditySwept
+    + totalDebt(
+        drawnShares,
+        drawnIndex3,
+        newRealizedPremiumRay,
+        premiumShares,
+        newPremiumOffsetRay,
+        deficitRay,
+    )
+    - feeAmount3
+)
+
+proveValid(
+    s,
+    'Share price does not decrease from T1 to T2',
+    totalAddedAssets2 >= totalAddedAssets1,
+)
+
+proveValid(
+    s,
+    'Share price does not decrease from T2 to T3',
+    totalAddedAssets3 >= totalAddedAssets2,
+)
diff --git a/tests/misc/z3/supply_share_price_repay.py b/tests/misc/z3/supply_share_price_repay.py
new file mode 100644
index 000000000..55e86b9d2
--- /dev/null
+++ b/tests/misc/z3/supply_share_price_repay.py
@@ -0,0 +1,19 @@
+# Highlights the fact that the supply share price does not decrease after a repay operation.
+from commons import *
+
+s = Solver()
+
+premiumRayBefore = Int('premiumRayBefore')
+s.add(0 <= premiumRayBefore, premiumRayBefore <= MAX_SUPPLY_AMOUNT)
+premiumRestoredRay = Int('premiumRestoredRay')
+s.add(0 <= premiumRestoredRay, premiumRestoredRay <= premiumRayBefore)
+
+premiumRayAfter = premiumRayBefore - premiumRestoredRay
+liquidityIncrease = divUp(premiumRestoredRay, RAY)
+actualPremiumDebtDecrease = divUp(premiumRayBefore, RAY) - divUp(premiumRayAfter, RAY)
+
+proveValid(
+    s,
+    'Share price does not decrease after repay',
+    liquidityIncrease >= actualPremiumDebtDecrease,
+)
diff --git a/uv.lock b/uv.lock
new file mode 100644
index 000000000..13b94960a
--- /dev/null
+++ b/uv.lock
@@ -0,0 +1,60 @@
+version = 1
+revision = 3
+requires-python = ">=3.13"
+
+[[package]]
+name = "aave-v4"
+version = "0.1.0"
+source = { virtual = "." }
+dependencies = [
+    { name = "z3-solver" },
+]
+
+[package.dev-dependencies]
+dev = [
+    { name = "ruff" },
+]
+
+[package.metadata]
+requires-dist = [{ name = "z3-solver", specifier = ">=4.15.7.0" }]
+
+[package.metadata.requires-dev]
+dev = [{ name = "ruff", specifier = ">=0.15.0" }]
+
+[[package]]
+name = "ruff"
+version = "0.15.0"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/c8/39/5cee96809fbca590abea6b46c6d1c586b49663d1d2830a751cc8fc42c666/ruff-0.15.0.tar.gz", hash = "sha256:6bdea47cdbea30d40f8f8d7d69c0854ba7c15420ec75a26f463290949d7f7e9a", size = 4524893, upload-time = "2026-02-03T17:53:35.357Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/bc/88/3fd1b0aa4b6330d6aaa63a285bc96c9f71970351579152d231ed90914586/ruff-0.15.0-py3-none-linux_armv6l.whl", hash = "sha256:aac4ebaa612a82b23d45964586f24ae9bc23ca101919f5590bdb368d74ad5455", size = 10354332, upload-time = "2026-02-03T17:52:54.892Z" },
+    { url = "https://files.pythonhosted.org/packages/72/f6/62e173fbb7eb75cc29fe2576a1e20f0a46f671a2587b5f604bfb0eaf5f6f/ruff-0.15.0-py3-none-macosx_10_12_x86_64.whl", hash = "sha256:dcd4be7cc75cfbbca24a98d04d0b9b36a270d0833241f776b788d59f4142b14d", size = 10767189, upload-time = "2026-02-03T17:53:19.778Z" },
+    { url = "https://files.pythonhosted.org/packages/99/e4/968ae17b676d1d2ff101d56dc69cf333e3a4c985e1ec23803df84fc7bf9e/ruff-0.15.0-py3-none-macosx_11_0_arm64.whl", hash = "sha256:d747e3319b2bce179c7c1eaad3d884dc0a199b5f4d5187620530adf9105268ce", size = 10075384, upload-time = "2026-02-03T17:53:29.241Z" },
+    { url = "https://files.pythonhosted.org/packages/a2/bf/9843c6044ab9e20af879c751487e61333ca79a2c8c3058b15722386b8cae/ruff-0.15.0-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:650bd9c56ae03102c51a5e4b554d74d825ff3abe4db22b90fd32d816c2e90621", size = 10481363, upload-time = "2026-02-03T17:52:43.332Z" },
+    { url = "https://files.pythonhosted.org/packages/55/d9/4ada5ccf4cd1f532db1c8d44b6f664f2208d3d93acbeec18f82315e15193/ruff-0.15.0-py3-none-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:a6664b7eac559e3048223a2da77769c2f92b43a6dfd4720cef42654299a599c9", size = 10187736, upload-time = "2026-02-03T17:53:00.522Z" },
+    { url = "https://files.pythonhosted.org/packages/86/e2/f25eaecd446af7bb132af0a1d5b135a62971a41f5366ff41d06d25e77a91/ruff-0.15.0-py3-none-manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:6f811f97b0f092b35320d1556f3353bf238763420ade5d9e62ebd2b73f2ff179", size = 10968415, upload-time = "2026-02-03T17:53:15.705Z" },
+    { url = "https://files.pythonhosted.org/packages/e7/dc/f06a8558d06333bf79b497d29a50c3a673d9251214e0d7ec78f90b30aa79/ruff-0.15.0-py3-none-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:761ec0a66680fab6454236635a39abaf14198818c8cdf691e036f4bc0f406b2d", size = 11809643, upload-time = "2026-02-03T17:53:23.031Z" },
+    { url = "https://files.pythonhosted.org/packages/dd/45/0ece8db2c474ad7df13af3a6d50f76e22a09d078af63078f005057ca59eb/ruff-0.15.0-py3-none-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:940f11c2604d317e797b289f4f9f3fa5555ffe4fb574b55ed006c3d9b6f0eb78", size = 11234787, upload-time = "2026-02-03T17:52:46.432Z" },
+    { url = "https://files.pythonhosted.org/packages/8a/d9/0e3a81467a120fd265658d127db648e4d3acfe3e4f6f5d4ea79fac47e587/ruff-0.15.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:bcbca3d40558789126da91d7ef9a7c87772ee107033db7191edefa34e2c7f1b4", size = 11112797, upload-time = "2026-02-03T17:52:49.274Z" },
+    { url = "https://files.pythonhosted.org/packages/b2/cb/8c0b3b0c692683f8ff31351dfb6241047fa873a4481a76df4335a8bff716/ruff-0.15.0-py3-none-manylinux_2_31_riscv64.whl", hash = "sha256:9a121a96db1d75fa3eb39c4539e607f628920dd72ff1f7c5ee4f1b768ac62d6e", size = 11033133, upload-time = "2026-02-03T17:53:33.105Z" },
+    { url = "https://files.pythonhosted.org/packages/f8/5e/23b87370cf0f9081a8c89a753e69a4e8778805b8802ccfe175cc410e50b9/ruff-0.15.0-py3-none-musllinux_1_2_aarch64.whl", hash = "sha256:5298d518e493061f2eabd4abd067c7e4fb89e2f63291c94332e35631c07c3662", size = 10442646, upload-time = "2026-02-03T17:53:06.278Z" },
+    { url = "https://files.pythonhosted.org/packages/e1/9a/3c94de5ce642830167e6d00b5c75aacd73e6347b4c7fc6828699b150a5ee/ruff-0.15.0-py3-none-musllinux_1_2_armv7l.whl", hash = "sha256:afb6e603d6375ff0d6b0cee563fa21ab570fd15e65c852cb24922cef25050cf1", size = 10195750, upload-time = "2026-02-03T17:53:26.084Z" },
+    { url = "https://files.pythonhosted.org/packages/30/15/e396325080d600b436acc970848d69df9c13977942fb62bb8722d729bee8/ruff-0.15.0-py3-none-musllinux_1_2_i686.whl", hash = "sha256:77e515f6b15f828b94dc17d2b4ace334c9ddb7d9468c54b2f9ed2b9c1593ef16", size = 10676120, upload-time = "2026-02-03T17:53:09.363Z" },
+    { url = "https://files.pythonhosted.org/packages/8d/c9/229a23d52a2983de1ad0fb0ee37d36e0257e6f28bfd6b498ee2c76361874/ruff-0.15.0-py3-none-musllinux_1_2_x86_64.whl", hash = "sha256:6f6e80850a01eb13b3e42ee0ebdf6e4497151b48c35051aab51c101266d187a3", size = 11201636, upload-time = "2026-02-03T17:52:57.281Z" },
+    { url = "https://files.pythonhosted.org/packages/6f/b0/69adf22f4e24f3677208adb715c578266842e6e6a3cc77483f48dd999ede/ruff-0.15.0-py3-none-win32.whl", hash = "sha256:238a717ef803e501b6d51e0bdd0d2c6e8513fe9eec14002445134d3907cd46c3", size = 10465945, upload-time = "2026-02-03T17:53:12.591Z" },
+    { url = "https://files.pythonhosted.org/packages/51/ad/f813b6e2c97e9b4598be25e94a9147b9af7e60523b0cb5d94d307c15229d/ruff-0.15.0-py3-none-win_amd64.whl", hash = "sha256:dd5e4d3301dc01de614da3cdffc33d4b1b96fb89e45721f1598e5532ccf78b18", size = 11564657, upload-time = "2026-02-03T17:52:51.893Z" },
+    { url = "https://files.pythonhosted.org/packages/f6/b0/2d823f6e77ebe560f4e397d078487e8d52c1516b331e3521bc75db4272ca/ruff-0.15.0-py3-none-win_arm64.whl", hash = "sha256:c480d632cc0ca3f0727acac8b7d053542d9e114a462a145d0b00e7cd658c515a", size = 10865753, upload-time = "2026-02-03T17:53:03.014Z" },
+]
+
+[[package]]
+name = "z3-solver"
+version = "4.15.7.0"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/fd/5d/810ba04f7e7f2f2e5f019dd75237d1a16b7388a0c72f7e532b27dde9f7e2/z3_solver-4.15.7.0.tar.gz", hash = "sha256:a26b91f861b6d13bb76f0ac568d3ef1c0a4801e70a135f80e66b49628565a460", size = 5071448, upload-time = "2026-02-09T01:08:40.767Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/a7/1b/d21f292b473c1c40bedf41d113577ae2bb7fcc715f54d42c10b7f2b3a186/z3_solver-4.15.7.0-py3-none-macosx_15_0_arm64.whl", hash = "sha256:a6c967677c67296a8b7c97dff68107f029c576a94cfb4abc9e08bf72e5499e5d", size = 36987369, upload-time = "2026-02-09T01:08:27.585Z" },
+    { url = "https://files.pythonhosted.org/packages/77/36/132c3d03de2eed160fad123207c981507193b2621e05b2909563775e0ad9/z3_solver-4.15.7.0-py3-none-macosx_15_0_x86_64.whl", hash = "sha256:a9644e958252dfdbdae2f787a8192fe4b8c156e7cf7b0e00a6a59e896a27569d", size = 47560235, upload-time = "2026-02-09T01:08:30.415Z" },
+    { url = "https://files.pythonhosted.org/packages/61/49/40b0ee7cd2425dfa05bde5776f6aa7e892460a5ca8016171204f9b2d42df/z3_solver-4.15.7.0-py3-none-win32.whl", hash = "sha256:2dd09ac8afde63035d9c0a63b23d448726e374ec588b67b5f5edce9d7e9b1a13", size = 13342998, upload-time = "2026-02-09T01:08:33.84Z" },
+    { url = "https://files.pythonhosted.org/packages/6c/ab/5a60c6ed712eb97749cd758162842cec771cfbe2c37ea43a251dc6fe583b/z3_solver-4.15.7.0-py3-none-win_amd64.whl", hash = "sha256:17f5ccea921d6a11bba5880281048c9f4a1e0c35f76e8ce69e72826c90c230bd", size = 16427563, upload-time = "2026-02-09T01:08:35.884Z" },
+    { url = "https://files.pythonhosted.org/packages/f0/1f/ea28f6b3dec9cbab32cf851b3a529c9fb8332300c7419a55ab68ef5b40ac/z3_solver-4.15.7.0-py3-none-win_arm64.whl", hash = "sha256:9bf1a350598bc92ece90220073fe47c0b0f8cbbeaaf62974de736bd79947f8bd", size = 15082309, upload-time = "2026-02-09T01:08:38.832Z" },
+]