diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index afde98e4b..a45e48254 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -251,7 +251,12 @@ Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) :=
   if to_Z y =? 0 then Fail_ Failure else
   mk_scalar ty (to_Z x / to_Z y).
 
-Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)).
+Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) :=
+  if to_Z y =? 0 then Fail_ Failure else
+  (* There can be an overflow if [x] is equal to the lower bound and [y] to [-1]:
+     the remainder is then in bounds (it is [0]) but the operation panics in Rust *)
+  if (to_Z x =? scalar_min ty) && (to_Z y =? (-1)) then Fail_ Failure else
+  mk_scalar ty (Z.rem (to_Z x) (to_Z y)).
   
 Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)).
 
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index c76fab8c1..a1cc40087 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -163,7 +163,16 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
+  if y <> 0 then
+    (* There can be an overflow if [x] is equal to the lower bound and [y] to [-1]:
+       the remainder is then in bounds (it is [0]) but the operation panics in Rust *)
+    if x = scalar_min ty && y = -1 then Fail Failure
+    else mk_scalar ty (int_rem x y)
+  else Fail Failure
+
+(* Checking consistency with Rust: [MIN % -1] panics, [MIN % 1] doesn't *)
+let _ = assert_norm(scalar_rem #I32 (-0x80000000) (-1) = Fail Failure)
+let _ = assert_norm(scalar_rem #I32 (-0x80000000) 1 = Ok 0)
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
diff --git a/backends/lean/Aeneas/Std/Scalar/CheckedOps/Rem.lean b/backends/lean/Aeneas/Std/Scalar/CheckedOps/Rem.lean
index a2717ad51..a950ee3ed 100644
--- a/backends/lean/Aeneas/Std/Scalar/CheckedOps/Rem.lean
+++ b/backends/lean/Aeneas/Std/Scalar/CheckedOps/Rem.lean
@@ -58,27 +58,31 @@ Signed checked rem
 -/
 theorem core.num.checked_rem_IScalar_bv_spec {ty} (x y : IScalar ty) :
   match core.num.checked_rem_IScalar x y with
-  | some z => y.val ≠ 0 ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
-  | none => y.val = 0 := by
+  | some z => y.val ≠ 0 ∧ ¬ (x.val = IScalar.min ty ∧ y.val = -1) ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
+  | none => y.val = 0 ∨ (x.val = IScalar.min ty ∧ y.val = -1) := by
   simp [checked_rem_IScalar, Option.ofResult, IScalar.rem]
   split_ifs
   . zify at *
     simp_all
-  . rename_i hnz
+  . rename_i hnz hNoOverflow
     simp
     have hnz' : y.val ≠ 0 := by zify at *; simp_all
     have : x % y = x.rem y := by rfl
-    have ⟨ _, hz ⟩ := spec_imp_exists (@IScalar.rem_bv_spec _ x y hnz')
+    have ⟨ _, hz ⟩ := spec_imp_exists (@IScalar.rem_bv_spec _ x y hnz' (by simp; tauto))
     simp [this, IScalar.rem, hnz] at hz
+    split_ifs at hz
+    simp at hz
     simp [*]
+    tauto
+  . simp_all
 
 iscalar @[step_pure «%S».checked_rem x y]
 theorem «%S».checked_rem_bv_spec (x y : «%S») :
   match core.num.checked_rem_IScalar x y with
-  | some z => y.val ≠ 0 ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
-  | none => y.val = 0 := by
+  | some z => y.val ≠ 0 ∧ ¬ (x.val = «%S».min ∧ y.val = -1) ∧ z.val = Int.tmod x.val y.val ∧ z.bv = BitVec.srem x.bv y.bv
+  | none => y.val = 0 ∨ (x.val = «%S».min ∧ y.val = -1) := by
   have := core.num.checked_rem_IScalar_bv_spec x y
-  simp_all only [«%S».bv]
+  simp_all only [«%S».bv, IScalar.min, «%S».min, «%S».numBits]
   cases h: core.num.checked_rem_IScalar x y <;> simp_all
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
index 460262a56..1d1ff6141 100644
--- a/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
+++ b/backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean
@@ -15,7 +15,10 @@ def UScalar.rem {ty : UScalarTy} (x y : UScalar ty) : Result (UScalar ty) :=
   if y.val != 0 then ok ⟨ BitVec.umod x.bv y.bv ⟩ else fail divisionByZero
 
 def IScalar.rem {ty : IScalarTy} (x y : IScalar ty) : Result (IScalar ty) :=
-  if y.val != 0 then ok ⟨ BitVec.srem x.bv y.bv ⟩
+  if y.val != 0 then
+    -- There can be an overflow if `x` is equal to the lower bound and `y` to `-1`
+    if ¬ (x.val = IScalar.min ty && y.val = -1) then ok ⟨ BitVec.srem x.bv y.bv ⟩
+    else fail integerOverflow
   else fail divisionByZero
 
 def UScalar.try_rem {ty : UScalarTy} (x y : UScalar ty) : Option (UScalar ty) :=
@@ -62,6 +65,23 @@ namespace Tests
   #assert bv_srem (-7) 3 = -1
   #assert bv_srem 7 (-3) = 1
   #assert bv_srem (-7) (-3) = -1
+
+  -- Checking that `MIN % -1` overflows (like `MIN / -1`) while `MIN % 1` succeeds
+  #assert (IScalar.rem (I8.ofInt (-2^7)) (I8.ofInt (-1)) == fail integerOverflow)
+  #assert (IScalar.rem (I16.ofInt (-2^15)) (I16.ofInt (-1)) == fail integerOverflow)
+  #assert (IScalar.rem (I32.ofInt (-2^31)) (I32.ofInt (-1)) == fail integerOverflow)
+  #assert (IScalar.rem (I64.ofInt (-2^63)) (I64.ofInt (-1)) == fail integerOverflow)
+  #assert (IScalar.rem (I128.ofInt (-2^127)) (I128.ofInt (-1)) == fail integerOverflow)
+  #assert (IScalar.rem (I8.ofInt (-2^7)) (I8.ofInt 1) == ok (I8.ofInt 0))
+  #assert (IScalar.rem (I16.ofInt (-2^15)) (I16.ofInt 1) == ok (I16.ofInt 0))
+  #assert (IScalar.rem (I32.ofInt (-2^31)) (I32.ofInt 1) == ok (I32.ofInt 0))
+  #assert (IScalar.rem (I64.ofInt (-2^63)) (I64.ofInt 1) == ok (I64.ofInt 0))
+  #assert (IScalar.rem (I128.ofInt (-2^127)) (I128.ofInt 1) == ok (I128.ofInt 0))
+  #assert (IScalar.rem (I32.ofInt (-7)) (I32.ofInt (-1)) == ok (I32.ofInt 0))
+  #assert (IScalar.rem (I32.ofInt 7) (I32.ofInt 3) == ok (I32.ofInt 1))
+  #assert (IScalar.rem (I32.ofInt 7) (I32.ofInt 0) == fail divisionByZero)
+  #assert (UScalar.rem (U32.ofNat 7) (U32.ofNat 3) == ok (U32.ofNat 1))
+  #assert (UScalar.rem (U32.ofNat 7) (U32.ofNat 0) == fail divisionByZero)
 end Tests
 
 /-!
@@ -81,10 +101,12 @@ theorem UScalar.rem_bv_spec {ty} (x : UScalar ty) {y : UScalar ty} (hzero : y.va
   simp
 
 /-- Generic theorem - shouldn't be used much -/
-theorem IScalar.rem_bv_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0) :
+theorem IScalar.rem_bv_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0)
+  (hNoOverflow : ¬ (x.val = IScalar.min ty ∧ y.val = -1)) :
   x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ∧ z.bv = BitVec.srem x.bv y.bv ⦄ := by
   conv => arg 1; simp [HMod.hMod]
-  simp only [spec_ok, rem, bne_iff_ne, ne_eq, hzero, not_false_eq_true, ↓reduceIte]
+  simp only [spec_ok, rem, bne_iff_ne, ne_eq, hzero, not_false_eq_true, ↓reduceIte,
+    Int.reduceNeg, Bool.and_eq_true, decide_eq_true_eq, hNoOverflow]
   simp only [val]
   simp only [BitVec.toInt_srem, bv_toInt_eq, and_true]
 
@@ -93,9 +115,10 @@ uscalar theorem «%S».rem_bv_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0)
   x % y ⦃ z => (↑z : Nat) = ↑x % ↑y ∧ z.bv = x.bv % y.bv ⦄ :=
   UScalar.rem_bv_spec x hnz
 
-iscalar theorem «%S».rem_bv_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
+iscalar theorem «%S».rem_bv_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0)
+  (hNoOverflow : ¬ (x.val = «%S».min ∧ y.val = -1)) :
   x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ∧ z.bv = BitVec.srem x.bv y.bv ⦄ :=
-  IScalar.rem_bv_spec x hnz
+  IScalar.rem_bv_spec x hnz (by scalar_tac)
 
 /-!
 Theorems with a specification which only uses integers
@@ -110,10 +133,11 @@ theorem UScalar.rem_spec {ty} (x : UScalar ty) {y : UScalar ty} (hzero : y.val 
     exact h.1
 
 /-- Generic theorem - shouldn't be used much -/
-theorem IScalar.rem_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0) :
+theorem IScalar.rem_spec {ty} (x : IScalar ty) {y : IScalar ty} (hzero : y.val ≠ 0)
+  (hNoOverflow : ¬ (x.val = IScalar.min ty ∧ y.val = -1)) :
   x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ⦄ := by
   apply spec_mono
-  · apply rem_bv_spec x hzero
+  · apply rem_bv_spec x hzero hNoOverflow
   · intros x' h
     exact h.1
 
@@ -121,8 +145,9 @@ uscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val 
   x % y ⦃ z => (↑z : Nat) = ↑x % ↑y ⦄ :=
   UScalar.rem_spec x hnz
 
-iscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0) :
+iscalar @[step] theorem «%S».rem_spec (x : «%S») {y : «%S»} (hnz : y.val ≠ 0)
+  (hNoOverflow : ¬ (x.val = «%S».min ∧ y.val = -1)) :
   x % y ⦃ z => (↑z : Int) = Int.tmod ↑x ↑y ⦄ :=
-  IScalar.rem_spec x hnz
+  IScalar.rem_spec x hnz (by scalar_tac)
 
 end Aeneas.Std
diff --git a/src/interp/InterpExpressions.ml b/src/interp/InterpExpressions.ml
index fdcb23b59..ebee6dbc4 100644
--- a/src/interp/InterpExpressions.ml
+++ b/src/interp/InterpExpressions.ml
@@ -1037,8 +1037,14 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop)
                   if sv2_value = Z.zero then Error ()
                   else mk_scalar ptr_size sv1_int_ty (Z.div sv1_value sv2_value)
               | Rem OPanic ->
-                  (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
-                  if sv2_value = Z.zero then Error ()
+                  (* See [https://github.com/ocaml/Zarith/blob/master/z.mli].
+                     [MIN % -1] panics in Rust (like [MIN / -1]): the result
+                     is in bounds (it is [0]) so [mk_scalar] doesn't catch it. *)
+                  if
+                    sv2_value = Z.zero
+                    || (sv1_value = scalar_min ptr_size sv1_int_ty
+                       && sv2_value = Z.minus_one)
+                  then Error ()
                   else mk_scalar ptr_size sv1_int_ty (Z.rem sv1_value sv2_value)
               | Add OPanic ->
                   mk_scalar ptr_size sv1_int_ty (Z.add sv1_value sv2_value)