diff --git a/.github/workflows/certora-gho.yml b/.github/workflows/certora-gho.yml
index 419b95d7..0e267505 100644
--- a/.github/workflows/certora-gho.yml
+++ b/.github/workflows/certora-gho.yml
@@ -52,7 +52,7 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyGhoToken.conf --rule length_leq_max_uint160 inv_balanceOf_leq_totalSupply total_supply_eq_sumAllLevel sumAllBalance_eq_totalSupply sumAllLevel_eq_sumAllBalance inv_valid_capacity inv_valid_level address_in_set_values_iff_in_set_indexes addr_in_set_iff_in_map addr_in_set_list_iff_in_map level_leq_capacity mint_after_burn burn_after_mint level_unchanged_after_mint_followed_by_burn level_after_mint level_after_burn facilitator_in_list_after_setFacilitatorBucketCapacity getFacilitatorBucketCapacity_after_setFacilitatorBucketCapacity facilitator_in_list_after_addFacilitator facilitator_in_list_after_mint_and_burn address_not_in_list_after_removeFacilitator balance_after_mint balance_after_burn mintLimitedByFacilitatorRemainingCapacity burnLimitedByFacilitatorLevel ARRAY_IS_INVERSE_OF_MAP_Invariant addressSetInvariant address_not_in_list_after_removeFacilitator_CASE_SPLIT_zero_address
+          - verifyGhoToken.conf 
           - verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
           - verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
           - verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
diff --git a/.github/workflows/certora-upgradeable-gho-token.yml b/.github/workflows/certora-upgradeable-gho-token.yml
new file mode 100644
index 00000000..5e9695e1
--- /dev/null
+++ b/.github/workflows/certora-upgradeable-gho-token.yml
@@ -0,0 +1,55 @@
+name: certora-upgradeable-gho-token
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: '11', java-package: jre }
+
+      - name: Install certora cli
+        run: pip install certora-cli==4.13.1
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.10
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          cd certora/gho
+          touch applyHarness.patch
+          make munged
+          cd ../..
+          echo "key length" ${#CERTORAKEY}
+          certoraRun certora/gho/conf/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyUpgradeableGhoToken.conf
diff --git a/certora/gho/applyHarness.patch b/certora/gho/applyHarness.patch
index 18b6fef3..61551884 100644
--- a/certora/gho/applyHarness.patch
+++ b/certora/gho/applyHarness.patch
@@ -1,13 +1,7 @@
-diff -ruN ../src/.gitignore .gitignore
---- ../src/.gitignore	1970-01-01 02:00:00.000000000 +0200
-+++ .gitignore	2023-02-26 11:58:05.000000000 +0200
-@@ -0,0 +1,2 @@
-+*
-+!.gitignore
-diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
---- ../src/contracts/gho/GhoToken.sol	2023-02-26 10:23:14.000000000 +0200
-+++ contracts/gho/GhoToken.sol	2023-02-26 13:26:13.000000000 +0200
-@@ -74,11 +74,16 @@
+diff -ruN ../../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
+--- ../../src/contracts/gho/GhoToken.sol	2024-05-21 10:57:52.000000000 +0300
++++ contracts/gho/GhoToken.sol	2024-05-27 12:55:24.588859419 +0300
+@@ -66,11 +66,16 @@
      uint128 bucketCapacity
    ) external onlyRole(FACILITATOR_MANAGER_ROLE) {
      Facilitator storage facilitator = _facilitators[facilitatorAddress];
@@ -24,9 +18,9 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
  
      _facilitatorsList.add(facilitatorAddress);
  
-@@ -92,6 +97,10 @@
-   /// @inheritdoc IGhoToken
-   function removeFacilitator(address facilitatorAddress) external onlyRole(FACILITATOR_MANAGER_ROLE) {
+@@ -86,6 +91,10 @@
+     address facilitatorAddress
+   ) external onlyRole(FACILITATOR_MANAGER_ROLE) {
      require(
 +      _facilitators[facilitatorAddress].isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
 +      'FACILITATOR_DOES_NOT_EXIST'
@@ -35,7 +29,7 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
        bytes(_facilitators[facilitatorAddress].label).length > 0,
        'FACILITATOR_DOES_NOT_EXIST'
      );
-@@ -111,6 +120,10 @@
+@@ -105,6 +114,10 @@
      address facilitator,
      uint128 newCapacity
    ) external onlyRole(BUCKET_MANAGER_ROLE) {
@@ -46,7 +40,7 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
      require(bytes(_facilitators[facilitator].label).length > 0, 'FACILITATOR_DOES_NOT_EXIST');
  
      uint256 oldCapacity = _facilitators[facilitator].bucketCapacity;
-@@ -125,12 +138,12 @@
+@@ -119,12 +132,12 @@
    }
  
    /// @inheritdoc IGhoToken
@@ -61,10 +55,10 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
      return _facilitatorsList.values();
    }
  }
