diff --git a/CHANGELOG.md b/CHANGELOG.md
index 728536a..9056f71 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,7 @@
 # Changelog
 
 ## Unreleased
+- added Kani verification harnesses for `Bytes::pop_front` and `Bytes::pop_back`
 - avoid flushing empty memory maps in `Section::freeze` to prevent macOS errors
 - derived zerocopy traits for `SectionHandle` to allow storing handles in `ByteArea` sections
 - added example demonstrating `ByteArea` with multiple typed sections, concurrent mutations, and freezing or persisting the area
diff --git a/src/bytes.rs b/src/bytes.rs
index c534b94..1a9562d 100644
--- a/src/bytes.rs
+++ b/src/bytes.rs
@@ -590,6 +590,40 @@ mod verification {
         assert_eq!(bytes.as_ref(), copy.as_ref());
     }
 
+    #[kani::proof]
+    #[kani::unwind(16)]
+    pub fn check_pop_front_behaviour() {
+        let data: Vec<u8> = Vec::bounded_any::<16>();
+        let mut bytes = Bytes::from_source(data.clone());
+        let snapshot = bytes.clone();
+
+        if let Some((expected, remainder)) = data.split_first() {
+            let popped = bytes.pop_front().expect("non-empty slice");
+            assert_eq!(popped, *expected);
+            assert_eq!(bytes.as_ref(), remainder);
+        } else {
+            assert!(bytes.pop_front().is_none());
+            assert_eq!(bytes.as_ref(), snapshot.as_ref());
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(16)]
+    pub fn check_pop_back_behaviour() {
+        let data: Vec<u8> = Vec::bounded_any::<16>();
+        let mut bytes = Bytes::from_source(data.clone());
+        let snapshot = bytes.clone();
+
+        if let Some((expected, remainder)) = data.split_last() {
+            let popped = bytes.pop_back().expect("non-empty slice");
+            assert_eq!(popped, *expected);
+            assert_eq!(bytes.as_ref(), remainder);
+        } else {
+            assert!(bytes.pop_back().is_none());
+            assert_eq!(bytes.as_ref(), snapshot.as_ref());
+        }
+    }
+
     #[kani::proof]
     #[kani::unwind(16)]
     pub fn check_slice_to_bytes_ok() {