diff --git a/Contracts/Smoke.lean b/Contracts/Smoke.lean
index ce69823c0b..6a97c53b8f 100644
--- a/Contracts/Smoke.lean
+++ b/Contracts/Smoke.lean
@@ -30,3 +30,4 @@ import Contracts.Smoke.ParetoSmallFidelityGaps
 import Contracts.Smoke.LinkedGettersAndDeferred
 import Contracts.Smoke.HopContextAndMutableTuples
 import Contracts.Smoke.LinkedRuntimeTarget
+import Contracts.Smoke.Erc20BalanceHop
diff --git a/Contracts/Smoke/Arithmetic.lean b/Contracts/Smoke/Arithmetic.lean
index bb2793bf90..102c99b10c 100644
--- a/Contracts/Smoke/Arithmetic.lean
+++ b/Contracts/Smoke/Arithmetic.lean
@@ -284,6 +284,34 @@ verity_contract Int256CheckedSmoke where
 
 #check_contract Int256CheckedSmoke
 
+-- G28 regression: an `Int256` storage read feeds the *signed* checked add in
+-- the executable plane. Before the fix `getStorage last` bound a raw `Uint256`
+-- word, so `addPanic current delta` used unsigned `addPanic` and reverted on
+-- `-1 + 25` (the words wrap mod 2^256) while Solidity `int256 +=` succeeds.
+private def okB {α : Type} : ContractResult α → Bool
+  | .success _ _ => true
+  | .revert _ _ => false
+
+private def slot0After {α : Type} : ContractResult α → Uint256
+  | .success _ s => s.readSlot 0
+  | .revert _ s => s.readSlot 0
+
+private def int256MinusOneState : ContractState :=
+  Verity.defaultState.writeSlot 0 (Verity.Core.Uint256.ofNat (2 ^ 256 - 1))
+
+example :
+    ((Int256CheckedSmoke.applyDelta (Verity.Core.Int256.ofInt 25)).run int256MinusOneState |> okB) = true := by decide +kernel
+
+example :
+    slot0After ((Int256CheckedSmoke.applyDelta (Verity.Core.Int256.ofInt 25)).run int256MinusOneState) = 24 := by decide +kernel
+
+-- Signed overflow still panics: `maxValue + 1`.
+private def int256MaxState : ContractState :=
+  Verity.defaultState.writeSlot 0 (Verity.Core.Uint256.ofNat (2 ^ 255 - 1))
+
+example :
+    ((Int256CheckedSmoke.applyDelta (Verity.Core.Int256.ofInt 1)).run int256MaxState |> okB) = false := by decide +kernel
+
 example : Int256CheckedSmoke.spec.fields.any (fun field =>
     field.name == "last" && field.slot == some 0 &&
       match field.ty with
diff --git a/Contracts/Smoke/Erc20BalanceHop.lean b/Contracts/Smoke/Erc20BalanceHop.lean
new file mode 100644
index 0000000000..e0379f3634
--- /dev/null
+++ b/Contracts/Smoke/Erc20BalanceHop.lean
@@ -0,0 +1,133 @@
+import Contracts.Common
+import Compiler.CheckContract
+
+set_option linter.unusedVariables false
+
+/-!
+# ERC-20 balance read and transfer through a linked hop (G14)
+
+A strategy-shaped contract reads `IERC20(token).balanceOf(this)` and calls
+`transfer` on a generated ERC-20 bound by `linked_contracts`. Both run the
+token's generated body at the runtime target (`hopCallView` / `hopCall`), so:
+
+* the balance read equals the token's own `balances` entry for the strategy,
+  parked at `.scoped token (.map 0 strategy)` (general theorem
+  `held_eq_token_entry`, for every state);
+* a transfer through the hop moves the token's balances, and the next balance
+  read sees the new value (kernel witnesses);
+* the strategy's own storage is untouched by the hop.
+
+This is the shape of `strategyUnderlyingBalance >= remainingReserve`
+(Pareto CLAIM-1): the left-hand side is a token-world word, not a value
+stored by the strategy.
+-/
+
+namespace Contracts.Smoke.Erc20BalanceHop
+
+open Contracts
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+verity_contract HopToken where
+  storage
+    balances : Address → Uint256 := slot 0
+
+  function view balanceOf (account : Address) : Uint256 := do
+    let b ← getMapping balances account
+    return b
+
+  function transfer (recipient : Address, amount : Uint256) : Bool := do
+    let sender ← msgSender
+    let fromBalance ← getMapping balances sender
+    require (fromBalance >= amount) "ERC20: transfer amount exceeds balance"
+    setMapping balances sender (sub fromBalance amount)
+    let toBalance ← getMapping balances recipient
+    setMapping balances recipient (add toBalance amount)
+    return true
+
+#check_contract HopToken
+
+verity_contract HopStrategy where
+  storage
+    reserve : Uint256 := slot 0
+
+  interfaces
+    interface IHopERC20 where
+      function balanceOf(Address) view returns (Uint256)
+      function transfer(Address, Uint256) returns (Bool)
+    end
+
+  linked_contracts
+    underlying : IHopERC20 := HopToken
+
+  function view held (_t : IHopERC20, _account : Address) : Uint256 := do
+    let v ← _t.balanceOf _account
+    return v
+
+  function reentrancy_trusted pay (_t : IHopERC20, _to : Address, _amount : Uint256) : Unit := do
+    let ok ← _t.transfer _to _amount
+    require ok "SafeERC20: ERC20 operation did not succeed"
+
+#check_contract HopStrategy
+
+/-- The typed view call elaborates to the token's generated body in a view hop. -/
+theorem held_is_hopCallView (t a : Address) :
+    HopStrategy.held t a = (do
+      let v ← Contract.hopCallView t (HopToken.balanceOf a)
+      return v) := rfl
+
+/-- For every state: reading `balanceOf(a)` on a distinct token returns the
+token's own parked `balances[a]` and leaves the caller's storage unchanged. -/
+theorem held_eq_token_entry (t a : Address) (s : ContractState) (h : s.thisAddress ≠ t) :
+    HopStrategy.held t a s =
+      ContractResult.success (s.storageWords (.scoped t.toNat (.map 0 a)))
+        { s with returndata := [] } := by
+  rw [held_is_hopCallView]
+  show (Contract.hopCallView t (HopToken.balanceOf a) >>= fun v => pure v) s = _
+  have hb : HopToken.balanceOf a = (do
+      let b ← getMapping HopToken.balances a
+      return b) := rfl
+  rw [hb]
+  show Verity.bind _ _ s = _
+  unfold Verity.bind
+  rw [Contract.hopCallView_of_ne t _ s h]
+  rfl
+
+def stratAddr : Address := (70 : Address)
+def tokenAddr : Address := (71 : Address)
+def userAddr : Address := (72 : Address)
+
+/-- Strategy at `stratAddr` with its own reserve 40; the token holds 100 for the
+strategy and 5 for the user in the token's namespace. -/
+def s0 : ContractState :=
+  ({ defaultState with thisAddress := stratAddr, sender := (1 : Address) }.withStorageWords fun k =>
+      if k == StorageKey.scoped tokenAddr.toNat (.map 0 stratAddr) then 100
+      else if k == StorageKey.scoped tokenAddr.toNat (.map 0 userAddr) then 5
+      else 0).writeSlot 0 40
+
+theorem held_strategy_is_100 :
+    (HopStrategy.held tokenAddr stratAddr s0).getValue? = some (100 : Uint256) := by
+  decide +kernel
+
+/-- `pay` runs the token's `transfer` with `msg.sender = strategy`. -/
+def s1 : ContractState :=
+  (HopStrategy.pay ExecutableCallContext.stub tokenAddr userAddr 30 s0).getState
+
+theorem pay_moves_token_balances :
+    s1.storageWords (.scoped tokenAddr.toNat (.map 0 stratAddr)) = 70 ∧
+    s1.storageWords (.scoped tokenAddr.toNat (.map 0 userAddr)) = 35 ∧
+    s1.readSlot 0 = 40 := by
+  decide +kernel
+
+theorem held_after_pay :
+    (HopStrategy.held tokenAddr stratAddr s1).getValue? = some (70 : Uint256) := by
+  decide +kernel
+
+/-- Over-transfer reverts inside the hop and the whole state is rolled back. -/
+theorem pay_overdraw_reverts :
+    (match HopStrategy.pay ExecutableCallContext.stub tokenAddr userAddr 101 s0 with
+      | .success _ _ => false
+      | .revert _ _ => true) = true := by
+  decide +kernel
+
+end Contracts.Smoke.Erc20BalanceHop
diff --git a/Contracts/Smoke/HashedMappings.lean b/Contracts/Smoke/HashedMappings.lean
index fac2b719e2..77604f380d 100644
--- a/Contracts/Smoke/HashedMappings.lean
+++ b/Contracts/Smoke/HashedMappings.lean
@@ -183,4 +183,29 @@ theorem hop_setRequest_frame (s : ContractState) (callee user : Address)
   exact ContractState.readMapChain_exitHop_enterHop_of_frame _ _ _ _ _ _ _
     (ContractState.storageWords_scoped_writeMapChain _ _ _ _ _ _ _)
 
+/-! ## Kernel evaluation of generated bodies (G2 residual)
+
+No executable accessor reaches keccak: nested / struct mappings live on the
+symbolic `mapChain` channel, single-key mappings on `.map` / `.mapUint` /
+`.map2`, and selectors are hashed at elaboration time. So whole generated
+bodies over hashed storage reduce in the kernel (`decide +kernel`), with no
+`native_decide` and no keccak evaluation. Only the *interpretation* layer
+(`mappingChainSlotLocation`, `solidityMappingSlot`, `@[implemented_by]`
+over a well-founded sponge) is not kernel-reducible; it is never on an
+execution path. -/
+
+private def g2User : Address := (0xabc : Address)
+
+private def g2Run : ContractResult (Uint256 × Uint256 × Uint256) :=
+  (do
+    HashedMappingExecSmoke.setRequest g2User 7 1000
+    HashedMappingExecSmoke.setReceipt g2User 55 3
+    let r ← HashedMappingExecSmoke.requestOf g2User 7
+    let other ← HashedMappingExecSmoke.requestOf g2User 8
+    let (p, e) ← HashedMappingExecSmoke.receiptOf g2User
+    return (r, other, p + e) : Contract _).run Verity.defaultState
+
+example : g2Run.getValue? = some ((1000 : Uint256), (0 : Uint256), (58 : Uint256)) := by
+  decide +kernel
+
 end Contracts.Smoke
diff --git a/Verity/Core.lean b/Verity/Core.lean
index a746468c44..f8f1aa1a34 100644
--- a/Verity/Core.lean
+++ b/Verity/Core.lean
@@ -2396,6 +2396,47 @@ def setMapping (s : StorageSlot (Address → Uint256)) (key : Address) (value :
         state.knownAddresses slot
   } := rfl
 
+/-! ### Mapping reads and writes through a distinct-address hop (G14)
+
+An ERC-20 `balanceOf(holder)` answered by a linked token body is a
+`getMapping` run inside `Contract.hopCallView token`. The callee sees its own
+mapping world (`enterHop` loads `.scoped token`), so the value read is the
+token's parked entry `.scoped token (.map slot holder)`, and the caller's
+storage is untouched. A committed mutating hop parks every plain non-slot
+write of the callee back under `.scoped callee`. -/
+
+/-- Successful distinct-address mutating hop: the result state is `exitHop`. -/
+theorem Contract.hopCall_success_of_ne {α : Type} (callee : Address) (body : Contract α)
+    (s s' : ContractState) (v : α) (h : s.thisAddress ≠ callee)
+    (hbody : body (s.enterHop s.thisAddress callee) = ContractResult.success v s') :
+    Contract.hopCall callee body s =
+      ContractResult.success v (s.exitHop s' s.thisAddress callee) := by
+  rw [Contract.hopCall_of_ne callee body s h, hbody]
+
+/-- After a successful distinct-address hop, the callee's parked word for any
+plain non-slot key (`.map`, `.map2`, `.mapUint`, `.mapChain`, `.addr`, ...) is
+the value that key had at the end of the callee body. -/
+theorem Contract.hopCall_scoped_callee {α : Type} (callee : Address) (body : Contract α)
+    (s s' : ContractState) (v : α) (h : s.thisAddress ≠ callee)
+    (hbody : body (s.enterHop s.thisAddress callee) = ContractResult.success v s')
+    (k : StorageKey) (hk : k.isPlainNonSlot = true) :
+    ((Contract.hopCall callee body s).getState).storageWords (.scoped callee.toNat k) =
+      s'.storageWords k := by
+  rw [Contract.hopCall_success_of_ne callee body s s' v h hbody]
+  exact ContractState.exitHop_scoped_callee s s' s.thisAddress callee k hk
+
+/-- `balanceOf`-shaped view hop: reading `slot[key]` inside
+`hopCallView callee` returns the callee's parked mapping entry and leaves the
+caller's state unchanged except for the cleared returndata. -/
+theorem Contract.hopCallView_getMapping (callee : Address)
+    (slot : StorageSlot (Address → Uint256)) (key : Address)
+    (s : ContractState) (h : s.thisAddress ≠ callee) :
+    Contract.hopCallView callee (getMapping slot key) s =
+      ContractResult.success (s.storageWords (.scoped callee.toNat (.map slot.slot key)))
+        { s with returndata := [] } := by
+  rw [Contract.hopCallView_of_ne callee _ s h]
+  rfl
+
 -- Typed address-valued mapping helpers on top of the word-backed storage model.
 def getMappingAddr (s : StorageSlot (Address → Uint256)) (key : Address) : Contract Address :=
   fun state => ContractResult.success (wordToAddress (state.readMap s.slot key)) state
@@ -2417,6 +2458,17 @@ def setMappingAddr (s : StorageSlot (Address → Uint256)) (key value : Address)
 def getMapping2 (s : StorageSlot (Address → Address → Uint256)) (key1 key2 : Address) : Contract Uint256 :=
   fun state => ContractResult.success (state.readMap2 s.slot key1 key2) state
 
+/-- Same as `hopCallView_getMapping` for the `getMapping2` (allowance) channel. -/
+theorem Contract.hopCallView_getMapping2 (callee : Address)
+    (slot : StorageSlot (Address → Address → Uint256)) (key1 key2 : Address)
+    (s : ContractState) (h : s.thisAddress ≠ callee) :
+    Contract.hopCallView callee (getMapping2 slot key1 key2) s =
+      ContractResult.success
+        (s.storageWords (.scoped callee.toNat (.map2 slot.slot key1 key2)))
+        { s with returndata := [] } := by
+  rw [Contract.hopCallView_of_ne callee _ s h]
+  rfl
+
 def setMapping2 (s : StorageSlot (Address → Address → Uint256)) (key1 key2 : Address) (value : Uint256) : Contract Unit :=
   fun state => ContractResult.success () (state.writeMap2 s.slot key1 key2 value)
 
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 785f7a4959..02e62b5a1b 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2258,6 +2258,16 @@ private partial def rewriteForEachExecutableDoElem
               let read ←
                 `(_root_.Verity.getPackedStorage $field:ident $(natTerm offset) $(natTerm width))
               pure (#[← `(doElem| let $name:ident ← $read:term)], locals)
+          -- `Int256` fields are stored as raw words (`StorageSlot Uint256`).
+          -- Reinterpret the word as `Int256` so that later checked arithmetic
+          -- (`addPanic cur delta`, ...) resolves to the signed instance, as in
+          -- the compilation model, instead of the unsigned one through the
+          -- `Int256 → Uint256` coercion (G28).
+          | some { ty := .scalar .int256, isTransient := false, packedBits := none, .. } =>
+              pure (#[← `(doElem| let $name:ident ← do
+                let word ← _root_.Verity.getStorage $field:ident
+                pure (_root_.Verity.Core.Int256.ofUint256 word))],
+                locals.push (mkTypedLocal (toString name.getId) .int256))
           | _ => pure (#[elem], locals)
       | `(term| getMappingN $field:ident $keys:term) =>
           -- Transient mapping chains read the EIP-1153 channel in the
diff --git a/artifacts/macro_property_tests/PropertyHopStrategy.t.sol b/artifacts/macro_property_tests/PropertyHopStrategy.t.sol
new file mode 100644
index 0000000000..081743a274
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyHopStrategy.t.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyHopStrategyTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Erc20BalanceHop.lean
+ */
+contract PropertyHopStrategyTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("HopStrategy");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: TODO decode and assert `held` result
+    function testTODO_Held_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("held(address,address)", alice, alice));
+        require(ok, "held reverted unexpectedly");
+        assertEq(ret.length, 32, "held ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 2: pay has no unexpected revert
+    function testAuto_Pay_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("pay(address,address,uint256)", alice, alice, uint256(1)));
+        require(ok, "pay reverted unexpectedly");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyHopToken.t.sol b/artifacts/macro_property_tests/PropertyHopToken.t.sol
new file mode 100644
index 0000000000..d7ac61cd3f
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyHopToken.t.sol
@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyHopTokenTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Erc20BalanceHop.lean
+ */
+contract PropertyHopTokenTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("HopToken");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: balanceOf reads the configured mapping value
+    function testAuto_BalanceOf_ReadsConfiguredMapping() public {
+        uint256 expected = uint256(1);
+        vm.store(target, _mappingSlot(bytes32(uint256(uint160(alice))), 0), bytes32(uint256(expected)));
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("balanceOf(address)", alice));
+        require(ok, "balanceOf reverted unexpectedly");
+        assertEq(ret.length, 32, "balanceOf ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, expected, "balanceOf should decode the configured mapping value");
+    }
+    // Property 2: TODO decode and assert `transfer` result
+    function testTODO_Transfer_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("transfer(address,uint256)", alice, uint256(1)));
+        require(ok, "transfer reverted unexpectedly");
+        assertEq(ret.length, 32, "transfer ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+}
diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 2b67547992..4e723041ea 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -1,6 +1,6 @@
 {
   "codebase": {
-    "core_lines": 2813,
+    "core_lines": 2865,
     "example_contracts": 19
   },
   "proofs": {
diff --git a/docs/PARETO_MODEL_SUPPORT.md b/docs/PARETO_MODEL_SUPPORT.md
index 0bf8ad6fe7..556845132a 100644
--- a/docs/PARETO_MODEL_SUPPORT.md
+++ b/docs/PARETO_MODEL_SUPPORT.md
@@ -44,7 +44,13 @@ pattern is the bit-reinterpretation already provided by `toUint256`.
 `FieldType.int256` (one EVM word, layout-identical to `uint256`) so the
 field round-trips through `Storage.lean`, layout reports, and
 `#check_contract`. The executable slot remains a `Uint256` word; the DSL
-and compilation model keep the signed tag.
+and compilation model keep the signed tag. In the executable plane
+`let x ← getStorage f` on an unpacked persistent `Int256` field binds
+`Int256.ofUint256 word`, so later `addPanic`/`subPanic`/... resolve to the
+signed instances exactly as in the compilation model (G28: before, `x` was
+the raw `Uint256` word and `addPanic x delta` silently used the unsigned
+check through the `Int256 → Uint256` coercion, reverting on valid
+`int256 +=` with a negative operand and missing real signed overflow).
 
 **Compilation model.** Bound `let x ← addPanic a b` with `Int256`
 operands lowers to wrapping `add`/`sub`/`mul` plus an `slt`-based overflow