-diff -ruN ../src/contracts/gho/interfaces/IGhoToken.sol contracts/gho/interfaces/IGhoToken.sol
---- ../src/contracts/gho/interfaces/IGhoToken.sol	2023-02-26 10:23:14.000000000 +0200
-+++ contracts/gho/interfaces/IGhoToken.sol	2023-02-26 11:58:05.000000000 +0200
-@@ -14,6 +14,7 @@
+diff -ruN ../../src/contracts/gho/interfaces/IGhoToken.sol contracts/gho/interfaces/IGhoToken.sol
+--- ../../src/contracts/gho/interfaces/IGhoToken.sol	2024-05-21 10:57:52.000000000 +0300
++++ contracts/gho/interfaces/IGhoToken.sol	2024-05-27 12:55:24.588859419 +0300
+@@ -13,6 +13,7 @@
      uint128 bucketCapacity;
      uint128 bucketLevel;
      string label;
@@ -72,3 +66,66 @@ diff -ruN ../src/contracts/gho/interfaces/IGhoToken.sol contracts/gho/interfaces
    }
  
    /**
+diff -ruN ../../src/contracts/gho/UpgradeableGhoToken.sol contracts/gho/UpgradeableGhoToken.sol
+--- ../../src/contracts/gho/UpgradeableGhoToken.sol	2024-05-21 11:57:23.000000000 +0300
++++ contracts/gho/UpgradeableGhoToken.sol	2024-05-27 15:04:16.458997293 +0300
+@@ -76,11 +76,16 @@
+     uint128 bucketCapacity
+   ) external onlyRole(FACILITATOR_MANAGER_ROLE) {
+     Facilitator storage facilitator = _facilitators[facilitatorAddress];
++    require(
++      !facilitator.isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
++      'FACILITATOR_ALREADY_EXISTS'
++    );
+     require(bytes(facilitator.label).length == 0, 'FACILITATOR_ALREADY_EXISTS');
+     require(bytes(facilitatorLabel).length > 0, 'INVALID_LABEL');
+ 
+     facilitator.label = facilitatorLabel;
+     facilitator.bucketCapacity = bucketCapacity;
++    facilitator.isLabelNonempty = true;
+ 
+     _facilitatorsList.add(facilitatorAddress);
+ 
+@@ -96,6 +101,10 @@
+     address facilitatorAddress
+   ) external onlyRole(FACILITATOR_MANAGER_ROLE) {
+     require(
++      _facilitators[facilitatorAddress].isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
++      'FACILITATOR_DOES_NOT_EXIST'
++    );
++    require(
+       bytes(_facilitators[facilitatorAddress].label).length > 0,
+       'FACILITATOR_DOES_NOT_EXIST'
+     );
+@@ -115,6 +124,10 @@
+     address facilitator,
+     uint128 newCapacity
+   ) external onlyRole(BUCKET_MANAGER_ROLE) {
++    require(
++      _facilitators[facilitator].isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
++      'FACILITATOR_DOES_NOT_EXIST'
++    );
+     require(bytes(_facilitators[facilitator].label).length > 0, 'FACILITATOR_DOES_NOT_EXIST');
+ 
+     uint256 oldCapacity = _facilitators[facilitator].bucketCapacity;
+@@ -129,12 +142,12 @@
+   }
+ 
+   /// @inheritdoc IGhoToken
+-  function getFacilitatorBucket(address facilitator) external view returns (uint256, uint256) {
++  function getFacilitatorBucket(address facilitator) public view returns (uint256, uint256) {
+     return (_facilitators[facilitator].bucketCapacity, _facilitators[facilitator].bucketLevel);
+   }
+ 
+   /// @inheritdoc IGhoToken
+-  function getFacilitatorsList() external view returns (address[] memory) {
++  function getFacilitatorsList() public view returns (address[] memory) {
+     return _facilitatorsList.values();
+   }
+ 
+diff -ruN ../../src/.gitignore .gitignore
+--- ../../src/.gitignore	1970-01-01 02:00:00.000000000 +0200
++++ .gitignore	2024-05-27 12:55:24.588859419 +0300
+@@ -0,0 +1,2 @@
++*
++!.gitignore
diff --git a/certora/gho/conf/verifyGhoToken.conf b/certora/gho/conf/verifyGhoToken.conf
index a99d2fb7..97a4e53d 100644
--- a/certora/gho/conf/verifyGhoToken.conf
+++ b/certora/gho/conf/verifyGhoToken.conf
@@ -1,7 +1,7 @@
 {
     "files": [
         "certora/gho/harness/GhoTokenHarness.sol:GhoTokenHarness",
-        "certora/gho/munged/contracts/gho/GhoToken.sol"
+//        "certora/gho/munged/contracts/gho/GhoToken.sol"
     ],
     "packages": [
         "@aave/core-v3/=lib/aave-v3-core",
diff --git a/certora/gho/conf/verifyUpgradeableGhoToken.conf b/certora/gho/conf/verifyUpgradeableGhoToken.conf
new file mode 100644
index 00000000..a5fb9de1
--- /dev/null
+++ b/certora/gho/conf/verifyUpgradeableGhoToken.conf
@@ -0,0 +1,18 @@
+{
+    "files": [
+        "certora/gho/harness/UpgradeableGhoTokenHarness.sol:UpgradeableGhoTokenHarness",
+//        "certora/gho/munged/contracts/gho/GhoToken.sol"
+    ],
+    "packages": [
+        "@aave/core-v3/=lib/aave-v3-core",
+        "@aave/periphery-v3/=lib/aave-v3-periphery",
+        "@aave/=lib/aave-token",
+        "@openzeppelin/=lib/openzeppelin-contracts",
+    ],
+    "loop_iter": "3",
+    "msg": "GhoToken, all rules.",
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "UpgradeableGhoTokenHarness:certora/gho/specs/ghoToken.spec"
+}
\ No newline at end of file
diff --git a/certora/gho/harness/UpgradeableGhoTokenHarness.sol b/certora/gho/harness/UpgradeableGhoTokenHarness.sol
new file mode 100644
index 00000000..f6937faa
--- /dev/null
+++ b/certora/gho/harness/UpgradeableGhoTokenHarness.sol
@@ -0,0 +1,84 @@
+pragma solidity ^0.8.0;
+
+import {IGhoToken} from '../munged/contracts/gho/interfaces/IGhoToken.sol';
+import '@openzeppelin/contracts/utils/structs/EnumerableSet.sol';
+import {UpgradeableGhoToken} from '../munged/contracts/gho/UpgradeableGhoToken.sol';
+
+contract UpgradeableGhoTokenHarness is UpgradeableGhoToken {
+  using EnumerableSet for EnumerableSet.AddressSet;
+
+  constructor() UpgradeableGhoToken() {}
+
+  /**
+   * @notice Returns the bucket capacity
+   * @param facilitator The address of the facilitator
+   * @return The facilitator bucket capacity
+   */
+  function getFacilitatorBucketCapacity(address facilitator) public view returns (uint256) {
+    (uint256 bucketCapacity, ) = getFacilitatorBucket(facilitator);
+    return bucketCapacity;
+  }
+
+  /**
+   * @notice Returns the bucket level
+   * @param facilitator The address of the facilitator
+   * @return The facilitator bucket level
+   */
+  function getFacilitatorBucketLevel(address facilitator) public view returns (uint256) {
+    (, uint256 bucketLevel) = getFacilitatorBucket(facilitator);
+    return bucketLevel;
+  }
+
+  /**
+   * @notice Returns the length of the facilitator list
+   * @return The length of the facilitator list
+   */
+  function getFacilitatorsListLen() external view returns (uint256) {
+    address[] memory flist = getFacilitatorsList();
+    return flist.length;
+  }
+
+  /**
+   * @notice Indicator of GhoToken mapping
+   * @param addr An address of a facilitator
+   * @return True of facilitator is in GhoToken mapping
+   */
+  function is_in_facilitator_mapping(address addr) external view returns (bool) {
+    Facilitator memory facilitator = _facilitators[addr];
+    return facilitator.isLabelNonempty; //TODO: remove workaround when CERT-977 is resolved
+    //  return (bytes(facilitator.label).length > 0);
+  }
+
+  /**
+   * @notice Indicator of AddressSet mapping
+   * @param addr An address of a facilitator
+   * @return True of facilitator is in AddressSet mapping
+   */
+  function is_in_facilitator_set_map(address addr) external view returns (bool) {
+    return _facilitatorsList.contains(addr);
+  }
+
+  /**
+   * @notice Indicator of AddressSet list
+   * @param addr An address of a facilitator
+   * @return True of facilitator is in AddressSet array
+   */
+  function is_in_facilitator_set_array(address addr) external view returns (bool) {
+    address[] memory flist = getFacilitatorsList();
+    for (uint256 i = 0; i < flist.length; ++i) {
+      if (address(flist[i]) == addr) {
+        return true;
+      }
+    }
+    return false;
+  }
+
+  /**
+   * @notice Converts address to bytes32
+   * @param value Some address
+   * @return b the value as bytes32
+   */
+  function to_bytes32(address value) external pure returns (bytes32 b) {
+    b = bytes32(uint256(uint160(value)));
+  }
+}
diff --git a/certora/gho/specs/ghoToken.spec b/certora/gho/specs/ghoToken.spec
index 2f427bca..322f0799 100644
--- a/certora/gho/specs/ghoToken.spec
+++ b/certora/gho/specs/ghoToken.spec
@@ -1,6 +1,5 @@
 import "set.spec";
 
-using GhoToken as GHOTOKEN;
 methods{
 	function mint(address,uint256) external;
 	function burn(uint256) external;
@@ -15,7 +14,6 @@ methods{
 	function is_in_facilitator_mapping(address) external returns bool envfree;
 	function is_in_facilitator_set_map(address) external returns bool envfree;
 	function is_in_facilitator_set_array(address) external returns bool envfree;
-	//function to_bytes32(address) external returns (bytes32) envfree;
 }
 
 ghost sumAllBalance() returns mathint {