diff --git a/certora_autosetup/certora/specs/summaries/EIP712.spec b/certora_autosetup/certora/specs/summaries/EIP712.spec
new file mode 100644
index 00000000..a7365efa
--- /dev/null
+++ b/certora_autosetup/certora/specs/summaries/EIP712.spec
@@ -0,0 +1,22 @@
+// EIP-712 typed-data hashing (solady `_hashTypedData`, OpenZeppelin `_hashTypedDataV4`).
+// The digest is a keccak over the domain separator and the struct hash, whose assembly
+// defeats the points-to analysis. It is modeled as a deterministic, injective
+// uninterpreted function of the struct hash: sound, keeps equal struct hashes mapped to
+// equal digests, and distinct struct hashes to distinct digests (collision-freedom,
+// matching the optimistic-hashing assumption).
+//
+// Injectivity is encoded via a left-inverse ghost rather than a two-variable forall:
+// recovering the struct hash from the digest is equivalent to injectivity (equal digests
+// force equal struct hashes through the inverse) but quantifies one variable and applies
+// the hash once, so the solver instantiates it linearly instead of over every pair.
+
+persistent ghost cvlHashTypedDataInv(bytes32) returns bytes32;
+
+persistent ghost cvlHashTypedData(bytes32) returns bytes32 {
+    axiom forall bytes32 s. cvlHashTypedDataInv(cvlHashTypedData(s)) == s;
+}
+
+methods {
+    function EIP712._hashTypedData(bytes32 structHash) internal returns (bytes32) => cvlHashTypedData(structHash);
+    function EIP712._hashTypedDataV4(bytes32 structHash) internal returns (bytes32) => cvlHashTypedData(structHash);
+}
diff --git a/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec b/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec
new file mode 100644
index 00000000..2297c2bc
--- /dev/null
+++ b/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec
@@ -0,0 +1,9 @@
+// OpenZeppelin Arrays.unsafeMemoryAccess: an unchecked (assembly `mload`) memory
+// array read whose raw pointer arithmetic defeats the points-to analysis. It reads
+// the element at `pos` without a bounds check, so it is modeled as `arr[pos]` (the
+// caller is responsible for `pos` being in bounds, matching the function's contract).
+methods {
+    function Arrays.unsafeMemoryAccess(uint256[] memory arr, uint256 pos) internal returns (uint256) => arr[pos];
+    function Arrays.unsafeMemoryAccess(bytes32[] memory arr, uint256 pos) internal returns (bytes32) => arr[pos];
+    function Arrays.unsafeMemoryAccess(address[] memory arr, uint256 pos) internal returns (address) => arr[pos];
+}
diff --git a/certora_autosetup/certora/specs/summaries/extload.template.spec b/certora_autosetup/certora/specs/summaries/extload.template.spec
index 01fa6b1e..49c7bdfa 100644
--- a/certora_autosetup/certora/specs/summaries/extload.template.spec
+++ b/certora_autosetup/certora/specs/summaries/extload.template.spec
@@ -7,6 +7,9 @@ methods {
     function $CONTRACT_NAME$.exttload(bytes32 slot) external returns (bytes32) => NONDET DELETE;
     function $CONTRACT_NAME$.exttload(bytes32[] slots) external returns (bytes32[] memory) => ArbBytes32(slots) DELETE;
     function $CONTRACT_NAME$.exttload(bytes32[] slots) external returns (bytes memory) => ArbBytes(slots) DELETE;
+    // camelCase naming (e.g. Aave: extSload / extSloads)
+    function $CONTRACT_NAME$.extSload(bytes32 slot) external returns (bytes32) => NONDET DELETE;
+    function $CONTRACT_NAME$.extSloads(bytes32[] slots) external returns (bytes32[] memory) => ArbBytes32(slots) DELETE;
 }
 
 function ArbBytes32(bytes32[] slots) returns bytes32[] {
diff --git a/certora_autosetup/setup/function_summaries.json b/certora_autosetup/setup/function_summaries.json
index 221284b2..a066c2a0 100644
--- a/certora_autosetup/setup/function_summaries.json
+++ b/certora_autosetup/setup/function_summaries.json
@@ -107,10 +107,22 @@
     "description": "OpenZeppelin BitMaps operations",
     "additional_contracts": ["specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol"]
   },
+  "oz_arrays_unsafeMemoryAccess": {
+    "names": ["unsafeMemoryAccess"],
+    "library_names": ["Arrays"],
+    "summary_file": "specs/summaries/OpenZeppelin/OZ_Arrays.spec",
+    "description": "OpenZeppelin Arrays.unsafeMemoryAccess (unchecked memory array read)"
+  },
+  "eip712_hashTypedData": {
+    "names": ["_hashTypedData", "_hashTypedDataV4"],
+    "library_names": ["EIP712"],
+    "summary_file": "specs/summaries/EIP712.spec",
+    "description": "EIP-712 typed-data hashing (solady _hashTypedData / OpenZeppelin _hashTypedDataV4)"
+  },
   "extload": {
-    "names": ["extsload", "exttload"],
+    "names": ["extsload", "exttload", "extSload", "extSloads"],
     "summary_file": "specs/summaries/extload.template.spec",
-    "description": "External storage load functions (extsload/exttload)"
+    "description": "External storage load functions (extsload/exttload, incl. camelCase extSload/extSloads)"
   },
   "safeTransfer": {
     "names": ["safeTransfer"],