diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec
index 35927c5d3..81b6d3604 100644
--- a/certora/specs/AccessControl.spec
+++ b/certora/specs/AccessControl.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IAccessControl.spec"
 
 /*
diff --git a/certora/specs/DoubleEndedQueue.spec b/certora/specs/DoubleEndedQueue.spec
index 2412b4cc8..2a196772d 100644
--- a/certora/specs/DoubleEndedQueue.spec
+++ b/certora/specs/DoubleEndedQueue.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     pushFront(bytes32)                    envfree
@@ -10,7 +10,7 @@ methods {
     // exposed for FV
     begin()             returns (int128)  envfree
     end()               returns (int128)  envfree
-    
+
     // view
     length()            returns (uint256) envfree
     empty()             returns (bool)    envfree
@@ -35,7 +35,7 @@ function max_int128() returns mathint {
 
 // Could be broken in theory, but not in practice
 function boundedQueue() returns bool {
-    return 
+    return
         max_int128() > to_mathint(end()) &&
         min_int128() < to_mathint(begin());
 }
@@ -78,11 +78,11 @@ invariant emptiness()
 invariant queueEndings()
     at_(length() - 1) == back() && at_(0) == front()
     filtered { f -> !f.isView }
-    { 
-        preserved { 
-            requireInvariant boundariesConsistency(); 
-            require boundedQueue(); 
-        } 
+    {
+        preserved {
+            requireInvariant boundariesConsistency();
+            require boundedQueue();
+        }
     }
 
 /*
@@ -94,12 +94,12 @@ rule pushFront(bytes32 value) {
     require boundedQueue();
 
     uint256 lengthBefore = length();
-    
+
     pushFront@withrevert(value);
-    
+
     // liveness
     assert !lastReverted, "never reverts";
-    
+
     // effect
     assert front() == value, "front set to value";
     assert length() == lengthBefore + 1, "queue extended";
@@ -134,12 +134,12 @@ rule pushBack(bytes32 value) {
     require boundedQueue();
 
     uint256 lengthBefore = length();
-    
+
     pushBack@withrevert(value);
-    
+
     // liveness
     assert !lastReverted, "never reverts";
-    
+
     // effect
     assert back() == value, "back set to value";
     assert length() == lengthBefore + 1, "queue increased";
@@ -205,7 +205,7 @@ rule popFrontConsistency(uint256 index) {
 
     // try to read value
     bytes32 after = at_@withrevert(index - 1);
-    
+
     assert !lastReverted, "value still exists in the queue";
     assert before == after, "values are offset and not modified";
 }
@@ -250,7 +250,7 @@ rule popBackConsistency(uint256 index) {
 
     // try to read value
     bytes32 after = at_@withrevert(index);
-    
+
     assert !lastReverted, "value still exists in the queue";
     assert before == after, "values are offset and not modified";
 }
@@ -262,10 +262,10 @@ rule popBackConsistency(uint256 index) {
 */
 rule clear {
     clear@withrevert();
-    
+
     // liveness
     assert !lastReverted, "never reverts";
-    
+
     // effect
     assert length() == 0, "sets length to 0";
 }
diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec
index 85f95e706..3bd2b38ba 100644
--- a/certora/specs/ERC20.spec
+++ b/certora/specs/ERC20.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IERC20.spec"
 import "methods/IERC2612.spec"
 
diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec
index 64d97342a..70a7c0795 100644
--- a/certora/specs/ERC20FlashMint.spec
+++ b/certora/specs/ERC20FlashMint.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IERC20.spec"
 import "methods/IERC3156.spec"
 
diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec
index c10173766..badfa7a28 100644
--- a/certora/specs/ERC20Wrapper.spec
+++ b/certora/specs/ERC20Wrapper.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "ERC20.spec"
 
 methods {
diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec
index 48503469b..9db13f45c 100644
--- a/certora/specs/ERC721.spec
+++ b/certora/specs/ERC721.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IERC721.spec"
 
 methods {
diff --git a/certora/specs/EnumerableMap.spec b/certora/specs/EnumerableMap.spec
index 56ef854c6..dea5d85ec 100644
--- a/certora/specs/EnumerableMap.spec
+++ b/certora/specs/EnumerableMap.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     // library
diff --git a/certora/specs/EnumerableSet.spec b/certora/specs/EnumerableSet.spec
index c94ba2437..d63c556aa 100644
--- a/certora/specs/EnumerableSet.spec
+++ b/certora/specs/EnumerableSet.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     // library
diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec
index 1ba8d54e8..0e0b1b714 100644
--- a/certora/specs/Initializable.spec
+++ b/certora/specs/Initializable.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     // initialize, reinitialize, disable
diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec
index 4fdfeb09c..4bf9e3005 100644
--- a/certora/specs/Ownable.spec
+++ b/certora/specs/Ownable.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IOwnable.spec"
 
 methods {
diff --git a/certora/specs/Ownable2Step.spec b/certora/specs/Ownable2Step.spec
index 70c520a03..47b1b8d75 100644
--- a/certora/specs/Ownable2Step.spec
+++ b/certora/specs/Ownable2Step.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IOwnable2Step.spec"
 
 methods {
diff --git a/certora/specs/Pausable.spec b/certora/specs/Pausable.spec
index e49293ffc..aea38003f 100644
--- a/certora/specs/Pausable.spec
+++ b/certora/specs/Pausable.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     paused() returns (bool) envfree
@@ -22,7 +22,7 @@ rule pause(env e) {
     bool success = !lastReverted;
 
     bool pausedAfter = paused();
-    
+
     // liveness
     assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
 
@@ -44,7 +44,7 @@ rule unpause(env e) {
     bool success = !lastReverted;
 
     bool pausedAfter = paused();
-    
+
     // liveness
     assert success <=> pausedBefore, "works if and only if the contract was paused before";
 
@@ -71,7 +71,7 @@ rule whenPaused(env e) {
 */
 rule whenNotPaused(env e) {
     require nonpayable(e);
-    
+
     onlyWhenNotPaused@withrevert(e);
     assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
 }
diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec
index e140c11de..05ecb1340 100644
--- a/certora/specs/TimelockController.spec
+++ b/certora/specs/TimelockController.spec
@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IAccessControl.spec"
 
 methods {
diff --git a/certora/specs/helpers.spec b/certora/specs/helpers/helpers.spec
similarity index 100%
rename from certora/specs/helpers.spec
rename to certora/specs/helpers/helpers.spec