diff --git a/.changeset/strong-poems-thank.md b/.changeset/strong-poems-thank.md
new file mode 100644
index 00000000000..5f496de7f68
--- /dev/null
+++ b/.changeset/strong-poems-thank.md
@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': major
+---
+
+`DoubleEndedQueue`: refactor internal structure to use `uint128` instead of `int128`. This has no effect on the library interface.
diff --git a/certora/harnesses/DoubleEndedQueueHarness.sol b/certora/harnesses/DoubleEndedQueueHarness.sol
index 35dd4a54aa5..c6a800726c7 100644
--- a/certora/harnesses/DoubleEndedQueueHarness.sol
+++ b/certora/harnesses/DoubleEndedQueueHarness.sol
@@ -29,11 +29,11 @@ contract DoubleEndedQueueHarness {
         _deque.clear();
     }
 
-    function begin() external view returns (int128) {
+    function begin() external view returns (uint128) {
         return _deque._begin;
     }
 
-    function end() external view returns (int128) {
+    function end() external view returns (uint128) {
         return _deque._end;
     }
 
diff --git a/certora/run.js b/certora/run.js
index fdee42d2ed4..68f34aab27c 100755
--- a/certora/run.js
+++ b/certora/run.js
@@ -28,6 +28,11 @@ const argv = require('yargs')
       type: 'number',
       default: 4,
     },
+    verbose: {
+      alias: 'v',
+      type: 'count',
+      default: 0,
+    },
     options: {
       alias: 'o',
       type: 'array',
@@ -65,6 +70,9 @@ for (const { spec, contract, files, options = [] } of specs) {
 // Run certora, aggregate the output and print it at the end
 async function runCertora(spec, contract, files, options = []) {
   const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
+  if (argv.verbose) {
+    console.log('Running:', args.join(' '));
+  }
   const child = proc.spawn('certoraRun', args);
 
   const stream = new PassThrough();
diff --git a/certora/specs/DoubleEndedQueue.spec b/certora/specs/DoubleEndedQueue.spec
index 2a196772d5a..3b71bb4c7a8 100644
--- a/certora/specs/DoubleEndedQueue.spec
+++ b/certora/specs/DoubleEndedQueue.spec
@@ -1,64 +1,25 @@
-import "helpers/helpers.spec"
+import "helpers/helpers.spec";
 
 methods {
-    pushFront(bytes32)                    envfree
-    pushBack(bytes32)                     envfree
-    popFront()          returns (bytes32) envfree
-    popBack()           returns (bytes32) envfree
-    clear()                               envfree
+    function pushFront(bytes32) external                   envfree;
+    function pushBack(bytes32)                    external envfree;
+    function popFront()         external returns (bytes32) envfree;
+    function popBack()          external returns (bytes32) envfree;
+    function clear()            external                   envfree;
 
     // exposed for FV
-    begin()             returns (int128)  envfree
-    end()               returns (int128)  envfree
+    function begin()            external returns (uint128) envfree;
+    function end()              external returns (uint128) envfree;
 
     // view
-    length()            returns (uint256) envfree
-    empty()             returns (bool)    envfree
-    front()             returns (bytes32) envfree
-    back()              returns (bytes32) envfree
-    at_(uint256)        returns (bytes32) envfree // at is a reserved word
+    function length()           external returns (uint256) envfree;
+    function empty()            external returns (bool)    envfree;
+    function front()            external returns (bytes32) envfree;
+    function back()             external returns (bytes32) envfree;
+    function at_(uint256)       external returns (bytes32) envfree; // at is a reserved word
 }
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Helpers                                                                                                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-
-function min_int128() returns mathint {
-    return -(1 << 127);
-}
-
-function max_int128() returns mathint {
-    return (1 << 127) - 1;
-}
-
-// Could be broken in theory, but not in practice
-function boundedQueue() returns bool {
-    return
-        max_int128() > to_mathint(end()) &&
-        min_int128() < to_mathint(begin());
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: end is larger or equal than begin                                                                        │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant boundariesConsistency()
-    end() >= begin()
-    filtered { f -> !f.isView }
-    { preserved { require boundedQueue(); } }
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: length is end minus begin                                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-invariant lengthConsistency()
-    length() == to_mathint(end()) - to_mathint(begin())
-    filtered { f -> !f.isView }
-    { preserved { require boundedQueue(); } }
+definition full() returns bool = length() == max_uint128;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -68,22 +29,19 @@ invariant lengthConsistency()
 invariant emptiness()
     empty() <=> length() == 0
     filtered { f -> !f.isView }
-    { preserved { require boundedQueue(); } }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: front points to the first index and back points to the last one                                          │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant queueEndings()
-    at_(length() - 1) == back() && at_(0) == front()
+invariant queueFront()
+    at_(0) == front()
+    filtered { f -> !f.isView }
+
+invariant queueBack()
+    at_(require_uint256(length() - 1)) == back()
     filtered { f -> !f.isView }
-    {
-        preserved {
-            requireInvariant boundariesConsistency();
-            require boundedQueue();
-        }
-    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -91,18 +49,18 @@ invariant queueEndings()
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule pushFront(bytes32 value) {
-    require boundedQueue();
-
     uint256 lengthBefore = length();
+    bool    fullBefore   = full();
 
     pushFront@withrevert(value);
+    bool success = !lastReverted;
 
     // liveness
-    assert !lastReverted, "never reverts";
+    assert success <=> !fullBefore, "never revert if not previously full";
 
     // effect
-    assert front() == value, "front set to value";
-    assert length() == lengthBefore + 1, "queue extended";
+    assert success => front() == value, "front set to value";
+    assert success => to_mathint(length()) == lengthBefore + 1, "queue extended";
 }
 
 /*
@@ -111,15 +69,13 @@ rule pushFront(bytes32 value) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule pushFrontConsistency(uint256 index) {
-    require boundedQueue();
-
     bytes32 beforeAt = at_(index);
 
     bytes32 value;
     pushFront(value);
 
     // try to read value
-    bytes32 afterAt = at_@withrevert(index + 1);
+    bytes32 afterAt = at_@withrevert(require_uint256(index + 1));
 
     assert !lastReverted, "value still there";
     assert afterAt == beforeAt, "data is preserved";
@@ -131,18 +87,18 @@ rule pushFrontConsistency(uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule pushBack(bytes32 value) {
-    require boundedQueue();
-
     uint256 lengthBefore = length();
+    bool    fullBefore   = full();
 
     pushBack@withrevert(value);
+    bool success = !lastReverted;
 
     // liveness
-    assert !lastReverted, "never reverts";
+    assert success <=> !fullBefore, "never revert if not previously full";
 
     // effect
-    assert back() == value, "back set to value";
-    assert length() == lengthBefore + 1, "queue increased";
+    assert success => back() == value, "back set to value";
+    assert success => to_mathint(length()) == lengthBefore + 1, "queue increased";
 }
 
 /*
@@ -151,8 +107,6 @@ rule pushBack(bytes32 value) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule pushBackConsistency(uint256 index) {
-    require boundedQueue();
-
     bytes32 beforeAt = at_(index);
 
     bytes32 value;
@@ -171,9 +125,6 @@ rule pushBackConsistency(uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule popFront {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     uint256 lengthBefore = length();
     bytes32 frontBefore = front@withrevert();
 
@@ -185,7 +136,7 @@ rule popFront {
 
     // effect
     assert success => frontBefore == popped, "previous front is returned";
-    assert success => length() == lengthBefore - 1, "queue decreased";
+    assert success => to_mathint(length()) == lengthBefore - 1, "queue decreased";
 }
 
 /*
@@ -194,9 +145,6 @@ rule popFront {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule popFrontConsistency(uint256 index) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     // Read (any) value that is not the front (this asserts the value exists / the queue is long enough)
     require index > 1;
     bytes32 before = at_(index);
@@ -204,7 +152,7 @@ rule popFrontConsistency(uint256 index) {
     popFront();
 
     // try to read value
-    bytes32 after = at_@withrevert(index - 1);
+    bytes32 after = at_@withrevert(require_uint256(index - 1));
 
     assert !lastReverted, "value still exists in the queue";
     assert before == after, "values are offset and not modified";
@@ -216,9 +164,6 @@ rule popFrontConsistency(uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule popBack {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     uint256 lengthBefore = length();
     bytes32 backBefore = back@withrevert();
 
@@ -230,7 +175,7 @@ rule popBack {
 
     // effect
     assert success => backBefore == popped, "previous back is returned";
-    assert success => length() == lengthBefore - 1, "queue decreased";
+    assert success => to_mathint(length()) == lengthBefore - 1, "queue decreased";
 }
 
 /*
@@ -239,11 +184,8 @@ rule popBack {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule popBackConsistency(uint256 index) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     // Read (any) value that is not the back (this asserts the value exists / the queue is long enough)
-    require index < length() - 1;
+    require to_mathint(index) < length() - 1;
     bytes32 before = at_(index);
 
     popBack();
@@ -275,24 +217,25 @@ rule clear {
 │ Rule: front/back access reverts only if the queue is empty or querying out of bounds                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-rule onlyEmptyRevert(env e) {
+rule onlyEmptyOrFullRevert(env e) {
     require nonpayable(e);
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
 
     method f;
     calldataarg args;
 
     bool emptyBefore = empty();
+    bool fullBefore = full();
 
     f@withrevert(e, args);
 
     assert lastReverted => (
-        (f.selector == front().selector && emptyBefore) ||
-        (f.selector == back().selector && emptyBefore) ||
-        (f.selector == popFront().selector  && emptyBefore) ||
-        (f.selector == popBack().selector  && emptyBefore) ||
-        f.selector == at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
+        (f.selector == sig:front().selector            && emptyBefore) ||
+        (f.selector == sig:back().selector             && emptyBefore) ||
+        (f.selector == sig:popFront().selector         && emptyBefore) ||
+        (f.selector == sig:popBack().selector          && emptyBefore) ||
+        (f.selector == sig:pushFront(bytes32).selector && fullBefore ) ||
+        (f.selector == sig:pushBack(bytes32).selector  && fullBefore ) ||
+        f.selector == sig:at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert
     ), "only revert if empty or out of bounds";
 }
 
@@ -302,9 +245,6 @@ rule onlyEmptyRevert(env e) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule onlyOutOfBoundsRevert(uint256 index) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     at_@withrevert(index);
 
     assert lastReverted <=> index >= length(), "only reverts if index is out of bounds";
@@ -316,9 +256,6 @@ rule onlyOutOfBoundsRevert(uint256 index) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule noLengthChange(env e) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     method f;
     calldataarg args;
 
@@ -327,11 +264,11 @@ rule noLengthChange(env e) {
     uint256 lengthAfter = length();
 
     assert lengthAfter != lengthBefore => (
-        (f.selector == pushFront(bytes32).selector && lengthAfter == lengthBefore + 1) ||
-        (f.selector == pushBack(bytes32).selector && lengthAfter == lengthBefore + 1) ||
-        (f.selector == popBack().selector && lengthAfter == lengthBefore - 1) ||
-        (f.selector == popFront().selector && lengthAfter == lengthBefore - 1) ||
-        (f.selector == clear().selector && lengthAfter == 0)
+        (f.selector == sig:pushFront(bytes32).selector && to_mathint(lengthAfter) == lengthBefore + 1) ||
+        (f.selector == sig:pushBack(bytes32).selector  && to_mathint(lengthAfter) == lengthBefore + 1) ||
+        (f.selector == sig:popBack().selector          && to_mathint(lengthAfter) == lengthBefore - 1) ||
+        (f.selector == sig:popFront().selector         && to_mathint(lengthAfter) == lengthBefore - 1) ||
+        (f.selector == sig:clear().selector            && lengthAfter == 0)
     ), "length is only affected by clear/pop/push operations";
 }
 
@@ -341,9 +278,6 @@ rule noLengthChange(env e) {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule noDataChange(env e) {
-    requireInvariant boundariesConsistency();
-    require boundedQueue();
-
     method f;
     calldataarg args;
 
@@ -354,13 +288,13 @@ rule noDataChange(env e) {
     bool atAfterSuccess = !lastReverted;
 
     assert !atAfterSuccess <=> (
-        f.selector == clear().selector ||
-        (f.selector == popBack().selector && index == length()) ||
-        (f.selector == popFront().selector && index == length())
+        (f.selector == sig:clear().selector                        ) ||
+        (f.selector == sig:popBack().selector  && index == length()) ||
+        (f.selector == sig:popFront().selector && index == length())
     ), "indexes of the queue are only removed by clear or pop";
 
     assert atAfterSuccess && atAfter != atBefore => (
-        f.selector == popFront().selector ||
-        f.selector == pushFront(bytes32).selector
+        f.selector == sig:popFront().selector ||
+        f.selector == sig:pushFront(bytes32).selector
     ), "values of the queue are only changed by popFront or pushFront";
 }
diff --git a/certora/specs/helpers/helpers.spec b/certora/specs/helpers/helpers.spec
index 04e76df94ae..a6c1e230248 100644
--- a/certora/specs/helpers/helpers.spec
+++ b/certora/specs/helpers/helpers.spec
@@ -2,9 +2,6 @@
 definition nonpayable(env e) returns bool = e.msg.value == 0;
 definition nonzerosender(env e) returns bool = e.msg.sender != 0;
 
-// constants
-definition max_uint48() returns mathint = (1 << 48) - 1;
-
 // math
 definition min(mathint a, mathint b) returns mathint = a < b ? a : b;
 definition max(mathint a, mathint b) returns mathint = a > b ? a : b;
diff --git a/contracts/utils/structs/DoubleEndedQueue.sol b/contracts/utils/structs/DoubleEndedQueue.sol
index 30d9532393d..928665beee8 100644
--- a/contracts/utils/structs/DoubleEndedQueue.sol
+++ b/contracts/utils/structs/DoubleEndedQueue.sol
@@ -2,8 +2,6 @@
 // OpenZeppelin Contracts (last updated v4.9.0) (utils/structs/DoubleEndedQueue.sol)
 pragma solidity ^0.8.19;
 
-import {SafeCast} from "../math/SafeCast.sol";
-
 /**
  * @dev A sequence of items with the ability to efficiently push and pop items (i.e. insert and remove) on both ends of
  * the sequence (called front and back). Among other access patterns, it can be used to implement efficient LIFO and
@@ -22,6 +20,11 @@ library DoubleEndedQueue {
      */
     error QueueEmpty();
 
+    /**
+     * @dev A push operation couldn't be completed due to the queue being full.
+     */
+    error QueueFull();
+
     /**
      * @dev An operation (e.g. {at}) couldn't be completed due to an index being out of bounds.
      */
@@ -40,18 +43,19 @@ library DoubleEndedQueue {
      * data[end - 1].
      */
     struct Bytes32Deque {
-        int128 _begin;
-        int128 _end;
-        mapping(int128 => bytes32) _data;
+        uint128 _begin;
+        uint128 _end;
+        mapping(uint128 => bytes32) _data;
     }
 
     /**
      * @dev Inserts an item at the end of the queue.
      */
     function pushBack(Bytes32Deque storage deque, bytes32 value) internal {
-        int128 backIndex = deque._end;
-        deque._data[backIndex] = value;
         unchecked {
+            uint128 backIndex = deque._end;
+            if (backIndex + 1 == deque._begin) revert QueueFull();
+            deque._data[backIndex] = value;
             deque._end = backIndex + 1;
         }
     }
@@ -62,26 +66,26 @@ library DoubleEndedQueue {
      * Reverts with `QueueEmpty` if the queue is empty.
      */
     function popBack(Bytes32Deque storage deque) internal returns (bytes32 value) {
-        if (empty(deque)) revert QueueEmpty();
-        int128 backIndex;
         unchecked {
-            backIndex = deque._end - 1;
+            uint128 backIndex = deque._end;
+            if (backIndex == deque._begin) revert QueueEmpty();
+            --backIndex;
+            value = deque._data[backIndex];
+            delete deque._data[backIndex];
+            deque._end = backIndex;
         }
-        value = deque._data[backIndex];
-        delete deque._data[backIndex];
-        deque._end = backIndex;
     }
 
     /**
      * @dev Inserts an item at the beginning of the queue.
      */
     function pushFront(Bytes32Deque storage deque, bytes32 value) internal {
-        int128 frontIndex;
         unchecked {
-            frontIndex = deque._begin - 1;
+            uint128 frontIndex = deque._begin - 1;
+            if (frontIndex == deque._end) revert QueueFull();
+            deque._data[frontIndex] = value;
+            deque._begin = frontIndex;
         }
-        deque._data[frontIndex] = value;
-        deque._begin = frontIndex;
     }
 
     /**
@@ -90,11 +94,11 @@ library DoubleEndedQueue {
      * Reverts with `QueueEmpty` if the queue is empty.
      */
     function popFront(Bytes32Deque storage deque) internal returns (bytes32 value) {
-        if (empty(deque)) revert QueueEmpty();
-        int128 frontIndex = deque._begin;
-        value = deque._data[frontIndex];
-        delete deque._data[frontIndex];
         unchecked {
+            uint128 frontIndex = deque._begin;
+            if (frontIndex == deque._end) revert QueueEmpty();
+            value = deque._data[frontIndex];
+            delete deque._data[frontIndex];
             deque._begin = frontIndex + 1;
         }
     }
@@ -106,8 +110,7 @@ library DoubleEndedQueue {
      */
     function front(Bytes32Deque storage deque) internal view returns (bytes32 value) {
         if (empty(deque)) revert QueueEmpty();
-        int128 frontIndex = deque._begin;
-        return deque._data[frontIndex];
+        return deque._data[deque._begin];
     }
 
     /**
@@ -117,11 +120,9 @@ library DoubleEndedQueue {
      */
     function back(Bytes32Deque storage deque) internal view returns (bytes32 value) {
         if (empty(deque)) revert QueueEmpty();
-        int128 backIndex;
         unchecked {
-            backIndex = deque._end - 1;
+            return deque._data[deque._end - 1];
         }
-        return deque._data[backIndex];
     }
 
     /**
@@ -131,10 +132,11 @@ library DoubleEndedQueue {
      * Reverts with `QueueOutOfBounds` if the index is out of bounds.
      */
     function at(Bytes32Deque storage deque, uint256 index) internal view returns (bytes32 value) {
-        // int256(deque._begin) is a safe upcast
-        int128 idx = SafeCast.toInt128(int256(deque._begin) + SafeCast.toInt256(index));
-        if (idx >= deque._end) revert QueueOutOfBounds();
-        return deque._data[idx];
+        if (index >= length(deque)) revert QueueOutOfBounds();
+        // By construction, length is a uint128, so the check above ensures that index can be safely downcast to uint128.
+        unchecked {
+            return deque._data[deque._begin + uint128(index)];
+        }
     }
 
     /**
@@ -152,10 +154,8 @@ library DoubleEndedQueue {
      * @dev Returns the number of items in the queue.
      */
     function length(Bytes32Deque storage deque) internal view returns (uint256) {
-        // The interface preserves the invariant that begin <= end so we assume this will not overflow.
-        // We also assume there are at most int256.max items in the queue.
         unchecked {
-            return uint256(int256(deque._end) - int256(deque._begin));
+            return uint256(deque._end - deque._begin);
         }
     }
 
@@ -163,6 +163,6 @@ library DoubleEndedQueue {
      * @dev Returns true if the queue is empty.
      */
     function empty(Bytes32Deque storage deque) internal view returns (bool) {
-        return deque._end <= deque._begin;
+        return deque._end == deque._begin;
     }
 }
diff --git a/requirements.txt b/requirements.txt
index da3e95766cb..b92a2728d53 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1 +1 @@
-certora-cli==3.6.4
+certora-cli==4.3.1