diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
index 3c9491b..761c3b0 100644
--- a/.devcontainer/Dockerfile
+++ b/.devcontainer/Dockerfile
@@ -85,7 +85,7 @@ ENV CARGO_HOME=/usr/local/cargo
 ENV KANI_HOME=/usr/local/kani
 ENV PATH="/usr/local/cargo/bin:${PATH}"
 
-ARG RUST_VERSION=1.90.0
+ARG RUST_VERSION=1.93.1
 RUN --mount=type=cache,target=/usr/local/cargo/registry \
 	curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \
 	| sh -s -- -y --no-modify-path --default-toolchain ${RUST_VERSION} && \
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 1269dcc..89b2ba7 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -5,8 +5,7 @@
 		"dockerfile": "Dockerfile",
 		"context": "..",
 		"cacheFrom": [
-			"ghcr.io/osirisrtos/osiris/devcontainer:main",
-			"ghcr.io/osirisrtos/osiris/devcontainer:main-cache"
+			"ghcr.io/osirisrtos/osiris/devcontainer",
 		]
 	},
 	"privileged": false,
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b57322c..96f89e9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -39,7 +39,7 @@ jobs:
         id: set_output
         run: |
           REPO=$(echo "${GITHUB_REPOSITORY}" | tr '[:upper:]' '[:lower:]')
-          CONTAINER_NAME="ghcr.io/${REPO}/devcontainer:main"
+          CONTAINER_NAME="ghcr.io/${REPO}/devcontainer:latest"
           echo "container_name=$CONTAINER_NAME" >> $GITHUB_OUTPUT
           echo "container_without_tag=ghcr.io/${REPO}/devcontainer" >> $GITHUB_OUTPUT
 
diff --git a/interface/src/lib.rs b/interface/src/lib.rs
index 1a334a8..ad78f0a 100644
--- a/interface/src/lib.rs
+++ b/interface/src/lib.rs
@@ -17,6 +17,28 @@ pub struct MemMapEntry {
     pub ty: u32,
 }
 
+#[cfg(kani)]
+impl kani::Arbitrary for MemMapEntry {
+    fn any() -> Self {
+        let size: u32 = kani::any_where(|&x| x % size_of::<MemMapEntry>() as u32 == 0);
+        let length = kani::any();
+        let addr = kani::any();
+
+        kani::assume(addr > 0);
+
+        MemMapEntry {
+            size,
+            addr,
+            length,
+            ty: kani::any(),
+        }
+    }
+
+    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
+        [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
+    }
+}
+
 #[repr(C)]
 #[derive(Debug, Clone, Copy, bytemuck::Pod, bytemuck::Zeroable)]
 pub struct InitDescriptor {
diff --git a/src/mem.rs b/src/mem.rs
index b1ec789..e38b3a2 100644
--- a/src/mem.rs
+++ b/src/mem.rs
@@ -95,35 +95,10 @@ pub fn align_up(size: usize) -> usize {
 // VERIFICATION -------------------------------------------------------------------------------------------------------
 #[cfg(kani)]
 mod verification {
-    use crate::MemMapEntry;
+    use crate::mem::alloc::MAX_ADDR;
 
     use super::*;
-    use kani::Arbitrary;
-
-    impl Arbitrary for MemMapEntry {
-        fn any() -> Self {
-            let size = size_of::<MemMapEntry>() as u32;
-            let length = kani::any();
-            let addr = kani::any();
-
-            kani::assume(
-                length < alloc::MAX_ADDR as u64
-                    && length > alloc::BestFitAllocator::MIN_RANGE_SIZE as u64,
-            );
-            kani::assume(addr < alloc::MAX_ADDR as u64 - length && addr > 0);
-
-            MemMapEntry {
-                size,
-                addr,
-                length,
-                ty: kani::any(),
-            }
-        }
-
-        fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
-            [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
-        }
-    }
+    use interface::{Args, InitDescriptor, MemMapEntry};
 
     fn mock_ptr_write<T>(dst: *mut T, src: T) {
         // Just a noop
@@ -135,6 +110,7 @@ mod verification {
         let mmap: [MemMapEntry; _] = kani::any();
 
         kani::assume(mmap.len() > 0 && mmap.len() <= 8);
+        // Apply constraints to all
         for entry in mmap.iter() {
             // Ensure aligned.
             kani::assume(entry.addr % align_of::<u128>() as u64 == 0);
@@ -142,6 +118,14 @@ mod verification {
             kani::assume(entry.addr > 0);
             kani::assume(entry.length > 0);
 
+            kani::assume(
+                entry.length < alloc::MAX_ADDR as u64
+                    && entry.length > alloc::BestFitAllocator::MIN_RANGE_SIZE as u64,
+            );
+            kani::assume(entry.addr < alloc::MAX_ADDR as u64 - entry.length && entry.addr > 0);
+        }
+
+        for entry in mmap.iter() {
             // Ensure non overlapping entries
             for other in mmap.iter() {
                 if entry.addr != other.addr {
@@ -153,13 +137,20 @@ mod verification {
             }
         }
 
-        let mmap_len = mmap.len();
+        let mmap_len = mmap.len() as u64;
 
         let boot_info = BootInfo {
-            implementer: core::ptr::null(),
-            variant: core::ptr::null(),
+            magic: interface::BOOT_INFO_MAGIC,
+            version: kani::any(),
             mmap,
             mmap_len,
+            args: Args {
+                init: InitDescriptor {
+                    begin: kani::any(),
+                    len: kani::any(),
+                    entry_offset: kani::any(),
+                },
+            },
         };
 
         assert!(init_memory(&boot_info).is_ok());
diff --git a/src/mem/alloc.rs b/src/mem/alloc.rs
index d02c2fd..710ad03 100644
--- a/src/mem/alloc.rs
+++ b/src/mem/alloc.rs
@@ -45,6 +45,7 @@ pub struct BestFitAllocator {
 
 /// Implementation of the BestFitAllocator.
 impl BestFitAllocator {
+    pub const MIN_RANGE_SIZE: usize = size_of::<BestFitMeta>() + Self::align_up() + 1;
     /// Creates a new BestFitAllocator.
     ///
     /// Returns the new BestFitAllocator.