diff --git a/.circleci/config.yml b/.circleci/config.yml
index 4fc7b72e..edd10bcc 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -69,7 +69,7 @@ jobs:
   
   check-release:
     docker:
-      - image: &img public.ecr.aws/certora/cvt-image:2024.06.13-3755-0351582
+      - image: &cvt public.ecr.aws/certora/cvt-image:2024.10.16-4473-ba570af
     resource_class: small
     working_directory: ~/repo
     steps:
@@ -116,7 +116,7 @@ jobs:
         type: string
         default: ""
     docker:
-      - image: &img public.ecr.aws/certora/cvt-image:2024.06.13-3755-0351582
+      - image: *cvt
     resource_class: small
     working_directory: ~/repo
     environment:
@@ -162,7 +162,7 @@ jobs:
       certora_cli_package:
         type: string
     docker:
-      - image: &img public.ecr.aws/certora/cvt-image:2024.06.13-3755-0351582
+      - image: *cvt
     resource_class: small
     working_directory: ~/repo
     steps:
@@ -183,7 +183,6 @@ jobs:
           path: ~/repo
 
 
-
 parameters:
   run_regtest:
     default: false
diff --git a/CVLByExample/ConfInheritance/MainContract.sol b/CVLByExample/ConfInheritance/MainContract.sol
new file mode 100644
index 00000000..4159bc2f
--- /dev/null
+++ b/CVLByExample/ConfInheritance/MainContract.sol
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract MainContract 
+{
+    address currentBidder;
+    uint256 public currentBid;
+
+    // At the entrance to `bid` address(this).balance is already increased by msg.value,
+    // so the receiver gets  `msg.value + address(this).balance` before.
+    // This reverts only if msg.value < address(this).balance
+    function bid() public payable
+    {
+        require(msg.value >= address(this).balance);
+        payable(currentBidder).transfer(address(this).balance);
+        currentBidder = msg.sender; 
+        currentBid = msg.value;
+    }
+}
\ No newline at end of file
diff --git a/CVLByExample/ConfInheritance/MainSpec.spec b/CVLByExample/ConfInheritance/MainSpec.spec
new file mode 100644
index 00000000..f6ee6195
--- /dev/null
+++ b/CVLByExample/ConfInheritance/MainSpec.spec
@@ -0,0 +1,44 @@
+/**
+ * @title  Native balances Example
+ *
+ * This is an example specification for using nativeBalances.
+ */
+
+methods {
+    function currentBid() external returns uint256 envfree; 
+}
+
+/// @title Basic rules ////////////////////////////////////////////////////
+
+/***
+ This rule demonstrates how the source of amount transferred affects the balance of the current contract.
+ This rule fails for `Auction.sol` because:
+ 1. The balance of `currentContract` is increased by `msg.value` at the entrance to `bid()`.
+ 2. the sender changes to `currentContract` in internal `bid()` and all his balance is transferred, so his balance does not increase.
+ This rule passes for `AuctionFixed.sol` because only `currentBid` is transferred.
+ */
+rule bidIncreasesAssets() {
+    env e;
+    require(e.msg.sender != currentContract);
+    require(e.msg.value > currentBid() );
+    uint256 balanceBefore = nativeBalances[currentContract];
+    bid(e);
+    assert nativeBalances[currentContract] > balanceBefore;
+}
+
+/***
+ This rule demonstrates how the source of amount transferred affects the balance of the current contract.
+ This rule passes vacuously for `Auction.sol` because of the `require e.msg.value > nativeBalances[currentContract]` in the spec
+ and `require msg.value >= msg.value + nativeBalances[currentContract]` in the code where `nativeBalances[currentContract] > 0`.
+ It passes non-vacuously for AuctionFixed.sol because the amount transferred is `currentBid` for which `msg.value >= currentBid`
+ can hold.
+ */
+rule bidSuccessfullyExpectVacuous() {
+    env e;
+    uint256 balanceBefore = nativeBalances[currentContract];
+    require(e.msg.sender != currentContract);
+    require(e.msg.value > 0 &&  e.msg.value > balanceBefore);
+    require (balanceBefore > 0);
+    bid(e);
+    assert nativeBalances[currentContract] >= balanceBefore;
+}
diff --git a/CVLByExample/ConfInheritance/README.md b/CVLByExample/ConfInheritance/README.md
new file mode 100644
index 00000000..49e87f54
--- /dev/null
+++ b/CVLByExample/ConfInheritance/README.md
@@ -0,0 +1,109 @@
+# Configuration File Inheritance Example
+
+This folder demonstrates how to use the **`override_base_config`** feature to inherit and selectively modify Certora Prover configuration files. By defining **common** settings in a **base** config (`base.conf`) and referencing it from different child configs, you can avoid duplication and streamline maintenance.
+
+---
+
+## Files
+
+1. **`MainContract.sol`**  
+   A minimal Solidity contract to be verified.
+
+2. **`base.conf`**  
+   **Base** configuration with shared defaults:
+   ```jsonc
+   {
+     "files": ["MainContract.sol"],
+     "verify": "MainContract:MainContract.spec",
+     "msg": "Main contract",
+     "optimistic_loop": true,
+     "loop_iter": "3",
+     "rule_sanity": "basic"
+   }
+   ```
+   - Defines the source files, contract–spec pairing, default loop settings, etc.
+
+3. **`new_fields.conf`**  
+   Child config **adding** a new field (`optimistic_hashing`) not present in `base.conf`:
+   ```jsonc
+   {
+     "override_base_config": "base.conf",
+     "optimistic_hashing": true
+   }
+   ```
+
+4. **`override_fields.conf`**  
+   Child config **overriding** certain fields from `base.conf`:
+   ```jsonc
+   {
+     "override_base_config": "base.conf",
+     "loop_iter": "10",
+     "optimistic_loop": false
+   }
+   ```
+
+5. **`invalid_base.conf`**  
+   A config that **incorrectly** attempts to act as a base while also referencing **another** base:
+   ```jsonc
+   {
+     "files": ["MainContract.sol"],
+     "verify": "MainContract:MainContract.spec",
+     "msg": "Main contract",
+     "optimistic_loop": true,
+     "loop_iter": "3",
+     "rule_sanity": "basic",
+     "override_base_config": "base.conf"
+   }
+   ```
+   - **This is invalid** because a base config must **not** itself contain `override_base_config`.
+   - The feature currently supports **only one** level of inheritance (no nested base configs).
+
+---
+
+## Usage Examples
+
+### Merging **`base.conf`** + **`new_fields.conf`**
+```bash
+certoraRun new_fields.conf
+```
+- Inherits `base.conf` and **adds** `"optimistic_hashing": true`.
+
+### Merging **`base.conf`** + **`override_fields.conf`**
+```bash
+certoraRun override_fields.conf
+```
+- Changes `loop_iter` from `"3"` to `"10"` and sets `optimistic_loop` to `false`.
+
+---
+
+## Invalid Base Example
+### Attempting to Use **`invalid_base.conf`**
+```bash
+certoraRun invalid_base.conf
+```
+Error:
+```
+certoraRun invalid_base.conf
+
+Cannot load base config: override_fields.conf
+base config cannot include 'override_base_config'
+
+Error when reading invalid_base.conf: Cannot load base config: override_fields.conf
+base config cannot include 'override_base_config'
+```
+
+- **`invalid_base.conf`** tries to reference `override_fields.conf` as a base config.
+- **This is disallowed** because the feature only supports **single-level inheritance**: a base config **cannot** itself specify an `override_base_config` field.
+
+---
+
+## Why Use `override_base_config`?
+
+1. **Reduce Duplication**  
+   Common fields (e.g., file lists, compiler version, environment arguments) live in **one** place.
+
+2. **Clear Overrides**  
+   Child configs only show what differs from the parent.
+
+3. **Easier Maintenance**  
+   Updating a shared parameter (e.g., loop iterations) means editing just one file.
diff --git a/CVLByExample/ConfInheritance/base.conf b/CVLByExample/ConfInheritance/base.conf
new file mode 100644
index 00000000..c7854234
--- /dev/null
+++ b/CVLByExample/ConfInheritance/base.conf
@@ -0,0 +1,10 @@
+{
+  "files": [
+    "MainContract.sol",
+  ],
+  "verify": "MainContract:MainSpec.spec",
+  "msg": "Main contract",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic"
+}
diff --git a/CVLByExample/ConfInheritance/invalid_base.conf b/CVLByExample/ConfInheritance/invalid_base.conf
new file mode 100644
index 00000000..d3b5ebec
--- /dev/null
+++ b/CVLByExample/ConfInheritance/invalid_base.conf
@@ -0,0 +1,11 @@
+{
+  "files": [
+    "MainContract.sol",
+  ],
+  "verify": "MainContract:MainSpec.spec",
+  "msg": "Main contract",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "override_base_config": "override_fields.conf",
+}
diff --git a/CVLByExample/ConfInheritance/new_fields.conf b/CVLByExample/ConfInheritance/new_fields.conf
new file mode 100644
index 00000000..9db89fe4
--- /dev/null
+++ b/CVLByExample/ConfInheritance/new_fields.conf
@@ -0,0 +1,5 @@
+{
+  "override_base_config": "base.conf",
+  "optimistic_hashing": true,
+}
+
diff --git a/CVLByExample/ConfInheritance/override_fields.conf b/CVLByExample/ConfInheritance/override_fields.conf
new file mode 100644
index 00000000..64dda4b2
--- /dev/null
+++ b/CVLByExample/ConfInheritance/override_fields.conf
@@ -0,0 +1,6 @@
+{
+  "override_base_config": "base.conf",
+  "loop_iter": "10",
+  "optimistic_loop": false,
+}
+
diff --git a/CVLByExample/README.md b/CVLByExample/README.md
index 0570a367..19596221 100644
--- a/CVLByExample/README.md
+++ b/CVLByExample/README.md
@@ -44,6 +44,7 @@
 | **ContractAlias**  | [example](https://github.com/Certora/Examples/blob/42395eb745d20c40c14f297fd28b3a658f87f889/CVLByExample/ContractAlias/ContractAlias.spec#L1-L3) |
 | **StoreToArray**  | [example](https://github.com/Certora/Examples/blob/niv/CERT-6524/CVLByExample/Types/StoreToArray/StoreToArray.spec#L4) |
 | **HookOnResetStorageCommand**  | [example](https://github.com/Certora/Examples/blob/niv/CERT-7022-Add-Hook-On-Reset-Storage-Example/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec#L1-L10) |
+| **RevertKeyWord**  | [example](https://github.com/Certora/Examples/blob/niv/CERT-8248-Revert-Example/CVLByExample/RevertKeyWord/example.spec#L13) |
 
 
 
diff --git a/CVLByExample/RevertKeyWord/C.sol b/CVLByExample/RevertKeyWord/C.sol
new file mode 100644
index 00000000..fad61a85
--- /dev/null
+++ b/CVLByExample/RevertKeyWord/C.sol
@@ -0,0 +1,49 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+/**
+ * @title C
+ * @dev A simple contract demonstrating functions that can revert
+ */
+contract C {
+    bool public fooWasCalled;
+
+    /**
+     * @notice Sets fooWasCalled and reverts if the input b is false
+     */
+    function foo(bool b) external {
+        fooWasCalled = true;
+        if (!b) {
+            revert("foo reverted");
+        }
+    }
+
+    /**
+     * @notice Calls foo and can therefore revert if foo reverts
+     */
+    function callFooFromContract(bool b) external {
+        this.foo(b);
+    }
+
+    /**
+     * @notice Dummy function that can be used to demonstrate "summary" usage
+     */
+    function summarizeMe(bool b) external {}
+
+    /**
+     * @notice Returns b or reverts if b is false
+     */
+    function canRevert(bool b) external returns (bool) {
+        if (!b) {
+            revert("canRevert reverted");
+        }
+        return b;
+    }
+
+    /**
+     * @notice Calls summarizeMe and can be used for demonstration of deeper calls
+     */
+    function callSummarizeMe(bool b) external {
+        this.summarizeMe(b);
+    }
+}
diff --git a/CVLByExample/RevertKeyWord/README.md b/CVLByExample/RevertKeyWord/README.md
new file mode 100644
index 00000000..47363c65
--- /dev/null
+++ b/CVLByExample/RevertKeyWord/README.md
@@ -0,0 +1,49 @@
+# CVL Revert Feature Example
+
+This folder demonstrates the newly introduced **CVL revert functionality** and the **`@withrevert`** annotation. These features allow you to:
+
+1. **Explicitly revert** inside CVL functions (e.g. `revert("some reason")`).
+2. **Capture revert signals** when calling any function—Solidity or CVL—using the `@withrevert` annotation, which sets the built-in CVL variable `lastReverted` to `true` if a revert occurs.
+
+## Files
+
+1. **`C.sol`**  
+   A simple Solidity contract with functions that may revert. The contract contains:
+   - `foo(bool b)`: sets a flag and reverts if `b` is false.  
+   - `canRevert(bool b)`: returns `b` or reverts if `b` is false.  
+   - `summarizeMe(bool b)`: a dummy function, used for demonstrating a CVL summary that can also revert.  
+   - `callSummarizeMe(bool b)`: calls `summarizeMe`; used to show how reverts in a summary can bubble up.  
+   - Additional helper functions like `callFooFromContract`.
+
+2. **`example.spec`**  
+   A CVL spec demonstrating:
+   - Calling a Solidity function with `@withrevert`, e.g. `foo@withrevert(b)`.
+   - Writing a CVL function (`cvlFunctionThatMayRevert`) that explicitly reverts when a condition fails.
+   - Two different ways to handle potential reverts from `canRevert(bool)`, illustrating how revert can either be captured inline or bubble up through a CVL wrapper.
+   - A **“summarize”** function, `cvlSummarizeMe`, that can revert if its boolean parameter is false, invoked via the contract function `callSummarizeMe@withrevert(b)`.
+
+## Usage
+
+1. **Command**
+    ```shell
+    certoraRun example.conf --server production --prover_version master
+    ```
+2. **Expected Output**
+    - The output should confirm that the spec passes, with the expected behavior of `lastReverted` in each case.
+    - Link: [Example Output](https://prover.certora.com/output/1512/3919ff99f4e84203a04e4aeab4fc8c11?anonymousKey=3a7682aefc6e9b26f248f7fc7a1aff60557281cf)
+
+3. **Examine the Rules**  
+   - **`testFooWithRevert`**  
+     Confirms that calling `foo` with `@withrevert` sets `lastReverted` exactly when the argument is false.  
+   - **`testCvlFunctionWithRevert`**  
+     Demonstrates how a CVL function (`cvlFunctionThatMayRevert`) can explicitly revert, and how `@withrevert` captures that.  
+   - **`testCanRevertInline`**  
+     Uses `wrapperForCanRevertInline(bool)`, which internally calls `canRevert@withrevert(condition)`, returning `lastReverted`.  
+   - **`testCanRevertBubbleUp`**  
+     Illustrates revert **bubbling up**. In `wrapperForCanRevertBubble(bool)`, we call `canRevert(condition)` *without* `@withrevert`, but then call the wrapper itself with `@withrevert`. The internal revert propagates, setting `lastReverted`.  
+   - **`testCallSummarizeMe`**  
+     Demonstrates a contract function (`callSummarizeMe`) that calls a **CVL summary** (`cvlSummarizeMe`). If the summary reverts (when the boolean input is false), the revert bubbles up to the contract caller, setting `lastReverted`.
+
+## Conclusion
+
+With these files (`C.sol`, `example.spec`, `Example.conf`, and this `README.md`), you can see how the new CVL revert feature works in practice. By enabling the `-cvlFunctionRevert` flag, you can write more expressive and accurate specs that treat reverts in CVL and Solidity calls consistently, capturing those reverts in **`lastReverted`** for precise modeling in your verification. The **bubble-up** behavior especially highlights how deeper CVL calls (including **summaries**) can now propagate reverts just like Solidity calls.
diff --git a/CVLByExample/RevertKeyWord/example.conf b/CVLByExample/RevertKeyWord/example.conf
new file mode 100644
index 00000000..6a697400
--- /dev/null
+++ b/CVLByExample/RevertKeyWord/example.conf
@@ -0,0 +1,13 @@
+{
+    "files": [
+        "C.sol"
+    ],
+    "independent_satisfy": true,
+    "process": "emv",
+    "solc": "solc8.26",
+    "verify": "C:example.spec",
+    "prover_args": [
+        "-cvlFunctionRevert true"
+    ],
+    "rule_sanity": "basic"
+}
diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec
new file mode 100644
index 00000000..a6a1f9bf
--- /dev/null
+++ b/CVLByExample/RevertKeyWord/example.spec
@@ -0,0 +1,109 @@
+// ---------------------------------------------------------
+// 1. Declare the contract methods we want to verify/inspect
+// ---------------------------------------------------------
+methods {
+    // Contract functions that may revert
+    function foo(bool) external envfree;
+    function canRevert(bool) external returns bool envfree;
+
+    // For demonstrating summary usage
+    function callSummarizeMe(bool) external envfree;
+    function summarizeMe(bool b) external => cvlSummarizeMe(b);
+}
+
+// ---------------------------------------------------------
+// 2. CVL function that explicitly uses the 'revert' keyword
+// ---------------------------------------------------------
+function cvlFunctionThatMayRevert(bool input) {
+    if (!input) {
+        revert("Input was false in CVL function");
+    }
+}
+
+// ---------------------------------------------------------
+// 3. A summary function that can revert.
+// ---------------------------------------------------------
+// The contract's `summarizeMe(bool b)` is mapped to `cvlSummarizeMe(b)` in CVL.
+// If `b` is false, we revert with a message. When called via `callSummarizeMe@withrevert(b)`,
+// any revert here bubbles up and sets `lastReverted`.
+function cvlSummarizeMe(bool b) {
+    if (!b) {
+        revert("Summarize revert because b is false");
+    }
+}
+
+// ---------------------------------------------------------
+// 4. Example rule: calling 'foo' with @withrevert
+// ---------------------------------------------------------
+rule testFooWithRevert {
+    bool condition;
+    // Using @withrevert to capture whether 'foo' reverts
+    foo@withrevert(condition);
+
+    // 'foo' reverts when 'condition' is false
+    assert lastReverted <=> !condition;
+}
+
+// ---------------------------------------------------------
+// 5. Example rule: calling a CVL function with @withrevert
+// ---------------------------------------------------------
+rule testCvlFunctionWithRevert {
+    bool condition;
+    // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' is set to true
+    cvlFunctionThatMayRevert@withrevert(condition);
+
+    // Check that 'lastReverted' matches whether 'condition' was false
+    assert lastReverted <=> !condition;
+}
+
+// ---------------------------------------------------------
+// 6. Demonstration #1 for canRevert: inline approach
+// ---------------------------------------------------------
+function wrapperForCanRevertInline(bool condition) returns bool {
+    // Here we call canRevert WITH @withrevert internally
+    canRevert@withrevert(condition);
+    return lastReverted; // We return the revert status
+}
+
+rule testCanRevertInline {
+    bool condition;
+    bool outcome = wrapperForCanRevertInline(condition);
+
+    // 'outcome' is true exactly when 'condition' is false (i.e., canRevert reverts)
+    assert outcome <=> !condition;
+}
+
+// ---------------------------------------------------------
+// 7. Demonstration #2 for canRevert: revert "bubbling up"
+// ---------------------------------------------------------
+// We call 'canRevert(condition)' WITHOUT '@withrevert' inside the wrapper,
+// letting the revert bubble up to the outer call (the rule).
+function wrapperForCanRevertBubble(bool condition) {
+    canRevert(condition);
+}
+
+rule testCanRevertBubbleUp {
+    bool condition;
+    // We call the wrapper with @withrevert, so if 'canRevert' reverts, it bubbles up
+    wrapperForCanRevertBubble@withrevert(condition);
+
+    // If 'condition' is false => 'canRevert' reverts => bubble up => lastReverted = true
+    assert lastReverted <=> !condition;
+}
+
+// ---------------------------------------------------------
+// 8. Summarize-Me case: the "most interesting" scenario
+// ---------------------------------------------------------
+// The contract function callSummarizeMe(b) calls summarizeMe(b),
+// which is summarized by cvlSummarizeMe(b). That summary reverts
+// if b == false. We'll use the 'rule sanity basic' flag to see the call trace.
+rule testCallSummarizeMe{
+    bool condition;
+    // Because summarizeMe is mapped to cvlSummarizeMe in CVL (which can revert),
+// calling callSummarizeMe with @withrevert will set lastReverted if condition == false.
+    callSummarizeMe@withrevert(condition);
+
+    // If condition is false => revert => lastReverted = true
+    // If condition is true => no revert => lastReverted = false
+    assert lastReverted <=> !condition;
+}
diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.conf b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.conf
new file mode 100644
index 00000000..9c5c9649
--- /dev/null
+++ b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.conf
@@ -0,0 +1,12 @@
+{
+    "files": [
+        "CalledContractAndExecutingContract.sol:Primary",
+        "CalledContractAndExecutingContract.sol:Secondary",
+        "CalledContractAndExecutingContract.sol:Tertiary"
+    ],
+    "link": [
+        "Primary:secondary=Secondary",
+        "Primary:tertiary=Tertiary"
+    ],
+    "verify": "Primary:CalledContractAndExecutingContract.spec"
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.sol b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.sol
new file mode 100644
index 00000000..ba02615e
--- /dev/null
+++ b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.sol
@@ -0,0 +1,103 @@
+// There are two contracts `Primary` and `Secondary` and a library `Library`.
+// Each has a `calleeInternal` and a `calleeExternal` function (these are
+// summarized in CalledContractAndExecutingContract.spec).  There are else several unsummarized `call...`
+// entry points; each is used in a rule in `CalledContractAndExecutingContract.spec`.
+
+contract Primary {
+
+    Secondary secondary;
+    Tertiary tertiary;
+
+    // callee functions are summarized
+
+    function calleeInternal() internal { }
+    function calleeExternal() external { }
+
+    // call functions are unsummarized; each corresponds to an example
+
+    function callPrimaryInternal() external {
+        calleeInternal();
+    }
+
+    function callSecondaryInternal() external {
+        secondary.callSecondaryInternal();
+    }
+
+    function callPrimaryExternal() external {
+        this.calleeExternal();
+    }
+
+    function callSecondaryExternal() external {
+        secondary.calleeExternal();
+    }
+
+    function callPrimaryExternalFromSecondary() external {
+        secondary.callPrimaryExternal(this);
+    }
+
+    function callLibraryInternalFromPrimary() external {
+        Library.calleeInternal();
+    }
+
+    function callLibraryExternalFromPrimary() external {
+        Library.calleeExternal();
+    }
+
+    function callLibraryInternalFromSecondary() external {
+        secondary.callLibraryInternal();
+    }
+
+    function callLibraryExternalFromSecondary() external {
+        secondary.callLibraryExternal();
+    }
+
+    function callTertiaryThroughSecondary() external {
+        secondary.callTertiaryExternal(tertiary);
+    }
+
+    function callSecondaryExternalViaDelegate() external {
+        address(secondary).delegatecall(abi.encodeWithSignature("calleeExternal()"));
+    }
+}
+
+
+contract Secondary {
+    // the `callee` methods are summarized
+
+    function calleeExternal() external { }
+    function calleeInternal() internal { }
+
+    // the `call` methods are used to dispatch to the callee methods
+
+    function callPrimaryExternal(Primary receiver) external {
+        receiver.calleeExternal();
+    }
+
+    function callSecondaryInternal() external {
+        calleeInternal();
+    }
+
+    function callLibraryInternal() external {
+        Library.calleeInternal();
+    }
+
+    function callLibraryExternal() external {
+        Library.calleeExternal();
+    }
+
+    function callTertiaryExternal(Tertiary receiver) external {
+        receiver.calleeExternal();
+    }
+}
+
+library Library {
+    function calleeExternal() external { }
+    function calleeInternal() internal { }
+}
+
+contract Tertiary {
+    // the `callee` methods are summarized
+
+    function calleeExternal() external { }
+    function calleeInternal() internal { }
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec
new file mode 100644
index 00000000..69ea61d3
--- /dev/null
+++ b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec
@@ -0,0 +1,136 @@
+// There are two contracts `Primary` and `Secondary` and a library `Library`,
+// each having a (summarized) `calleeInternal` and a `calleeExternal` method.
+// The contracts also have several `call` methods that call the different callee
+// methods from different callers.
+//
+// The summaries for all the `callee` methods save several values in ghosts:
+// * `calledContract` in the `called` ghost.
+// * `executingContract` in the `executing` ghost.
+// * `e.msg.sender` in the `sender` ghost.
+// the rules then check that all ghosts are updated correctly.
+// All assertions should pass.
+
+
+using Primary   as primary;
+using Secondary as secondary;
+using Tertiary  as tertiary;
+
+methods {
+    function _.calleeInternal() internal with (env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void;
+    function _.calleeExternal() external with (env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void ALL;
+}
+
+ghost address called;
+ghost address executing;
+ghost address sender;
+
+function saveContracts(address _called, address _executing, address _sender) {
+    called = _called;
+    executing = _executing;
+    sender = _sender;
+}
+
+rule primaryInternal(env e) {
+    callPrimaryInternal(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+
+rule secondaryInternal(env e) {
+    callSecondaryInternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == primary;
+}
+
+rule primaryExternal(env e) {
+    callPrimaryExternal(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == primary;
+}
+
+rule secondaryExternal(env e) {
+    callSecondaryExternal(e);
+    assert called == secondary;
+    assert executing == primary;
+    assert sender == primary;
+}
+
+rule primaryExternalFromSecondary(env e) {
+    callPrimaryExternalFromSecondary(e);
+    assert called == primary;
+    assert executing == secondary;
+    assert sender == secondary;
+}
+
+rule libraryInternalFromPrimary(env e) {
+    callLibraryInternalFromPrimary(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+
+rule libraryExternalFromPrimary(env e) {
+    callLibraryExternalFromPrimary(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+
+rule libraryInternalFromSecondary(env e) {
+    callLibraryInternalFromSecondary(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == primary;
+}
+
+rule libraryExternalFromSecondary(env e) {
+    callLibraryExternalFromSecondary(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == primary;
+}
+
+rule secondaryToPrimaryFromSpec(env e) {
+    secondary.callPrimaryExternal(e,primary);
+    assert called == primary;
+    assert executing == secondary;
+    assert sender == secondary;
+}
+
+rule secondaryToSecondaryFromSpec(env e) {
+    secondary.callSecondaryInternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == e.msg.sender;
+}
+
+rule secondaryToLibraryInternalFromSpec(env e) {
+    secondary.callLibraryInternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == e.msg.sender;
+}
+
+rule secondaryToLibraryExternalFromSpec(env e) {
+    secondary.callLibraryExternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == e.msg.sender;
+}
+
+rule tertiaryThroughSecondary(env e) {
+    callTertiaryThroughSecondary(e);
+    assert called == tertiary;
+    assert executing == secondary;
+    assert sender == secondary;
+}
+
+rule secondaryExternalViaDelegateFromPrimary(env e) {
+    callSecondaryExternalViaDelegate(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/README.md b/CVLByExample/Summarization/CalledContractAndExecutingContract/README.md
new file mode 100644
index 00000000..6e010c79
--- /dev/null
+++ b/CVLByExample/Summarization/CalledContractAndExecutingContract/README.md
@@ -0,0 +1,109 @@
+# Using `calledContract` and `executingContract` in Summaries
+
+This directory demonstrates how to use two CVL keywords—`calledContract` and `executingContract`—to track function call details within a summary context. The repository contains:
+
+1. A Solidity file, **`CalledContractAndExecutingContract.sol`**, which defines contracts **`Primary`**, **`Secondary`**, and **`Tertiary`**, as well as a **`Library`**.  
+2. A CVL spec file, **`CalledContractAndExecutingContract.spec`**, which verifies rules about contract function calls and how the two new keywords behave under different call types.
+
+## 1. Solidity File Overview
+
+The file **`CalledContractAndExecutingContract.sol`** declares three contracts (`Primary`, `Secondary`, `Tertiary`) and one library (`Library`). Each contract has two “callee” functions:
+
+- `calleeInternal()` – an internal function  
+- `calleeExternal()` – an external function  
+
+In addition, `Primary` and `Secondary` implement various "call" functions that invoke these callee functions in different ways:
+
+1. **Calls within the same contract** (e.g., `Primary` calling its own internal method).  
+2. **Calls to another contract** (e.g., `Primary` calling an external method on `Secondary`).  
+3. **Calls from one contract to another that in turn calls back** (e.g., `Secondary` calling `Primary` again).  
+4. **Library calls**, both internal and external (e.g., `Library.calleeInternal()` from within `Primary` or `Secondary`).  
+5. **Delegate calls**, where `Primary` uses `delegatecall` to call `Secondary`'s external function, ensuring the code runs in `Secondary` but uses `Primary`'s storage context.  
+
+These different invocation patterns let us test when and how `calledContract` and `executingContract` diverge.
+
+## 2. CVL Specification Overview
+
+The **`CalledContractAndExecutingContract.spec`** file does two key things:
+
+1. **Summaries**: Inside the `methods` block, it summarizes every `calleeInternal` and `calleeExternal` function (for all contracts and the library) by calling a helper function, `saveContracts`, which writes into ghost variables `called`, `executing`, and `sender`.
+2. **Rules**: A series of rules each perform a high-level call (e.g., `callPrimaryInternal`, `callSecondaryExternal`, etc.) from the `Primary` contract, and then assert that the ghost variables hold the correct addresses for the **called contract**, the **executing contract**, and the **sender**.  
+
+### 2.1 Summaries (Using `calledContract` and `executingContract`)
+
+In the `methods` block, the specification shows how to attach a summary to an internal or external function:
+
+```solidity
+methods {
+    function _.calleeInternal() internal with (env e)
+        => saveContracts(calledContract, executingContract, e.msg.sender)
+        expect void;
+
+    function _.calleeExternal() external with (env e)
+        => saveContracts(calledContract, executingContract, e.msg.sender)
+        expect void ALL;
+}
+```
+
+Here:
+- **`calledContract`** is the address of the contract on which the summarized function was called.
+- **`executingContract`** is the address of the contract that is actually running the function code.  
+- **`e.msg.sender`** is the caller’s address as specified in the test environment.
+
+These three values are passed to `saveContracts`, which stores them in ghost variables `called`, `executing`, and `sender`:
+
+```solidity
+ghost address called;
+ghost address executing;
+ghost address sender;
+
+function saveContracts(address _called, address _executing, address _sender) {
+    called = _called;
+    executing = _executing;
+    sender = _sender;
+}
+```
+
+By capturing these addresses as ghost variables, we can write rules that check whether the correct caller/callee relationship is preserved.
+
+### 2.2 Rules
+
+Each rule (e.g., `rule primaryInternal(env e)`) performs a specific contract call (like `callPrimaryInternal`) and then checks the ghost variables. For instance:
+
+```solidity
+rule primaryInternal(env e) {
+    callPrimaryInternal(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+```
+
+- We make a call to `callPrimaryInternal`.
+- Internally, this triggers `calleeInternal` on the same contract (`Primary`), setting `called = primary`, `executing = primary`, and `sender = e.msg.sender`.
+- The rule then **asserts** that these ghost variables match the expected values.
+
+By comparing `called`, `executing`, and `sender` in each rule, we ensure that **internal calls**, **external calls**, **delegate calls**, and **library calls** update the ghosts consistently with how the EVM actually routes the call.
+
+## 3. Behavior of `calledContract` and `executingContract`
+
+### `calledContract`
+- Represents the address of the contract on which the summarized method was called, or more precisely in whose context it runs. It is essentially `address(this)` in the context of the original call you are summarizing.
+- For **internal calls**, and non-delegate **external calls** `calledContract` is the same as the contract containing the function.
+- For **library calls** and **delegate calls**, `calledContract` is the contract *initiating* the code execution (since libraries and delegate calls run in the caller’s context).
+
+### `executingContract`
+- Represents the address of the contract that *initiated the call*.
+- For **internal** and **delegate** calls, this will be the same as `calledContract`.
+- For **external** calls, it will be the address of the caller, while `calledContract` is the address of the receiver.
+
+### Additional Notes on the Keywords
+- They are not arbitrary variables that can be combined or manipulated further. You can only pass them into your summary function (e.g., `saveContracts`) or reference them directly in your specification.  
+
+## 4. Run the Example
+To run the example use:
+```
+certoraRun CalledContractAndExecutingContract.conf
+```
+
+[The report of this run](https://prover.certora.com/output/15800/c768f4f7ac724e2db90104a412b7a89b?anonymousKey=2c30fbec58b46141e53e0d2d1693b8b6dab00e27)
diff --git a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
index 0f947b85..f8111ba8 100644
--- a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
+++ b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
@@ -41,10 +41,10 @@ methods{
 function setup(env e){
     address zero_address = 0;
     uint256 MINIMUM_LIQUIDITY = 1000;
-    require totalSupply() == 0 || currentContract._balances[zero_address] == MINIMUM_LIQUIDITY;
-    require currentContract._balances[zero_address] + currentContract._balances[e.msg.sender] <= totalSupply();
-    require _token0 == token0();
-    require _token1 == token1();
+    require totalSupply() == 0 || currentContract._balances[zero_address] == MINIMUM_LIQUIDITY, "Either pool is empty or minimum liquidity is locked";
+    require currentContract._balances[zero_address] + currentContract._balances[e.msg.sender] <= totalSupply(), "Sum of balances does not exceed total supply, rule sumFunds";
+    require _token0 == token0(), "Token0 reference must match contract's token0";
+    require _token1 == token1(), "Token1 reference must match contract's token1";
 }
 
 
@@ -68,11 +68,10 @@ Formula:
 rule integrityOfSwap(address recipient) {
     env e; /* represents global solidity variables such as msg.sender, block.timestamp */
     setup(e);
-    require recipient != currentContract; /* currentContract is a CVL keyword, assigned the main contract under test */  
     uint256 balanceBefore = _token0.balanceOf(recipient);
     uint256 amountOut = swap(_token1, recipient);
     uint256 balanceAfter = _token0.balanceOf(recipient);
-    assert balanceAfter == balanceBefore + amountOut; 
+    assert (recipient != currentContract) => balanceAfter == balanceBefore + amountOut; 
 }
 
 /*
@@ -92,8 +91,8 @@ Formula:
 rule noDecreaseByOther(method f, address account) {
     env e;
     setup(e);
-    require e.msg.sender != account;
-    require account != currentContract; 
+    require e.msg.sender != account, "Sender must be different from account to test unauthorized access";
+    require account != currentContract, "Account must not be the pool contract to properly test balance changes"; 
     uint256 allowance = allowance(account, e.msg.sender); 
     
     uint256 before = currentContract._balances[account];
@@ -132,13 +131,13 @@ invariant balanceGreaterThanReserve()
         // it is not msg.sender. It would not be safe to do if the call was to a function of an unresolved contract.
         preserved _.transferFrom(address sender, address recipient,uint256 amount) with (env e1) {
             requireInvariant allowanceOfPoolAlwaysZero(e1.msg.sender);
-            require e1.msg.sender != currentContract;
+            require e1.msg.sender != currentContract, "The pool does not call itself";
         }
 
         // This preserved is safe because transfer is called from the currentContract whose code is known and
         // it is not msg.sender.
         preserved _.transfer(address recipient, uint256 amount) with (env e2) {
-            require e2.msg.sender != currentContract;
+            require e2.msg.sender != currentContract, "Caller must not be the pool contract for external transfer calls";
         }
     }
 
@@ -147,12 +146,12 @@ invariant allowanceOfPoolAlwaysZero(address a)
     {
         // This preserved is safe because we know the code in the pool contract.
         preserved _.approve(address spender, uint256 amount) with (env e1) {
-            require e1.msg.sender != _pool;
+            require e1.msg.sender != _pool, "Sender must not be the pool contract for approve calls";
         }
 
         // This preserved is safe because we know the code in the pool contract.
         preserved _.increaseAllowance(address spender, uint256 addedValue) with (env e2) {
-            require e2.msg.sender != _pool;
+            require e2.msg.sender != _pool, "Sender must not be the pool contract for increaseAllowance calls";
         }
     }
 
@@ -203,11 +202,11 @@ rule monotonicityOfMint(uint256 x, uint256 y, address recipient) {
     env eM;
     setup(eM);
     address token;
-    require token == _token0 || token == _token1;
+    require token == _token0 || token == _token1, "Token must be either token0 or token1";
     requireInvariant integrityOfTotalSupply();
     storage init = lastStorage;
-    require recipient != currentContract;
-    require x > y ;
+    require recipient != currentContract, "Recipient must not be the pool contract to properly test external balance changes";
+    require x > y, "First amount must be greater than second amount to test monotonicity";
     token.transfer(eT0, currentContract, x);
     uint256 amountOut0 = mint(eM,recipient);
     uint256 balanceAfter1 = currentContract._balances[recipient];
@@ -261,12 +260,12 @@ rule possibleToFullyWithdraw(address sender, uint256 amount) {
     env eM;
     setup(eM);
     address token;
-    require token == _token0 || token == _token1;
+    require token == _token0 || token == _token1, "Token must be either token0 or token1";
     uint256 balanceBefore = token.balanceOf(eT0,sender);
     
-    require eM.msg.sender == sender;
-    require eT0.msg.sender == sender;
-    require amount > 0;
+    require eM.msg.sender == sender, "Message sender must be the same as the user to perform withdrawal";
+    require eT0.msg.sender == sender, "Message sender must be the same as the user to perform transfer";
+    require amount > 0, "Amount must be positive to test meaningful deposit and withdrawal";
     token.transfer(eT0, currentContract, amount);
     uint256 amountOut0 = mint(eM,sender);
     // immediately withdraw 
@@ -289,7 +288,7 @@ rule zeroWithdrawNoEffect(address to) {
     env e;
     setup(e);
     // The assumption is  no skimming 
-    require currentContract.reserve0 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract);
+    require currentContract.reserve0 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract), "Reserves must match balances to ensure no skimming has occurred";
     storage before = lastStorage;
     burnSingle(e, _token0, 0, to);
     storage after = lastStorage;
diff --git a/DEFI/ConstantProductPool/runFixed.conf b/DEFI/ConstantProductPool/runFixed.conf
index da1b632b..975c0bc8 100644
--- a/DEFI/ConstantProductPool/runFixed.conf
+++ b/DEFI/ConstantProductPool/runFixed.conf
@@ -12,6 +12,7 @@
   "optimistic_loop": true,
   // msg to recognize this run (presented in your list of jobs under prover.cerotra.com)
   "msg": "CVLExmaple: ConstantProductPool fixed version",
-  "rule_sanity": "basic"
+  "rule_sanity": "basic",
+  "enforce_require_reason": true
 }
 // alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --send_only --msg "CVLExmaple: ConstantProductPool fixed version"`
\ No newline at end of file