diff --git a/CHANGELOG.md b/CHANGELOG.md
index 46ab1a5..c184657 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,8 @@
 - removed the old `ByteBuffer` type in favor of `ByteArea`
 - added tests covering `ByteArea` sections, typed reserves and persistence
 - added test verifying alignment padding between differently aligned writes
+- added property tests generating random `ByteArea` sections and documented
+  multi-typed section layouts
 - split Kani verification into `verify.sh` and streamline `preflight.sh`
 - clarify that `verify.sh` runs on a dedicated system and document avoiding async code
 - install `rustfmt` and the Kani verifier automatically via `cargo install`
diff --git a/src/area.rs b/src/area.rs
index ae95a42..7dd6d61 100644
--- a/src/area.rs
+++ b/src/area.rs
@@ -13,6 +13,38 @@
 //! lifetime. Multiple sections may coexist; their byte ranges do not overlap.
 //! Freezing a section via [`Section::freeze`] remaps its range as immutable and
 //! returns [`Bytes`].
+//!
+//! # Examples
+//!
+//! ```
+//! # #[cfg(all(feature = "mmap", feature = "zerocopy"))]
+//! # {
+//! use anybytes::area::ByteArea;
+//!
+//! let mut area = ByteArea::new().unwrap();
+//! let mut sections = area.sections();
+//!
+//! let mut a = sections.reserve::<u8>(1).unwrap();
+//! a.as_mut_slice()[0] = 1;
+//!
+//! let mut b = sections.reserve::<u32>(1).unwrap();
+//! b.as_mut_slice()[0] = 2;
+//!
+//! let bytes_a = a.freeze().unwrap();
+//! let bytes_b = b.freeze().unwrap();
+//! drop(sections);
+//! let all = area.freeze().unwrap();
+//!
+//! assert_eq!(bytes_a.as_ref(), &[1]);
+//! assert_eq!(bytes_b.as_ref(), &2u32.to_ne_bytes());
+//!
+//! let mut expected = Vec::new();
+//! expected.extend_from_slice(&[1]);
+//! expected.extend_from_slice(&[0; 3]);
+//! expected.extend_from_slice(&2u32.to_ne_bytes());
+//! assert_eq!(all.as_ref(), expected.as_slice());
+//! # }
+//! ```
 
 use std::io::{self, Seek, SeekFrom};
 use std::marker::PhantomData;
diff --git a/tests/area.rs b/tests/area.rs
new file mode 100644
index 0000000..0b0ce81
--- /dev/null
+++ b/tests/area.rs
@@ -0,0 +1,75 @@
+#![cfg(all(feature = "mmap", feature = "zerocopy"))]
+
+use anybytes::area::ByteArea;
+use proptest::prelude::*;
+
+fn align_up(val: usize, align: usize) -> usize {
+    (val + align - 1) & !(align - 1)
+}
+
+#[derive(Debug, Clone)]
+enum Segment {
+    U8(Vec<u8>),
+    U16(Vec<u16>),
+    U32(Vec<u32>),
+}
+
+proptest! {
+    #![proptest_config(ProptestConfig { cases: 64, .. ProptestConfig::default() })]
+    #[test]
+    fn freeze_preserves_layout(segs in prop::collection::vec(
+        prop_oneof![
+            prop::collection::vec(any::<u8>(), 1..4).prop_map(Segment::U8),
+            prop::collection::vec(any::<u16>(), 1..4).prop_map(Segment::U16),
+            prop::collection::vec(any::<u32>(), 1..4).prop_map(Segment::U32),
+        ],
+        0..4,
+    )) {
+        let mut area = ByteArea::new().expect("area");
+        let mut sections = area.sections();
+        let mut expected: Vec<u8> = Vec::new();
+
+        for seg in segs {
+            match seg {
+                Segment::U8(data) => {
+                    let start = align_up(expected.len(), core::mem::align_of::<u8>());
+                    expected.resize(start, 0);
+                    let mut section = sections.reserve::<u8>(data.len()).expect("reserve u8");
+                    section.as_mut_slice().copy_from_slice(&data);
+                    let bytes = section.freeze().expect("freeze");
+                    expected.extend_from_slice(&data);
+                    let end = expected.len();
+                    prop_assert_eq!(bytes.as_ref(), &expected[start..end]);
+                }
+                Segment::U16(data) => {
+                    let start = align_up(expected.len(), core::mem::align_of::<u16>());
+                    expected.resize(start, 0);
+                    let mut section = sections.reserve::<u16>(data.len()).expect("reserve u16");
+                    section.as_mut_slice().copy_from_slice(&data);
+                    let bytes = section.freeze().expect("freeze");
+                    for v in &data {
+                        expected.extend_from_slice(&v.to_ne_bytes());
+                    }
+                    let end = expected.len();
+                    prop_assert_eq!(bytes.as_ref(), &expected[start..end]);
+                }
+                Segment::U32(data) => {
+                    let start = align_up(expected.len(), core::mem::align_of::<u32>());
+                    expected.resize(start, 0);
+                    let mut section = sections.reserve::<u32>(data.len()).expect("reserve u32");
+                    section.as_mut_slice().copy_from_slice(&data);
+                    let bytes = section.freeze().expect("freeze");
+                    for v in &data {
+                        expected.extend_from_slice(&v.to_ne_bytes());
+                    }
+                    let end = expected.len();
+                    prop_assert_eq!(bytes.as_ref(), &expected[start..end]);
+                }
+            }
+        }
+
+        drop(sections);
+        let all = area.freeze().expect("freeze area");
+        prop_assert_eq!(all.as_ref(), expected.as_slice());
+    }
+}