diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index 23af8ec4d8..52437a6f88 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -85,3 +85,27 @@ def List.toByteArray (bs : List UInt8) : ByteArray :=
   loop bs ByteArray.empty
 
 instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
+
+/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
+def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 7).toUInt64 <<< 0x38 |||
+  (bs.get! 6).toUInt64 <<< 0x30 |||
+  (bs.get! 5).toUInt64 <<< 0x28 |||
+  (bs.get! 4).toUInt64 <<< 0x20 |||
+  (bs.get! 3).toUInt64 <<< 0x18 |||
+  (bs.get! 2).toUInt64 <<< 0x10 |||
+  (bs.get! 1).toUInt64 <<< 0x8  |||
+  (bs.get! 0).toUInt64
diff --git a/tests/lean/bytearray.lean b/tests/lean/bytearray.lean
index 41aed42023..4baad04f20 100644
--- a/tests/lean/bytearray.lean
+++ b/tests/lean/bytearray.lean
@@ -15,3 +15,6 @@ IO.println (bs.extract 1 3);
 pure ()
 
 #eval tst
+
+#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64LE! == 0x1122334455667788
+#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64BE! == 0x8877665544332211
diff --git a/tests/lean/bytearray.lean.expected.out b/tests/lean/bytearray.lean.expected.out
index a649f0566b..2776ec93a5 100644
--- a/tests/lean/bytearray.lean.expected.out
+++ b/tests/lean/bytearray.lean.expected.out
@@ -5,3 +5,5 @@
 4
 [1, 20, 3, 4, 1, 20, 3, 4]
 [20, 3]
+true
+true