diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
index 9b8eb83b..028b1ceb 100644
--- a/.github/workflows/certora-gsm.yml
+++ b/.github/workflows/certora-gsm.yml
@@ -38,11 +38,11 @@ jobs:
           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: Install node dependencies
         run: |
           npm i
-      
+
       - name: Verify rule ${{ matrix.rule }}
         run: |
           echo "key length" ${#CERTORAKEY}
@@ -69,4 +69,3 @@ jobs:
           - non-4626/otakar-getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
           - non-4626/otakar-finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
           - non-4626/otakar-OracleSwapFreezer.conf
-          
diff --git a/README.md b/README.md
index 64bbe1dd..0dc83f4f 100644
--- a/README.md
+++ b/README.md
@@ -45,6 +45,7 @@ You can find all audit reports under the [audits](./audits/) folder
 - [2023-06-13 - Sigma Prime (GhoSteward)](./audits/2023-06-13_GhoSteward_SigmaPrime.pdf)
 - [2023-09-20 - Emanuele Ricci @Stermi (GHO Stability Module)](./audits/2023-09-20_GSM_Stermi.pdf)
 - [2023-10-23 - Sigma Prime (GHO Stability Module)](./audits/2023-10-23_GSM_SigmaPrime.pdf)
+- [2023-12-07 - Certora Formal Verification (GHO Stability Module)](./certora/reports/Formal_Verification_Report_of_GHO_Stability_Module.pdf)
 
 ## Getting Started
 
diff --git a/certora/GSM/harness/OracleSwapFreezerHarness.sol b/certora/GSM/harness/OracleSwapFreezerHarness.sol
index f0bee2f1..6a4de982 100644
--- a/certora/GSM/harness/OracleSwapFreezerHarness.sol
+++ b/certora/GSM/harness/OracleSwapFreezerHarness.sol
@@ -78,7 +78,7 @@ contract OracleSwapFreezerHarness is OracleSwapFreezer {
     return IPriceOracle(ADDRESS_PROVIDER.getPriceOracle()).getAssetPrice(UNDERLYING_ASSET);
   }
 
-  function hasRole() external view returns(bool) {
+  function hasRole() external view returns (bool) {
     return GSM.hasRole(GSM.SWAP_FREEZER_ROLE(), address(this));
   }
 }