diff --git a/examples/safeSlice.dfy b/examples/safeSlice.dfy
new file mode 100644
index 0000000..6be0eb4
--- /dev/null
+++ b/examples/safeSlice.dfy
@@ -0,0 +1,48 @@
+// Generated by lsc from safeSlice.ts
+
+function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+  ensures |SafeSlice(s, lo, hi)| <= |s|
+{
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
+}
+
+function sliceNegativeStart(): seq<int>
+{
+  SafeSlice([1, 2], -1, 2)
+}
+
+lemma sliceNegativeStart_ensures()
+  ensures (sliceNegativeStart() == [2])
+{
+}
+
+function sliceNegativeEnd(): seq<int>
+{
+  SafeSlice([1, 2], 0, -1)
+}
+
+lemma sliceNegativeEnd_ensures()
+  ensures (sliceNegativeEnd() == [1])
+{
+}
+
+function sliceNegativeBounds(): seq<int>
+{
+  SafeSlice([1, 2, 3, 4], -3, -1)
+}
+
+lemma sliceNegativeBounds_ensures()
+  ensures (sliceNegativeBounds() == [2, 3])
+{
+}
diff --git a/examples/safeSlice.dfy.gen b/examples/safeSlice.dfy.gen
new file mode 100644
index 0000000..6be0eb4
--- /dev/null
+++ b/examples/safeSlice.dfy.gen
@@ -0,0 +1,48 @@
+// Generated by lsc from safeSlice.ts
+
+function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+  ensures |SafeSlice(s, lo, hi)| <= |s|
+{
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
+}
+
+function sliceNegativeStart(): seq<int>
+{
+  SafeSlice([1, 2], -1, 2)
+}
+
+lemma sliceNegativeStart_ensures()
+  ensures (sliceNegativeStart() == [2])
+{
+}
+
+function sliceNegativeEnd(): seq<int>
+{
+  SafeSlice([1, 2], 0, -1)
+}
+
+lemma sliceNegativeEnd_ensures()
+  ensures (sliceNegativeEnd() == [1])
+{
+}
+
+function sliceNegativeBounds(): seq<int>
+{
+  SafeSlice([1, 2, 3, 4], -3, -1)
+}
+
+lemma sliceNegativeBounds_ensures()
+  ensures (sliceNegativeBounds() == [2, 3])
+{
+}
diff --git a/examples/safeSlice.ts b/examples/safeSlice.ts
new file mode 100644
index 0000000..44a6a34
--- /dev/null
+++ b/examples/safeSlice.ts
@@ -0,0 +1,21 @@
+// examples/safeSlice.ts
+
+//@ backend dafny
+//@ safe-slice
+
+
+
+function sliceNegativeStart(): number[] {
+  //@ ensures \result === [2]
+  return [1, 2].slice(-1, 2);
+}
+
+function sliceNegativeEnd(): number[] {
+  //@ ensures \result === [1]
+  return [1, 2].slice(0, -1);
+}
+
+function sliceNegativeBounds(): number[] {
+  //@ ensures \result === [2, 3]
+  return [1, 2, 3, 4].slice(-3, -1);
+}
diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts
index 8522268..9d600ed 100644
--- a/tools/src/dafny-emit.ts
+++ b/tools/src/dafny-emit.ts
@@ -1003,12 +1003,21 @@ const SEQ_JOIN = `function SeqJoin(s: seq<string>, sep: string): string
   else s[0] + sep + SeqJoin(s[1..], sep)
 }`;
 
-const SAFE_SLICE = `function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+const SAFE_SLICE = `function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
   ensures |SafeSlice(s, lo, hi)| <= |s|
 {
-  var lo' := if lo < 0 then 0 else if lo > |s| as int then |s| else lo;
-  var hi' := if hi > |s| as int then |s| else if hi < lo' then lo' else hi;
-  s[lo'..hi']
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
 }`;
 
 const STRING_INDEX_OF = `function StringIndexOf(s: string, sub: string): int