diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index eb7d66df1d7f..f8e384b5e2c1 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -47,6 +47,25 @@ def Float.lt : Float → Float → Prop := fun a b =>
 def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
+/--
+Raw transmutation from `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+-/
+@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
+
+/--
+Raw transmutation to `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+
+Note that this function is distinct from `Float.toUInt64`, which attempts
+to preserve the numeric value, and not the bitwise value.
+-/
+@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
+
 instance : Add Float := ⟨Float.add⟩
 instance : Sub Float := ⟨Float.sub⟩
 instance : Mul Float := ⟨Float.mul⟩
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 25b041650017..fb093d76df77 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -2691,6 +2691,8 @@ static inline size_t lean_float_to_usize(double a) {
     else
         return (size_t) lean_float_to_uint32(a); // NOLINT
 }
+LEAN_EXPORT double lean_float_from_bits(uint64_t u);
+LEAN_EXPORT uint64_t lean_float_to_bits(double d);
 static inline double lean_float_add(double a, double b) { return a + b; }
 static inline double lean_float_sub(double a, double b) { return a - b; }
 static inline double lean_float_mul(double a, double b) { return a * b; }
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index b23a29177d72..2634445fed9d 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1620,6 +1620,21 @@ extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
     return r;
 }
 
+extern "C" LEAN_EXPORT double lean_float_from_bits(uint64_t u)
+{
+    static_assert(sizeof(double) == sizeof(u), "`double` unexpected size.");
+    double ret;
+    std::memcpy(&ret, &u, sizeof(double));
+    return ret;
+}
+
+extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
+{
+    uint64_t ret;
+    std::memcpy(&ret, &d, sizeof(double));
+    return ret;
+}
+
 // =======================================
 // Strings
 
diff --git a/tests/lean/run/floatBits.lean b/tests/lean/run/floatBits.lean
new file mode 100644
index 000000000000..1904df8fd1ba
--- /dev/null
+++ b/tests/lean/run/floatBits.lean
@@ -0,0 +1,13 @@
+def d : Float := 1.245
+
+/--
+info: 4608285800708723180
+-/
+#guard_msgs in
+#eval d.toBits
+
+/--
+info: true
+-/
+#guard_msgs in
+#eval Float.fromBits d.toBits == d