diff --git a/lakefile.lean b/lakefile.lean
index 687c0590..47dbaea0 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -29,12 +29,27 @@ end Tests
 
 section FFI
 
-/- Build the static lib for the Rust crate -/
+/-- Build the static lib for the Rust crate -/
 extern_lib ix_rs pkg := do
   proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
-  let name := nameToStaticLib "ix_rs"
-  let srcPath := pkg.dir / "target" / "release" / name
-  return pure srcPath
+  let libName := nameToStaticLib "ix_rs"
+  let libPath := pkg.dir / "target" / "release" / libName
+
+  -- If the static lib has changed, remove cached binaries for recompilation
+  let libBytes ← IO.FS.readBinFile libPath
+  let libHash := toString $ hash libBytes
+  let libHashPath := pkg.nativeLibDir / (libName ++ ".hash")
+  let shouldCleanBinaries ←
+    if ← pkg.binDir.pathExists then
+      if ← libHashPath.pathExists then
+        let cachedHash ← IO.FS.readFile libHashPath
+        pure $ libHash != cachedHash -- Clean up in case of hash mismatch
+      else pure true -- No hash file
+    else pure false -- No files to remove
+  if shouldCleanBinaries then IO.FS.removeDirAll pkg.binDir
+  IO.FS.writeFile libHashPath libHash
+
+  return pure libPath
 
 end FFI
 
diff --git a/src/lean/ffi.rs b/src/lean/ffi.rs
index 9abf3f0d..32baa087 100644
--- a/src/lean/ffi.rs
+++ b/src/lean/ffi.rs
@@ -9,10 +9,7 @@ extern "C" fn add_u32s(a: u32, b: u32) -> u32 {
 /// `@& ByteArray → UInt8`
 #[no_mangle]
 extern "C" fn byte_array_sum(o: &LeanSArrayObject) -> u8 {
-    o.m_data
-        .slice(o.m_size)
-        .iter()
-        .fold(0, |acc, x| x.overflowing_add(acc).0)
+    o.data().iter().fold(0, |acc, x| x.overflowing_add(acc).0)
 }
 
 /// `USize → ByteArray`
@@ -24,5 +21,5 @@ extern "C" fn byte_array_zeros(len: usize) -> *const LeanSArrayObject {
 /// `@& ByteArray → @& ByteArray → Bool`
 #[no_mangle]
 extern "C" fn byte_array_beq(a: &LeanSArrayObject, b: &LeanSArrayObject) -> bool {
-    a.slice() == b.slice()
+    a.data() == b.data()
 }
diff --git a/src/lean/sarray.rs b/src/lean/sarray.rs
index 4153d355..96537e7b 100644
--- a/src/lean/sarray.rs
+++ b/src/lean/sarray.rs
@@ -24,7 +24,8 @@ pub struct LeanSArrayObject {
 }
 
 impl LeanSArrayObject {
-    pub fn slice(&self) -> &[u8] {
+    #[inline]
+    pub fn data(&self) -> &[u8] {
         self.m_data.slice(self.m_size)
     }
 
@@ -34,7 +35,7 @@ impl LeanSArrayObject {
             size_of::<LeanSArrayObject>() + len,
             align_of::<LeanSArrayObject>(),
         )
-        .unwrap();
+        .expect("Couldn't compute the memory layout");
 
         let ptr = unsafe { alloc(layout) as *mut LeanSArrayObject };
         if ptr.is_null() {