diff --git a/Cargo.lock b/Cargo.lock
index ad0c763ca..d0cc31d9e 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -919,6 +919,21 @@ dependencies = [
  "slab",
 ]
 
+[[package]]
+name = "generator"
+version = "0.8.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "52f04ae4152da20c76fe800fa48659201d5cf627c5149ca0b707b69d7eef6cf9"
+dependencies = [
+ "cc",
+ "cfg-if",
+ "libc",
+ "log",
+ "rustversion",
+ "windows-link",
+ "windows-result",
+]
+
 [[package]]
 name = "generic-array"
 version = "0.14.7"
@@ -1451,6 +1466,7 @@ dependencies = [
  "either",
  "hashbrown",
  "litebox_util_log",
+ "loom",
  "rangemap",
  "ringbuf",
  "slabmalloc",
@@ -1792,6 +1808,19 @@ dependencies = [
  "value-bag",
 ]
 
+[[package]]
+name = "loom"
+version = "0.7.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "419e0dc8046cb947daa77eb95ae174acfbddb7673b4151f56d1eed8e93fbfaca"
+dependencies = [
+ "cfg-if",
+ "generator",
+ "scoped-tls",
+ "tracing",
+ "tracing-subscriber",
+]
+
 [[package]]
 name = "managed"
 version = "0.8.0"
@@ -2515,6 +2544,12 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "scoped-tls"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e1cf6437eb19a8f4a6cc0f7dca544973b0b78843adbfeb3683d1a94a0024a294"
+
 [[package]]
 name = "scopeguard"
 version = "1.2.0"
diff --git a/litebox/Cargo.toml b/litebox/Cargo.toml
index 44c0f35c7..6bcb17529 100644
--- a/litebox/Cargo.toml
+++ b/litebox/Cargo.toml
@@ -20,6 +20,7 @@ buddy_system_allocator = { version = "0.11.0", default-features = false, feature
 # Depend on (currently unreleased) slabmalloc `main`, which contains some fixes on top of `0.11.0`
 slabmalloc = { git = "https://github.com/gz/rust-slabmalloc.git", rev = "19480b2e82704210abafe575fb9699184c1be110" }
 litebox_util_log = { version = "0.1.0", path = "../litebox_util_log" }
+loom = { version = "0.7", optional = true }
 
 [target.'cfg(windows)'.dependencies]
 windows-sys = { version = "0.60.2", features = [
@@ -34,6 +35,7 @@ windows-sys = { version = "0.60.2", features = [
 lock_tracing = ["dep:arrayvec", "spin/mutex"]
 panic_on_unclosed_fd_drop = []
 enforce_singleton_litebox_instance = []
+loom = ["dep:loom"]
 
 [lints]
 workspace = true
diff --git a/litebox/src/event/observer.rs b/litebox/src/event/observer.rs
index 42cdbd409..b6fa9cbc4 100644
--- a/litebox/src/event/observer.rs
+++ b/litebox/src/event/observer.rs
@@ -5,7 +5,11 @@
 
 use alloc::collections::btree_map::BTreeMap;
 use alloc::sync::{Arc, Weak};
+
+#[cfg(not(feature = "loom"))]
 use core::sync::atomic::{AtomicUsize, Ordering};
+#[cfg(feature = "loom")]
+use loom::sync::atomic::{AtomicUsize, Ordering};
 
 use crate::sync::{Mutex, RawSyncPrimitivesProvider};
 
diff --git a/litebox/src/event/polling.rs b/litebox/src/event/polling.rs
index 07f0170f3..eca7e5896 100644
--- a/litebox/src/event/polling.rs
+++ b/litebox/src/event/polling.rs
@@ -3,11 +3,14 @@
 
 //! Polling-related functionality
 
-use core::sync::atomic::AtomicBool;
-
 use alloc::sync::{Arc, Weak};
 use thiserror::Error;
 
+#[cfg(not(feature = "loom"))]
+use core::sync::atomic::{AtomicBool, Ordering};
+#[cfg(feature = "loom")]
+use loom::sync::atomic::{AtomicBool, Ordering};
+
 use super::{
     Events,
     observer::{Observer, Subject},
@@ -158,19 +161,99 @@ impl<Platform: RawSyncPrimitivesProvider> PolleeObserver<Platform> {
     }
 
     fn reset(&self) {
-        self.ready
-            .store(false, core::sync::atomic::Ordering::SeqCst);
+        self.ready.store(false, Ordering::SeqCst);
     }
 
     fn is_ready(&self) -> bool {
-        self.ready.load(core::sync::atomic::Ordering::SeqCst)
+        self.ready.load(Ordering::Acquire)
     }
 }
 
 impl<Platform: RawSyncPrimitivesProvider> Observer<Events> for PolleeObserver<Platform> {
     fn on_events(&self, _events: &Events) {
-        self.ready
-            .store(true, core::sync::atomic::Ordering::Release);
+        self.ready.store(true, Ordering::SeqCst);
+        #[cfg(feature = "loom")]
+        loom::sync::atomic::fence(Ordering::SeqCst);
         self.waker.wake();
     }
 }
+
+#[cfg(all(test, feature = "loom"))]
+mod loom_tests {
+    use alloc::boxed::Box;
+
+    use super::{Pollee, TryOpError};
+    use crate::event::{Events, wait::WaitState};
+    use crate::platform::loom_model::{Arc, LoomPlatform, atomic};
+
+    fn model(f: impl Fn() + Send + Sync + 'static) {
+        let mut builder = loom::model::Builder::new();
+        builder.preemption_bound = Some(1);
+        builder.check(f);
+    }
+
+    fn platform() -> &'static LoomPlatform {
+        Box::leak(Box::new(LoomPlatform::new()))
+    }
+
+    #[test]
+    fn wait_does_not_miss_notification() {
+        model(|| {
+            let pollee = Arc::new(Pollee::<LoomPlatform>::new());
+            let ready = Arc::new(loom::sync::Mutex::new(false));
+            let registered = Arc::new(atomic::AtomicBool::new(false));
+
+            let waiter = {
+                let pollee = Arc::clone(&pollee);
+                let ready = Arc::clone(&ready);
+                let registered = Arc::clone(&registered);
+                loom::thread::spawn(move || {
+                    let wait_state = WaitState::new(platform());
+                    wait_state.context().wait_on_events(
+                        false,
+                        Events::IN,
+                        |observer, filter| {
+                            pollee.register_observer(observer, filter);
+                            registered.store(true, atomic::Ordering::SeqCst);
+                            Ok(())
+                        },
+                        || {
+                            if *ready.lock().unwrap() {
+                                Ok(())
+                            } else {
+                                Err(TryOpError::<()>::TryAgain)
+                            }
+                        },
+                    )
+                })
+            };
+
+            let notifier = loom::thread::spawn(move || {
+                while !registered.load(atomic::Ordering::SeqCst) {
+                    loom::thread::yield_now();
+                }
+                *ready.lock().unwrap() = true;
+                pollee.notify_observers(Events::IN);
+            });
+
+            waiter.join().unwrap().unwrap();
+            notifier.join().unwrap();
+        });
+    }
+
+    #[test]
+    fn nonblock_does_not_register_observer() {
+        model(|| {
+            let pollee = Pollee::<LoomPlatform>::new();
+            let wait_state = WaitState::new(platform());
+
+            let result: Result<(), TryOpError<()>> =
+                pollee.wait(&wait_state.context(), true, Events::IN, || {
+                    Err(TryOpError::<()>::TryAgain)
+                });
+
+            assert!(matches!(result, Err(TryOpError::TryAgain)));
+            pollee.notify_observers(Events::IN);
+        });
+    }
+}
diff --git a/litebox/src/event/wait.rs b/litebox/src/event/wait.rs
index eb879c363..76849081b 100644
--- a/litebox/src/event/wait.rs
+++ b/litebox/src/event/wait.rs
@@ -25,6 +25,11 @@
 use alloc::sync::Arc;
 use core::{marker::PhantomData, sync::atomic::Ordering};
 
+#[cfg(not(feature = "loom"))]
+use core::sync::atomic::fence;
+#[cfg(feature = "loom")]
+use loom::sync::atomic::fence;
+
 use crate::{
     platform::{
         ImmediatelyWokenUp, Instant as _, RawMutex, ThreadProvider, TimeProvider,
@@ -83,7 +88,7 @@ impl<Platform: RawSyncPrimitivesProvider> WaitState<Platform> {
         Self {
             waker: Waker(Arc::new(WaitStateInner {
                 platform,
-                condvar: <Platform::RawMutex as RawMutex>::INIT,
+                condvar: <Platform::RawMutex as RawMutex>::new(),
             })),
             _phantom: PhantomData,
         }
@@ -110,6 +115,11 @@ impl<Platform: RawSyncPrimitivesProvider> WaitState<Platform> {
         }
     }
 
+    #[cfg(all(test, feature = "loom"))]
+    pub(crate) fn is_running_in_host_for_test(&self) -> bool {
+        self.waker.0.state_for_assert() == ThreadState::RUNNING_IN_HOST
+    }
+
     /// Sets the wait state so that [`ThreadHandle::interrupt`] will interrupt
     /// the guest execution, then calls `f` to see if the guest is still ready
     /// to run.
@@ -132,6 +142,9 @@ impl<Platform: RawSyncPrimitivesProvider> WaitState<Platform> {
         self.waker
             .0
             .set_state(ThreadState::RUNNING_IN_GUEST, Ordering::SeqCst);
+        // loom does not support SeqCst for load/store: see https://github.com/tokio-rs/loom/issues/180
+        #[cfg(feature = "loom")]
+        loom::sync::atomic::fence(Ordering::SeqCst);
         let ready_to_run_guest = f();
         if !ready_to_run_guest {
             self.waker
@@ -182,7 +195,7 @@ impl<Platform: RawSyncPrimitivesProvider> WaitStateInner<Platform> {
             Err(_) => {
                 // Provide a consistent release fence even if we didn't wake up
                 // the thread.
-                core::sync::atomic::fence(Ordering::Release);
+                fence(Ordering::Release);
             }
         }
     }
@@ -192,9 +205,13 @@ impl<Platform: RawSyncPrimitivesProvider> WaitStateInner<Platform> {
     }
 
     fn set_state(&self, new_state: ThreadState, ordering: Ordering) {
+        #[cfg(not(feature = "loom"))]
         self.condvar
             .underlying_atomic()
             .store(new_state.0, ordering);
+        // See test `relaxed_load_does_not_observe_own_relaxed_store`
+        #[cfg(feature = "loom")]
+        let _ = self.condvar.underlying_atomic().swap(new_state.0, ordering);
     }
 }
 
@@ -235,7 +252,7 @@ impl<Platform: RawSyncPrimitivesProvider + ThreadProvider> ThreadHandle<Platform
             Err(_) => {
                 // Provide a consistent release fence even if we didn't wake up
                 // the thread.
-                core::sync::atomic::fence(Ordering::Release);
+                fence(Ordering::Release);
             }
         }
     }
@@ -292,7 +309,7 @@ pub trait CheckForInterrupt {
     ///
     /// This is called by [`WaitContext::wait_until`] each time it is about to
     /// block the thread. If this returns `true`, the wait will return with
-    /// [`WaitError::Interrupted`].
+    /// [`WaitError::Interrupted`], which in turn is converted into the wait's error type.
     fn check_for_interrupt(&self) -> bool;
 }
 
@@ -378,6 +395,9 @@ impl<'a, Platform: RawSyncPrimitivesProvider + TimeProvider> WaitContext<'a, Pla
         self.waker
             .0
             .set_state(ThreadState::WAITING, Ordering::SeqCst);
+        // loom does not support SeqCst for load/store: see https://github.com/tokio-rs/loom/issues/180
+        #[cfg(feature = "loom")]
+        loom::sync::atomic::fence(Ordering::SeqCst);
     }
 
     /// Returns the thread to the running state after a wait.
diff --git a/litebox/src/platform/loom_model.rs b/litebox/src/platform/loom_model.rs
new file mode 100644
index 000000000..5a23dc84e
--- /dev/null
+++ b/litebox/src/platform/loom_model.rs
@@ -0,0 +1,536 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT license.
+
+//! Loom models for platform synchronization primitives.
+//!
+//! These types are intended for tests in this crate and dependent crates. They
+//! model platform behavior with Loom primitives, but they are not production
+//! platform implementations.
+
+use core::sync::atomic::Ordering;
+
+use alloc::collections::VecDeque;
+use alloc::vec::Vec;
+use loom::sync::Mutex;
+pub use loom::sync::{Arc, atomic};
+use loom::thread;
+
+use super::{
+    ImmediatelyWokenUp, Instant, RawAtomicU32, RawMutex, RawMutexProvider, RawPointerProvider,
+    SystemTime, TimeProvider, UnblockedOrTimedOut,
+};
+
+/// A Loom model of a futex word and its wait queue.
+///
+/// `block` models `FUTEX_WAIT`: while holding the internal queue lock, it checks
+/// whether the word still equals the expected value and only then parks on the
+/// condition variable. `wake_many` holds the same queue lock while selecting and
+/// notifying waiters, so a wake cannot be lost between the value check and the
+/// wait operation.
+pub struct LoomFutex {
+    word: RawAtomicU32,
+    queue: Mutex<WaitQueue>,
+}
+
+#[derive(Default)]
+struct WaitQueue {
+    waiters: VecDeque<Arc<Waiter>>,
+}
+
+struct Waiter {
+    thread: thread::Thread,
+    woken: atomic::AtomicBool,
+}
+
+impl LoomFutex {
+    /// Creates a new futex model with the given initial word value.
+    pub fn new(value: u32) -> Self {
+        Self {
+            word: atomic::AtomicU32::new(value),
+            queue: Mutex::new(WaitQueue::default()),
+        }
+    }
+
+    /// Returns the modeled futex word.
+    pub fn word(&self) -> &atomic::AtomicU32 {
+        &self.word
+    }
+
+    /// Wakes up to `n` waiters blocked on this futex.
+    ///
+    /// The returned value is the number of waiters selected for wakeup. This
+    /// mirrors futex semantics: selected waiters are no longer eligible for a
+    /// second wake, even if they have not yet resumed execution.
+    ///
+    /// # Panics
+    ///
+    /// Panics if Loom reports that the modeled wait-queue mutex has been
+    /// poisoned.
+    pub fn wake_many(&self, n: usize) -> usize {
+        let mut queue = self.queue.lock().unwrap();
+        let to_wake = queue.waiters.len().min(n);
+        let waiters: Vec<_> = (0..to_wake)
+            .filter_map(|_| queue.waiters.pop_front())
+            .collect();
+        drop(queue);
+
+        for waiter in waiters {
+            waiter.woken.store(true, Ordering::Release);
+            waiter.thread.unpark();
+        }
+
+        to_wake
+    }
+
+    /// Wakes one waiter blocked on this futex.
+    pub fn wake_one(&self) -> bool {
+        self.wake_many(1) > 0
+    }
+
+    /// Wakes all currently eligible waiters blocked on this futex.
+    pub fn wake_all(&self) -> usize {
+        self.wake_many(usize::MAX)
+    }
+
+    /// Blocks if the futex word is still equal to `expected`.
+    ///
+    /// This returns after a wake operation selects this waiter. A wake does not
+    /// imply that the futex word has changed; callers must re-check their own
+    /// synchronization state, just as they would around a real futex wait.
+    ///
+    /// # Panics
+    ///
+    /// Panics if Loom reports that the modeled wait-queue mutex or condition
+    /// variable has been poisoned.
+    pub fn block(&self, expected: u32) -> Result<(), ImmediatelyWokenUp> {
+        let waiter = Arc::new(Waiter {
+            thread: thread::current(),
+            woken: atomic::AtomicBool::new(false),
+        });
+
+        let mut queue = self.queue.lock().unwrap();
+        let value = self.word.load(Ordering::SeqCst);
+        if value != expected {
+            return Err(ImmediatelyWokenUp);
+        }
+        queue.waiters.push_back(Arc::clone(&waiter));
+        drop(queue);
+
+        while !waiter.woken.load(Ordering::Acquire) {
+            thread::park();
+        }
+        Ok(())
+    }
+
+    /// Blocks like [`Self::block`].
+    ///
+    /// Loom's condition variable does not model timeouts, so this returns
+    /// `Unblocked` after a modeled wake and never produces `TimedOut`.
+    ///
+    /// # Panics
+    ///
+    /// Panics under the same conditions as [`Self::block`].
+    pub fn block_or_timeout(
+        &self,
+        expected: u32,
+        _timeout: core::time::Duration,
+    ) -> Result<UnblockedOrTimedOut, ImmediatelyWokenUp> {
+        self.block(expected)
+            .map(|()| UnblockedOrTimedOut::Unblocked)
+    }
+}
+
+/// A [`RawMutex`] implementation backed by [`LoomFutex`].
+pub struct LoomRawMutex {
+    futex: LoomFutex,
+}
+
+impl LoomRawMutex {
+    /// Creates a new Loom raw mutex.
+    pub fn new() -> Self {
+        Self {
+            futex: LoomFutex::new(0),
+        }
+    }
+}
+
+impl Default for LoomRawMutex {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+impl RawMutex for LoomRawMutex {
+    fn new() -> Self {
+        LoomRawMutex::new()
+    }
+
+    fn underlying_atomic(&self) -> &RawAtomicU32 {
+        self.futex.word()
+    }
+
+    fn wake_many(&self, n: usize) -> usize {
+        self.futex.wake_many(n)
+    }
+
+    fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
+        self.futex.block(val)
+    }
+
+    fn block_or_timeout(
+        &self,
+        val: u32,
+        timeout: core::time::Duration,
+    ) -> Result<UnblockedOrTimedOut, ImmediatelyWokenUp> {
+        self.futex.block_or_timeout(val, timeout)
+    }
+}
+
+/// A minimal platform for Loom tests of raw synchronization primitives.
+pub struct LoomPlatform {
+    current_time: atomic::AtomicU64,
+}
+
+impl LoomPlatform {
+    /// Creates a new Loom platform model.
+    pub fn new() -> Self {
+        Self {
+            current_time: atomic::AtomicU64::new(0),
+        }
+    }
+}
+
+impl Default for LoomPlatform {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+impl RawMutexProvider for LoomPlatform {
+    type RawMutex = LoomRawMutex;
+}
+
+impl RawPointerProvider for LoomPlatform {
+    type RawConstPointer<T: zerocopy::FromBytes> = super::trivial_providers::TransparentConstPtr<T>;
+    type RawMutPointer<T: zerocopy::FromBytes + zerocopy::IntoBytes> =
+        super::trivial_providers::TransparentMutPtr<T>;
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
+pub struct LoomInstant {
+    time: u64,
+}
+
+impl Instant for LoomInstant {
+    fn checked_duration_since(&self, earlier: &Self) -> Option<core::time::Duration> {
+        if earlier.time <= self.time {
+            Some(core::time::Duration::from_millis(self.time - earlier.time))
+        } else {
+            None
+        }
+    }
+
+    fn checked_add(&self, duration: core::time::Duration) -> Option<Self> {
+        let duration_millis: u64 = duration.as_millis().try_into().ok()?;
+        Some(Self {
+            time: self.time.checked_add(duration_millis)?,
+        })
+    }
+}
+
+pub struct LoomSystemTime {
+    time: u64,
+}
+
+impl SystemTime for LoomSystemTime {
+    const UNIX_EPOCH: Self = Self { time: 0 };
+
+    fn duration_since(&self, earlier: &Self) -> Result<core::time::Duration, core::time::Duration> {
+        match self.time.cmp(&earlier.time) {
+            core::cmp::Ordering::Less => {
+                Err(core::time::Duration::from_millis(earlier.time - self.time))
+            }
+            core::cmp::Ordering::Equal => Ok(core::time::Duration::from_millis(0)),
+            core::cmp::Ordering::Greater => {
+                Ok(core::time::Duration::from_millis(self.time - earlier.time))
+            }
+        }
+    }
+}
+
+impl TimeProvider for LoomPlatform {
+    type Instant = LoomInstant;
+    type SystemTime = LoomSystemTime;
+
+    fn now(&self) -> Self::Instant {
+        LoomInstant {
+            time: self.current_time.fetch_add(1, Ordering::SeqCst),
+        }
+    }
+
+    fn current_time(&self) -> Self::SystemTime {
+        LoomSystemTime {
+            time: self.current_time.load(Ordering::SeqCst),
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    extern crate std;
+
+    use core::sync::atomic::Ordering;
+
+    use super::{Arc, LoomFutex, Waiter, atomic};
+    use crate::platform::{ImmediatelyWokenUp, UnblockedOrTimedOut};
+
+    macro_rules! loom_trace {
+        ($($arg:tt)*) => {{
+            std::eprintln!("[{:?}] {}", loom::thread::current().id(), format_args!($($arg)*));
+        }};
+    }
+
+    fn waiter() -> Arc<Waiter> {
+        Arc::new(Waiter {
+            thread: loom::thread::current(),
+            woken: atomic::AtomicBool::new(false),
+        })
+    }
+
+    #[test]
+    fn block_returns_immediately_when_word_mismatches() {
+        loom::model(|| {
+            let futex = LoomFutex::new(1);
+
+            match futex.block(0) {
+                Err(ImmediatelyWokenUp) => {}
+                Ok(()) => panic!("futex wait should not block when the word already differs"),
+            }
+        });
+    }
+
+    #[test]
+    fn block_or_timeout_returns_immediately_when_word_mismatches() {
+        loom::model(|| {
+            let futex = LoomFutex::new(1);
+
+            match futex.block_or_timeout(0, core::time::Duration::from_secs(1)) {
+                Err(ImmediatelyWokenUp) => {}
+                Ok(UnblockedOrTimedOut::Unblocked) => {
+                    panic!("futex wait should not consume a wake when the word already differs")
+                }
+                Ok(UnblockedOrTimedOut::TimedOut) => {
+                    panic!("LoomFutex does not model timeout expiration")
+                }
+            }
+        });
+    }
+
+    #[test]
+    fn wake_many_returns_zero_without_waiters() {
+        loom::model(|| {
+            let futex = LoomFutex::new(0);
+
+            assert_eq!(futex.wake_many(1), 0);
+            assert_eq!(futex.wake_all(), 0);
+        });
+    }
+
+    #[test]
+    fn wake_one_does_not_select_the_same_waiter_twice() {
+        loom::model(|| {
+            let futex = LoomFutex::new(0);
+            let waiter = waiter();
+            futex
+                .queue
+                .lock()
+                .unwrap()
+                .waiters
+                .push_back(Arc::clone(&waiter));
+
+            assert!(futex.wake_one());
+            assert!(!futex.wake_one());
+            assert!(waiter.woken.load(Ordering::Acquire));
+            assert!(futex.queue.lock().unwrap().waiters.is_empty());
+        });
+    }
+
+    #[test]
+    fn wake_all_selects_all_eligible_waiters() {
+        loom::model(|| {
+            let futex = LoomFutex::new(0);
+            let waiters = [waiter(), waiter(), waiter()];
+            futex
+                .queue
+                .lock()
+                .unwrap()
+                .waiters
+                .extend(waiters.iter().map(Arc::clone));
+
+            assert_eq!(futex.wake_all(), 3);
+            assert!(
+                waiters
+                    .iter()
+                    .all(|waiter| waiter.woken.load(Ordering::Acquire))
+            );
+            assert!(futex.queue.lock().unwrap().waiters.is_empty());
+        });
+    }
+
+    #[test]
+    fn wait_does_not_miss_wake_between_check_and_park() {
+        loom::model(|| {
+            let futex = Arc::new(LoomFutex::new(0));
+
+            let waiter = {
+                let futex = Arc::clone(&futex);
+                loom::thread::spawn(move || {
+                    for _ in 0..2 {
+                        let _ = futex.block(0);
+                    }
+                })
+            };
+
+            let waker = {
+                let futex = Arc::clone(&futex);
+                loom::thread::spawn(move || {
+                    futex.word().store(1, Ordering::Release);
+                    futex.wake_one();
+                })
+            };
+
+            waiter.join().unwrap();
+            waker.join().unwrap();
+        });
+    }
+
+    #[test]
+    fn test_seq_cst_ordering() {
+        loom::model(|| {
+            let first = Arc::new(loom::sync::atomic::AtomicUsize::new(0));
+            let second = Arc::new(loom::sync::atomic::AtomicUsize::new(0));
+            let sum = Arc::new(loom::sync::atomic::AtomicUsize::new(0));
+
+            let writer = {
+                let first_clone = Arc::clone(&first);
+                let second_clone = Arc::clone(&second);
+                let sum_clone = Arc::clone(&sum);
+                loom::thread::spawn(move || {
+                    loom_trace!("writer: first.store(1)");
+                    first_clone.store(1, Ordering::SeqCst);
+                    // loom does not support SeqCst for load/store: see https://github.com/tokio-rs/loom/issues/180
+                    loom::sync::atomic::fence(Ordering::SeqCst);
+                    let second = second_clone.load(Ordering::SeqCst);
+                    loom_trace!("writer: second.load() = {second}");
+                    if second == 1 {
+                        loom_trace!("writer: sum.fetch_add(1)");
+                        sum_clone.fetch_add(1, Ordering::SeqCst);
+                    }
+                })
+            };
+
+            let reader = {
+                let sum_clone = Arc::clone(&sum);
+                loom::thread::spawn(move || {
+                    loom_trace!("reader: second.store(1)");
+                    second.store(1, Ordering::SeqCst);
+                    loom::sync::atomic::fence(Ordering::SeqCst);
+                    let first = first.load(Ordering::SeqCst);
+                    loom_trace!("reader: first.load() = {first}");
+                    if first == 1 {
+                        loom_trace!("reader: sum.fetch_add(1)");
+                        sum_clone.fetch_add(1, Ordering::SeqCst);
+                    }
+                })
+            };
+
+            writer.join().unwrap();
+            reader.join().unwrap();
+
+            let sum = sum.load(Ordering::SeqCst);
+            loom_trace!("main: sum.load() = {sum}");
+            assert!(sum == 1 || sum == 2);
+        });
+    }
+
+    #[test]
+    fn test_fetch_update() {
+        loom::model(|| {
+            let atomic = Arc::new(loom::sync::atomic::AtomicUsize::new(0));
+
+            let updater = {
+                let atomic = Arc::clone(&atomic);
+                loom::thread::spawn(move || {
+                    let result = atomic.fetch_update(Ordering::Release, Ordering::Acquire, |x| {
+                        if x == 0 { Some(2) } else { None }
+                    });
+                    loom_trace!("updater: fetch_update() = {result:?}");
+                })
+            };
+
+            let writer = {
+                let atomic = Arc::clone(&atomic);
+                loom::thread::spawn(move || {
+                    // `store` would fail the test while `swap` works.
+                    // Might relate to https://github.com/tokio-rs/loom/issues/254
+                    // atomic.store(1, Ordering::Relaxed);
+                    let val = atomic.swap(1, Ordering::Relaxed);
+                    loom_trace!("writer: atomic.swap(1) = {val:?}");
+                })
+            };
+
+            updater.join().unwrap();
+            writer.join().unwrap();
+
+            let val = atomic.load(Ordering::Relaxed);
+            loom_trace!("main: atomic.load() = {val:?}");
+            assert_eq!(val, 1);
+        });
+    }
+
+    /// Minimal repro of a loom modeling bug: a thread's `Relaxed` load does
+    /// not always observe its own immediately-preceding `Relaxed` store to the
+    /// same atomic when another thread's RMW has interleaved between two
+    /// earlier same-thread writes.
+    ///
+    /// Schedule explored by loom:
+    /// - T1: store(1, SeqCst); fence(SeqCst);
+    /// - T2: compare_exchange(1, 2, Release, Relaxed);
+    /// - T1: store(0, Relaxed);
+    /// - T1: load(Relaxed);
+    ///
+    /// See https://github.com/tokio-rs/loom/issues/389 for more detail.
+    #[test]
+    fn relaxed_load_does_not_observe_own_relaxed_store() {
+        loom::model(|| {
+            let v = Arc::new(atomic::AtomicU32::new(0));
+
+            let t2 = {
+                let v = Arc::clone(&v);
+                loom::thread::spawn(move || {
+                    loom_trace!("T2: compare_exchange(1, 2)");
+                    let old = v.compare_exchange(1, 2, Ordering::Release, Ordering::Relaxed);
+                    loom_trace!("T2: compare_exchange returned {old:?}");
+                })
+            };
+
+            v.store(1, Ordering::SeqCst);
+            loom::sync::atomic::fence(Ordering::SeqCst);
+            loom::thread::yield_now();
+
+            // See https://github.com/tokio-rs/loom/issues/389
+            // v.store(0, Ordering::Relaxed);
+            let _ = v.swap(0, Ordering::Relaxed);
+            let observed = v.load(Ordering::Relaxed);
+            loom_trace!("T1: final load = {observed}");
+
+            t2.join().unwrap();
+
+            assert_eq!(
+                observed, 0,
+                "T1's Relaxed load must observe its own preceding Relaxed store \
+                 of 0 (CoWR coherence); loom #180-style modeling artifact"
+            );
+        });
+    }
+}
diff --git a/litebox/src/platform/mock.rs b/litebox/src/platform/mock.rs
index 4bcb936eb..cf56a7a25 100644
--- a/litebox/src/platform/mock.rs
+++ b/litebox/src/platform/mock.rs
@@ -11,7 +11,6 @@
 // Pull in `std` for the test-only world, so that we have a nicer/easier time writing tests
 extern crate std;
 
-use core::sync::atomic::AtomicU32;
 use std::collections::VecDeque;
 use std::sync::atomic::{AtomicU64, Ordering};
 use std::sync::{Mutex, RwLock};
@@ -60,7 +59,7 @@ impl MockPlatform {
 impl Provider for MockPlatform {}
 
 pub(crate) struct MockRawMutex {
-    inner: AtomicU32,
+    inner: RawAtomicU32,
     internal_state: std::sync::RwLock<MockRawMutexInternalState>,
 }
 
@@ -70,9 +69,21 @@ struct MockRawMutexInternalState {
 }
 
 impl MockRawMutex {
+    #[cfg(not(feature = "loom"))]
     const fn new() -> Self {
         Self {
-            inner: AtomicU32::new(0),
+            inner: RawAtomicU32::new(0),
+            internal_state: std::sync::RwLock::new(MockRawMutexInternalState {
+                number_to_wake_up: 0,
+                number_blocked: 0,
+            }),
+        }
+    }
+
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        Self {
+            inner: RawAtomicU32::new(0),
             internal_state: std::sync::RwLock::new(MockRawMutexInternalState {
                 number_to_wake_up: 0,
                 number_blocked: 0,
@@ -144,9 +155,15 @@ impl MockRawMutex {
 }
 
 impl RawMutex for MockRawMutex {
+    #[cfg(not(feature = "loom"))]
     const INIT: Self = Self::new();
 
-    fn underlying_atomic(&self) -> &AtomicU32 {
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        MockRawMutex::new()
+    }
+
+    fn underlying_atomic(&self) -> &RawAtomicU32 {
         &self.inner
     }
 
diff --git a/litebox/src/platform/mod.rs b/litebox/src/platform/mod.rs
index 2a0b6a9df..656b5fe28 100644
--- a/litebox/src/platform/mod.rs
+++ b/litebox/src/platform/mod.rs
@@ -8,6 +8,8 @@
 //! other crates that implement them upon various types.
 
 pub mod common_providers;
+#[cfg(feature = "loom")]
+pub mod loom_model;
 pub mod page_mgmt;
 pub mod trivial_providers;
 
@@ -20,6 +22,11 @@ use zerocopy::{FromBytes, IntoBytes};
 
 pub use page_mgmt::PageManagementProvider;
 
+#[cfg(not(feature = "loom"))]
+pub use core::sync::atomic::AtomicU32 as RawAtomicU32;
+#[cfg(feature = "loom")]
+pub use loom::sync::atomic::AtomicU32 as RawAtomicU32;
+
 /// A provider of a platform upon which LiteBox can execute.
 ///
 /// Ideally, a [`Provider`] is zero-sized, and only exists to provide access to functionality
@@ -290,10 +297,24 @@ pub trait RawMutexProvider {
 pub trait RawMutex: Send + Sync + 'static {
     /// The initial value for a raw mutex, with an underlying atomic with a
     /// value of zero.
+    #[cfg(not(feature = "loom"))]
     const INIT: Self;
 
+    /// Creates a raw mutex with an underlying atomic value of zero.
+    #[cfg(not(feature = "loom"))]
+    fn new() -> Self
+    where
+        Self: Sized,
+    {
+        Self::INIT
+    }
+
+    /// Creates a raw mutex with an underlying atomic value of zero.
+    #[cfg(feature = "loom")]
+    fn new() -> Self;
+
     /// Returns a reference to the underlying atomic value
-    fn underlying_atomic(&self) -> &core::sync::atomic::AtomicU32;
+    fn underlying_atomic(&self) -> &RawAtomicU32;
 
     /// Wake up `n` threads blocked on on this raw mutex.
     ///
diff --git a/litebox/src/sync/condvar.rs b/litebox/src/sync/condvar.rs
index 640526a65..9c9cae3fd 100644
--- a/litebox/src/sync/condvar.rs
+++ b/litebox/src/sync/condvar.rs
@@ -15,11 +15,20 @@ pub struct Condvar<Platform: RawMutexProvider> {
 
 impl<Platform: RawMutexProvider> Condvar<Platform> {
     #[inline]
+    #[cfg(not(feature = "loom"))]
     pub(super) const fn new() -> Self {
         Self {
             futex: <Platform::RawMutex as crate::platform::RawMutex>::INIT,
         }
     }
+
+    #[inline]
+    #[cfg(feature = "loom")]
+    pub(super) fn new() -> Self {
+        Self {
+            futex: <Platform::RawMutex as crate::platform::RawMutex>::new(),
+        }
+    }
 }
 
 // NOTE(jayb): I am not pulling in any functionality from `sandbox_core` here, because it is not
diff --git a/litebox/src/sync/futex.rs b/litebox/src/sync/futex.rs
index dadbf9ba1..f9cde4197 100644
--- a/litebox/src/sync/futex.rs
+++ b/litebox/src/sync/futex.rs
@@ -13,7 +13,12 @@
 use core::hash::BuildHasher as _;
 use core::num::NonZeroU32;
 use core::pin::pin;
-use core::sync::atomic::{AtomicBool, Ordering};
+use core::sync::atomic::Ordering;
+
+#[cfg(not(feature = "loom"))]
+use core::sync::atomic::AtomicBool;
+#[cfg(feature = "loom")]
+use loom::sync::atomic::AtomicBool;
 
 use super::RawSyncPrimitivesProvider;
 use crate::event::wait::{WaitContext, WaitError, Waker};
@@ -37,7 +42,10 @@ pub struct FutexManager<Platform: RawSyncPrimitivesProvider> {
 ///
 /// FUTURE: consider making this scale with some property of the platform, such
 /// as number of CPUs.
+#[cfg(not(feature = "loom"))]
 const HASH_TABLE_ENTRIES: usize = 256;
+#[cfg(feature = "loom")]
+const HASH_TABLE_ENTRIES: usize = 4;
 
 struct FutexEntry<Platform: RawSyncPrimitivesProvider> {
     addr: usize,
@@ -105,12 +113,13 @@ impl<Platform: RawSyncPrimitivesProvider + RawPointerProvider + TimeProvider>
         // entry goes out of scope.
         entry.as_mut().insert(bucket);
 
-        // Check the value once. Do this only after inserting into the list so
-        // that we don't miss a wakeup.
+        // Check the value once. Do this only after inserting into the
+        // list so that we don't miss a wakeup.
         let value = futex_addr.read_at_offset(0).ok_or(FutexError::Fault)?;
         if value != expected_value {
             return Err(FutexError::ImmediatelyWokenBecauseValueMismatch);
         }
+
         // Only return when woken--don't reevaluate the futex word. This
         // ensures that the rate control mechanisms provided by the futex
         // interface are effective.
@@ -160,7 +169,9 @@ impl<Platform: RawSyncPrimitivesProvider + RawPointerProvider + TimeProvider>
         // Wake the waiters outside the `extract_if` closure to minimize the list's lock hold
         // time.
         for entry in entries {
-            entry.done.store(true, Ordering::Relaxed);
+            entry.done.store(true, Ordering::SeqCst);
+            #[cfg(feature = "loom")]
+            loom::sync::atomic::fence(Ordering::SeqCst);
             entry.waker.wake();
         }
         Ok(woken)
@@ -180,7 +191,7 @@ pub enum FutexError {
     Fault,
 }
 
-#[cfg(test)]
+#[cfg(all(test, not(feature = "loom")))]
 mod tests {
     extern crate std;
 
@@ -359,3 +370,385 @@ mod tests {
         assert!((1..=3).contains(&woken));
     }
 }
+
+#[cfg(all(test, feature = "loom"))]
+mod loom_tests {
+    use alloc::boxed::Box;
+    use core::marker::PhantomData;
+    use core::num::NonZeroU32;
+
+    use super::{FutexError, FutexManager};
+    use crate::event::wait::WaitState;
+    use crate::platform::loom_model::{Arc, LoomPlatform, LoomRawMutex};
+    use crate::platform::{RawConstPointer, RawMutPointer, RawMutexProvider, RawPointerProvider};
+    use crate::platform::{TimeProvider, trivial_providers};
+    use loom::sync::atomic::{AtomicU32, Ordering, fence};
+    use zerocopy::{FromBytes, IntoBytes};
+
+    fn model(f: impl Fn() + Send + Sync + 'static) {
+        let mut builder = loom::model::Builder::new();
+        builder.preemption_bound = Some(1);
+        builder.check(f);
+    }
+
+    fn platform() -> &'static FutexTestPlatform {
+        Box::leak(Box::new(FutexTestPlatform::new()))
+    }
+
+    fn futex_addr(
+        word: &Arc<AtomicU32>,
+    ) -> <FutexTestPlatform as RawPointerProvider>::RawMutPointer<u32> {
+        FutexTestMutPtr::from_atomic_u32(Arc::as_ptr(word))
+    }
+
+    struct FutexTestPlatform {
+        platform: LoomPlatform,
+    }
+
+    impl FutexTestPlatform {
+        fn new() -> Self {
+            Self {
+                platform: LoomPlatform::new(),
+            }
+        }
+    }
+
+    impl RawMutexProvider for FutexTestPlatform {
+        type RawMutex = LoomRawMutex;
+    }
+
+    impl RawPointerProvider for FutexTestPlatform {
+        type RawConstPointer<T: FromBytes> = FutexTestConstPtr<T>;
+        type RawMutPointer<T: FromBytes + IntoBytes> = FutexTestMutPtr<T>;
+    }
+
+    impl TimeProvider for FutexTestPlatform {
+        type Instant = <LoomPlatform as TimeProvider>::Instant;
+        type SystemTime = <LoomPlatform as TimeProvider>::SystemTime;
+
+        fn now(&self) -> Self::Instant {
+            self.platform.now()
+        }
+
+        fn current_time(&self) -> Self::SystemTime {
+            self.platform.current_time()
+        }
+    }
+
+    #[derive(Clone, Copy, Debug, Eq, PartialEq)]
+    #[repr(usize)]
+    enum FutexTestPtrKind {
+        Regular = 0,
+        AtomicU32 = 1,
+    }
+
+    #[derive(Clone, Copy, Debug, FromBytes, IntoBytes)]
+    #[repr(C)]
+    struct FutexTestPtrRepr {
+        kind: usize,
+        addr: usize,
+    }
+
+    impl FutexTestPtrRepr {
+        fn new(kind: FutexTestPtrKind, addr: usize) -> Self {
+            Self {
+                kind: kind as usize,
+                addr,
+            }
+        }
+
+        fn kind(&self) -> Option<FutexTestPtrKind> {
+            match self.kind {
+                kind if kind == FutexTestPtrKind::Regular as usize => {
+                    Some(FutexTestPtrKind::Regular)
+                }
+                kind if kind == FutexTestPtrKind::AtomicU32 as usize => {
+                    Some(FutexTestPtrKind::AtomicU32)
+                }
+                _ => None,
+            }
+        }
+    }
+
+    #[derive(FromBytes, IntoBytes)]
+    #[repr(transparent)]
+    struct FutexTestConstPtr<T: Sized> {
+        inner: FutexTestPtrRepr,
+        _phantom_ptr: PhantomData<*const T>,
+    }
+
+    impl<T> Clone for FutexTestConstPtr<T> {
+        fn clone(&self) -> Self {
+            *self
+        }
+    }
+
+    impl<T> Copy for FutexTestConstPtr<T> {}
+
+    impl<T> core::fmt::Debug for FutexTestConstPtr<T> {
+        fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
+            f.debug_struct("FutexTestConstPtr")
+                .field("kind", &self.inner.kind())
+                .field("addr", &self.inner.addr)
+                .finish()
+        }
+    }
+
+    impl<T: FromBytes> RawConstPointer<T> for FutexTestConstPtr<T> {
+        fn as_usize(&self) -> usize {
+            self.inner.addr
+        }
+
+        fn from_usize(addr: usize) -> Self {
+            Self {
+                inner: FutexTestPtrRepr::new(FutexTestPtrKind::Regular, addr),
+                _phantom_ptr: PhantomData,
+            }
+        }
+
+        fn read_at_offset(self, count: isize) -> Option<T> {
+            read_at_offset(self.inner, count)
+        }
+
+        fn to_owned_slice(self, len: usize) -> Option<Box<[T]>> {
+            let ptr = transparent_const_ptr(self.inner)?;
+            ptr.to_owned_slice(len)
+        }
+    }
+
+    #[derive(FromBytes, IntoBytes)]
+    #[repr(transparent)]
+    struct FutexTestMutPtr<T: Sized> {
+        inner: FutexTestPtrRepr,
+        _phantom_ptr: PhantomData<*mut T>,
+    }
+
+    impl FutexTestMutPtr<u32> {
+        fn from_atomic_u32(word: *const AtomicU32) -> Self {
+            Self {
+                inner: FutexTestPtrRepr::new(FutexTestPtrKind::AtomicU32, word as usize),
+                _phantom_ptr: PhantomData,
+            }
+        }
+    }
+
+    impl<T> Clone for FutexTestMutPtr<T> {
+        fn clone(&self) -> Self {
+            *self
+        }
+    }
+
+    impl<T> Copy for FutexTestMutPtr<T> {}
+
+    impl<T> core::fmt::Debug for FutexTestMutPtr<T> {
+        fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
+            f.debug_struct("FutexTestMutPtr")
+                .field("kind", &self.inner.kind())
+                .field("addr", &self.inner.addr)
+                .finish()
+        }
+    }
+
+    impl<T: FromBytes> RawConstPointer<T> for FutexTestMutPtr<T> {
+        fn as_usize(&self) -> usize {
+            self.inner.addr
+        }
+
+        fn from_usize(addr: usize) -> Self {
+            Self {
+                inner: FutexTestPtrRepr::new(FutexTestPtrKind::Regular, addr),
+                _phantom_ptr: PhantomData,
+            }
+        }
+
+        fn read_at_offset(self, count: isize) -> Option<T> {
+            read_at_offset(self.inner, count)
+        }
+
+        fn to_owned_slice(self, len: usize) -> Option<Box<[T]>> {
+            let ptr = transparent_const_ptr(self.inner)?;
+            ptr.to_owned_slice(len)
+        }
+    }
+
+    impl<T: FromBytes + IntoBytes> RawMutPointer<T> for FutexTestMutPtr<T> {
+        fn write_at_offset(self, count: isize, value: T) -> Option<()> {
+            if self.inner.kind()? == FutexTestPtrKind::AtomicU32 {
+                if core::mem::size_of::<T>() != core::mem::size_of::<u32>() || count != 0 {
+                    return None;
+                }
+                let ptr = self.inner.addr as *const AtomicU32;
+                if ptr.is_null() || !ptr.is_aligned() {
+                    return None;
+                }
+                let mut bytes = [0; core::mem::size_of::<u32>()];
+                let value_ptr = core::ptr::from_ref(&value).cast::<u8>();
+                // SAFETY: `value` is a valid initialized `T`, and `bytes` has exactly
+                // the same size in this branch.
+                unsafe {
+                    core::ptr::copy_nonoverlapping(value_ptr, bytes.as_mut_ptr(), bytes.len());
+                    (*ptr).store(u32::from_ne_bytes(bytes), Ordering::SeqCst);
+                }
+                Some(())
+            } else {
+                let ptr = transparent_mut_ptr(self.inner)?;
+                ptr.write_at_offset(count, value)
+            }
+        }
+
+        fn mutate_subslice_with<R>(
+            self,
+            range: impl core::ops::RangeBounds<isize>,
+            f: impl FnOnce(&mut [T]) -> R,
+        ) -> Option<R> {
+            let ptr = transparent_mut_ptr(self.inner)?;
+            #[allow(deprecated)]
+            ptr.mutate_subslice_with(range, f)
+        }
+    }
+
+    fn read_at_offset<T: FromBytes>(ptr_repr: FutexTestPtrRepr, count: isize) -> Option<T> {
+        if ptr_repr.kind()? == FutexTestPtrKind::AtomicU32 {
+            assert!(core::mem::size_of::<T>() == core::mem::size_of::<u32>() && count == 0);
+
+            let ptr = ptr_repr.addr as *const AtomicU32;
+            if ptr.is_null() || !ptr.is_aligned() {
+                return None;
+            }
+            // SAFETY: futex test pointers are created from `Arc<AtomicU32>`, and the
+            // alignment check above rejects invalid addresses for this model.
+            let value = unsafe { (*ptr).load(Ordering::SeqCst) };
+            let bytes = value.to_ne_bytes();
+            T::read_from_bytes(&bytes).ok()
+        } else {
+            let ptr = transparent_const_ptr(ptr_repr)?;
+            ptr.read_at_offset(count)
+        }
+    }
+
+    fn transparent_const_ptr<T: FromBytes>(
+        ptr_repr: FutexTestPtrRepr,
+    ) -> Option<trivial_providers::TransparentConstPtr<T>> {
+        if ptr_repr.kind()? == FutexTestPtrKind::Regular {
+            Some(trivial_providers::TransparentConstPtr::<T>::from_usize(
+                ptr_repr.addr,
+            ))
+        } else {
+            None
+        }
+    }
+
+    fn transparent_mut_ptr<T: FromBytes + IntoBytes>(
+        ptr_repr: FutexTestPtrRepr,
+    ) -> Option<trivial_providers::TransparentMutPtr<T>> {
+        if ptr_repr.kind()? == FutexTestPtrKind::Regular {
+            Some(trivial_providers::TransparentMutPtr::<T>::from_usize(
+                ptr_repr.addr,
+            ))
+        } else {
+            None
+        }
+    }
+
+    fn assert_wait_result(result: Result<(), FutexError>) {
+        match result {
+            Ok(()) | Err(FutexError::ImmediatelyWokenBecauseValueMismatch) => {}
+            Err(FutexError::NotAligned | FutexError::Fault | FutexError::WaitError(_)) => {
+                panic!("unexpected futex wait result: {result:?}")
+            }
+        }
+    }
+
+    #[test]
+    fn wait_returns_immediately_when_value_mismatches() {
+        model(|| {
+            let futex_manager = FutexManager::<FutexTestPlatform>::new();
+            let futex_word = Arc::new(AtomicU32::new(1));
+            let wait_state = WaitState::new(platform());
+
+            let result =
+                futex_manager.wait(&wait_state.context(), futex_addr(&futex_word), 0, None);
+
+            assert!(matches!(
+                result,
+                Err(FutexError::ImmediatelyWokenBecauseValueMismatch)
+            ));
+        });
+    }
+
+    #[test]
+    fn wake_without_waiters_returns_zero() {
+        model(|| {
+            let futex_manager = FutexManager::<FutexTestPlatform>::new();
+            let futex_word = Arc::new(AtomicU32::new(0));
+
+            let woken = futex_manager
+                .wake(futex_addr(&futex_word), NonZeroU32::new(1).unwrap(), None)
+                .unwrap();
+
+            assert_eq!(woken, 0);
+        });
+    }
+
+    #[test]
+    fn wait_wake_does_not_miss_registered_waiter() {
+        model(|| {
+            let futex_manager = Arc::new(FutexManager::<FutexTestPlatform>::new());
+            let futex_word = Arc::new(AtomicU32::new(0));
+
+            let waiter = {
+                let futex_manager = Arc::clone(&futex_manager);
+                let futex_word = Arc::clone(&futex_word);
+                loom::thread::spawn(move || {
+                    let wait_state = WaitState::new(platform());
+                    let result =
+                        futex_manager.wait(&wait_state.context(), futex_addr(&futex_word), 0, None);
+                    assert!(wait_state.is_running_in_host_for_test());
+                    result
+                })
+            };
+
+            let waker = loom::thread::spawn(move || {
+                let addr = futex_addr(&futex_word);
+                futex_word.store(1, Ordering::SeqCst);
+                fence(Ordering::SeqCst);
+                let woken = futex_manager
+                    .wake(addr, NonZeroU32::new(1).unwrap(), None)
+                    .unwrap();
+                assert!(woken <= 1);
+            });
+
+            assert_wait_result(waiter.join().unwrap());
+            waker.join().unwrap();
+        });
+    }
+
+    #[test]
+    fn wake_all_releases_multiple_waiters() {
+        model(|| {
+            let futex_manager = Arc::new(FutexManager::<FutexTestPlatform>::new());
+            let futex_word = Arc::new(AtomicU32::new(0));
+
+            let waiter = |futex_manager: Arc<FutexManager<FutexTestPlatform>>,
+                          futex_word: Arc<AtomicU32>| {
+                loom::thread::spawn(move || {
+                    let wait_state = WaitState::new(platform());
+                    futex_manager.wait(&wait_state.context(), futex_addr(&futex_word), 0, None)
+                })
+            };
+
+            let waiter_a = waiter(Arc::clone(&futex_manager), Arc::clone(&futex_word));
+            let waiter_b = waiter(Arc::clone(&futex_manager), Arc::clone(&futex_word));
+
+            let addr = futex_addr(&futex_word);
+            futex_word.store(1, Ordering::SeqCst);
+            let woken = futex_manager
+                .wake(addr, NonZeroU32::new(u32::MAX).unwrap(), None)
+                .unwrap();
+            assert!(woken <= 2);
+
+            assert_wait_result(waiter_a.join().unwrap());
+            assert_wait_result(waiter_b.join().unwrap());
+        });
+    }
+}
diff --git a/litebox/src/sync/mutex.rs b/litebox/src/sync/mutex.rs
index 1c0def2b3..56e512843 100644
--- a/litebox/src/sync/mutex.rs
+++ b/litebox/src/sync/mutex.rs
@@ -26,10 +26,18 @@ struct SpinEnabledRawMutex<Platform: RawSyncPrimitivesProvider> {
 impl<Platform: RawSyncPrimitivesProvider> SpinEnabledRawMutex<Platform> {
     /// Create a new [`SpinEnabledRawMutex`] from a [`RawMutex`](crate::platform::RawMutex).
     #[inline]
+    #[cfg(not(feature = "loom"))]
     const fn new(raw: Platform::RawMutex) -> Self {
         Self { raw }
     }
 
+    /// Create a new [`SpinEnabledRawMutex`] from a [`RawMutex`](crate::platform::RawMutex).
+    #[inline]
+    #[cfg(feature = "loom")]
+    fn new(raw: Platform::RawMutex) -> Self {
+        Self { raw }
+    }
+
     /// Attempts to acquire this mutex without blocking. Returns `true` if the lock was successfully
     /// acquired and `false` otherwise.
     #[inline]
@@ -194,6 +202,7 @@ impl<Platform: RawSyncPrimitivesProvider, T> Mutex<Platform, T> {
     /// Returns a new mutex wrapping the given value.
     #[inline]
     #[cfg_attr(feature = "lock_tracing", track_caller)]
+    #[cfg(not(feature = "loom"))]
     pub const fn new(val: T) -> Self {
         Self {
             raw: SpinEnabledRawMutex::new(
@@ -204,6 +213,21 @@ impl<Platform: RawSyncPrimitivesProvider, T> Mutex<Platform, T> {
             data: UnsafeCell::new(val),
         }
     }
+
+    /// Returns a new mutex wrapping the given value.
+    #[inline]
+    #[cfg_attr(feature = "lock_tracing", track_caller)]
+    #[cfg(feature = "loom")]
+    pub fn new(val: T) -> Self {
+        Self {
+            raw: SpinEnabledRawMutex::new(
+                <Platform as crate::platform::RawMutexProvider>::RawMutex::new(),
+            ),
+            #[cfg(feature = "lock_tracing")]
+            creation: super::lock_tracing::Creation::new(),
+            data: UnsafeCell::new(val),
+        }
+    }
 }
 
 // SAFETY: `Mutex<T>` inherits `Send` from `T`.
@@ -253,3 +277,75 @@ impl<Platform: RawSyncPrimitivesProvider, T: ?Sized> Drop for Mutex<Platform, T>
             .record_destruction_if_registered(LockType::Mutex, self.raw.raw.underlying_atomic());
     }
 }
+
+#[cfg(all(test, feature = "loom"))]
+mod loom_tests {
+    use loom::sync::atomic::{AtomicUsize, Ordering};
+
+    use crate::platform::loom_model::{Arc, LoomPlatform};
+
+    use super::Mutex;
+
+    fn model(f: impl Fn() + Send + Sync + 'static) {
+        let mut builder = loom::model::Builder::new();
+        builder.preemption_bound = Some(1);
+        builder.check(f);
+    }
+
+    #[test]
+    fn guards_are_exclusive() {
+        model(|| {
+            let mutex = Arc::new(Mutex::<LoomPlatform, usize>::new(0));
+            let active_guards = Arc::new(AtomicUsize::new(0));
+
+            let worker = |mutex: Arc<Mutex<LoomPlatform, usize>>,
+                          active_guards: Arc<AtomicUsize>| {
+                loom::thread::spawn(move || {
+                    let mut guard = mutex.lock();
+                    assert_eq!(active_guards.swap(1, Ordering::SeqCst), 0);
+
+                    let value = *guard;
+                    loom::thread::yield_now();
+                    *guard = value + 1;
+
+                    active_guards.store(0, Ordering::SeqCst);
+                    drop(guard);
+                })
+            };
+
+            let worker_a = worker(Arc::clone(&mutex), Arc::clone(&active_guards));
+            let worker_b = worker(Arc::clone(&mutex), Arc::clone(&active_guards));
+
+            worker_a.join().unwrap();
+            worker_b.join().unwrap();
+
+            assert_eq!(*mutex.lock(), 2);
+        });
+    }
+
+    #[test]
+    fn contended_lock_wakes_waiter() {
+        model(|| {
+            let mutex = Arc::new(Mutex::<LoomPlatform, usize>::new(0));
+
+            let holder = {
+                let mutex = Arc::clone(&mutex);
+                loom::thread::spawn(move || {
+                    let mut guard = mutex.lock();
+                    *guard += 1;
+                    loom::thread::yield_now();
+                    drop(guard);
+                })
+            };
+
+            let waiter = loom::thread::spawn(move || {
+                let mut guard = mutex.lock();
+                *guard += 1;
+                drop(guard);
+            });
+
+            holder.join().unwrap();
+            waiter.join().unwrap();
+        });
+    }
+}
diff --git a/litebox/src/sync/rwlock.rs b/litebox/src/sync/rwlock.rs
index babda7af2..6eed11bc6 100644
--- a/litebox/src/sync/rwlock.rs
+++ b/litebox/src/sync/rwlock.rs
@@ -77,6 +77,7 @@ fn has_reached_max_readers(state: u32) -> bool {
 
 impl<Platform: RawSyncPrimitivesProvider> RawRwLock<Platform> {
     #[inline]
+    #[cfg(not(feature = "loom"))]
     const fn new() -> Self {
         Self {
             state: <Platform::RawMutex as RawMutex>::INIT,
@@ -84,6 +85,15 @@ impl<Platform: RawSyncPrimitivesProvider> RawRwLock<Platform> {
         }
     }
 
+    #[inline]
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        Self {
+            state: <Platform::RawMutex as RawMutex>::new(),
+            writer_notify: <Platform::RawMutex as RawMutex>::new(),
+        }
+    }
+
     #[expect(dead_code, reason = "we may need this eventually for RwLock::try_read")]
     #[inline]
     fn try_read(&self) -> bool {
@@ -361,12 +371,18 @@ impl<Platform: RawSyncPrimitivesProvider> RawRwLock<Platform> {
     /// Spin for a while, but stop directly at the given condition.
     #[inline]
     fn spin_until(&self, f: impl Fn(u32) -> bool) -> u32 {
+        #[cfg(feature = "loom")]
+        let mut spin = 2;
+        #[cfg(not(feature = "loom"))]
         let mut spin = 100; // Chosen by fair dice roll.
         loop {
             let state = self.state.underlying_atomic().load(Relaxed);
             if f(state) || spin == 0 {
                 return state;
             }
+            #[cfg(feature = "loom")]
+            loom::thread::yield_now();
+            #[cfg(not(feature = "loom"))]
             core::hint::spin_loop();
             spin -= 1;
         }
@@ -600,6 +616,7 @@ impl<Platform: RawSyncPrimitivesProvider, T> RwLock<Platform, T> {
     /// Returns a new reader/writer lock wrapping the given value.
     #[inline]
     #[cfg_attr(feature = "lock_tracing", track_caller)]
+    #[cfg(not(feature = "loom"))]
     pub const fn new(val: T) -> Self {
         Self {
             raw: RawRwLock::new(),
@@ -608,6 +625,19 @@ impl<Platform: RawSyncPrimitivesProvider, T> RwLock<Platform, T> {
             data: UnsafeCell::new(val),
         }
     }
+
+    /// Returns a new reader/writer lock wrapping the given value.
+    #[inline]
+    #[cfg_attr(feature = "lock_tracing", track_caller)]
+    #[cfg(feature = "loom")]
+    pub fn new(val: T) -> Self {
+        Self {
+            raw: RawRwLock::new(),
+            #[cfg(feature = "lock_tracing")]
+            creation: super::lock_tracing::Creation::new(),
+            data: UnsafeCell::new(val),
+        }
+    }
 }
 
 impl<Platform: RawSyncPrimitivesProvider, T> RwLock<Platform, T> {
@@ -709,3 +739,113 @@ unsafe impl<Platform: RawSyncPrimitivesProvider, T: Send> Send for RwLock<Platfo
 // writer can transfer `T` between threads, but the `Sync` bound is necessary,
 // too, since readers on multiple threads can share `T` simultaneously.
 unsafe impl<Platform: RawSyncPrimitivesProvider, T: Send + Sync> Sync for RwLock<Platform, T> {}
+
+#[cfg(all(test, feature = "loom"))]
+mod loom_tests {
+    use loom::sync::atomic::{AtomicUsize, Ordering};
+
+    use crate::platform::loom_model::{Arc, LoomPlatform};
+
+    use super::RwLock;
+
+    fn model(f: impl Fn() + Send + Sync + 'static) {
+        let mut builder = loom::model::Builder::new();
+        builder.preemption_bound = Some(2);
+        builder.check(f);
+    }
+
+    #[test]
+    fn readers_can_share() {
+        model(|| {
+            let lock = Arc::new(RwLock::<LoomPlatform, usize>::new(0));
+            let active_readers = Arc::new(AtomicUsize::new(0));
+
+            let reader = |lock: Arc<RwLock<LoomPlatform, usize>>,
+                          active_readers: Arc<AtomicUsize>| {
+                loom::thread::spawn(move || {
+                    let guard = lock.read();
+                    let readers = active_readers.fetch_add(1, Ordering::SeqCst) + 1;
+                    assert!(readers <= 2);
+                    let value = *guard;
+                    loom::thread::yield_now();
+                    assert_eq!(*guard, value);
+                    active_readers.fetch_sub(1, Ordering::SeqCst);
+                    drop(guard);
+                })
+            };
+
+            let reader_a = reader(Arc::clone(&lock), Arc::clone(&active_readers));
+            let reader_b = reader(Arc::clone(&lock), Arc::clone(&active_readers));
+
+            reader_a.join().unwrap();
+            reader_b.join().unwrap();
+        });
+    }
+
+    #[test]
+    fn reader_and_writer_are_exclusive() {
+        model(|| {
+            let lock = Arc::new(RwLock::<LoomPlatform, usize>::new(0));
+            let active_readers = Arc::new(AtomicUsize::new(0));
+            let active_writers = Arc::new(AtomicUsize::new(0));
+
+            let reader = {
+                let lock = Arc::clone(&lock);
+                let active_readers = Arc::clone(&active_readers);
+                let active_writers = Arc::clone(&active_writers);
+                loom::thread::spawn(move || {
+                    let guard = lock.read();
+                    active_readers.fetch_add(1, Ordering::SeqCst);
+                    assert_eq!(active_writers.load(Ordering::SeqCst), 0);
+                    loom::thread::yield_now();
+                    assert_eq!(active_writers.load(Ordering::SeqCst), 0);
+                    active_readers.fetch_sub(1, Ordering::SeqCst);
+                    drop(guard);
+                })
+            };
+
+            let writer = loom::thread::spawn(move || {
+                let mut guard = lock.write();
+                assert_eq!(active_writers.swap(1, Ordering::SeqCst), 0);
+                assert_eq!(active_readers.load(Ordering::SeqCst), 0);
+                *guard += 1;
+                loom::thread::yield_now();
+                assert_eq!(active_readers.load(Ordering::SeqCst), 0);
+                active_writers.store(0, Ordering::SeqCst);
+                drop(guard);
+            });
+
+            reader.join().unwrap();
+            writer.join().unwrap();
+        });
+    }
+
+    #[test]
+    fn writers_are_exclusive() {
+        model(|| {
+            let lock = Arc::new(RwLock::<LoomPlatform, usize>::new(0));
+            let active_writers = Arc::new(AtomicUsize::new(0));
+
+            let writer = |lock: Arc<RwLock<LoomPlatform, usize>>,
+                          active_writers: Arc<AtomicUsize>| {
+                loom::thread::spawn(move || {
+                    let mut guard = lock.write();
+                    assert_eq!(active_writers.swap(1, Ordering::SeqCst), 0);
+                    let value = *guard;
+                    loom::thread::yield_now();
+                    *guard = value + 1;
+                    active_writers.store(0, Ordering::SeqCst);
+                    drop(guard);
+                })
+            };
+
+            let writer_a = writer(Arc::clone(&lock), Arc::clone(&active_writers));
+            let writer_b = writer(Arc::clone(&lock), Arc::clone(&active_writers));
+
+            writer_a.join().unwrap();
+            writer_b.join().unwrap();
+
+            assert_eq!(*lock.read(), 2);
+        });
+    }
+}
diff --git a/litebox/src/utilities/loan_list.rs b/litebox/src/utilities/loan_list.rs
index 5ca868eea..afb6f19cf 100644
--- a/litebox/src/utilities/loan_list.rs
+++ b/litebox/src/utilities/loan_list.rs
@@ -80,7 +80,7 @@ impl<'a, Platform: RawSyncPrimitivesProvider, T> LoanListEntry<'a, Platform, T>
             node: Node {
                 ptrs: UnsafeCell::new(ListPointers::new()),
                 data: EntryData {
-                    state: <Platform::RawMutex as RawMutex>::INIT,
+                    state: <Platform::RawMutex as RawMutex>::new(),
                     value,
                 },
             },
@@ -202,6 +202,9 @@ impl<Platform: RawSyncPrimitivesProvider, T> LoanList<Platform, T> {
                 }
                 EntryState::REMOVED_WAKING => {
                     // Spin until the remover finishes waking us.
+                    #[cfg(feature = "loom")]
+                    loom::thread::yield_now();
+                    #[cfg(not(feature = "loom"))]
                     core::hint::spin_loop();
                 }
                 state => panic!("invalid state waiting for entry removal: {state:?}"),
@@ -518,7 +521,7 @@ impl<T> LinkedList<T> {
     }
 }
 
-#[cfg(test)]
+#[cfg(all(test, not(feature = "loom")))]
 mod tests {
     extern crate std;
 
@@ -621,3 +624,110 @@ mod tests {
         std::println!("{removed} items removed and observed");
     }
 }
+
+#[cfg(all(test, feature = "loom"))]
+mod loom_tests {
+    use alloc::boxed::Box;
+    use core::ops::ControlFlow;
+
+    use loom::sync::atomic::{AtomicBool, Ordering};
+
+    use super::{LoanList, LoanListEntry};
+    use crate::platform::loom_model::{Arc, LoomPlatform};
+
+    fn model(f: impl Fn() + Send + Sync + 'static) {
+        let mut builder = loom::model::Builder::new();
+        builder.preemption_bound = Some(2);
+        builder.check(f);
+    }
+
+    #[test]
+    fn owner_remove_waits_for_loan_to_complete() {
+        model(|| {
+            struct Value {
+                removed: AtomicBool,
+            }
+
+            let list = Arc::new(LoanList::<LoomPlatform, Value>::new());
+            let inserted = Arc::new(AtomicBool::new(false));
+            let loaned = Arc::new(AtomicBool::new(false));
+            let owner_removed = Arc::new(AtomicBool::new(false));
+
+            let owner = {
+                let list = Arc::clone(&list);
+                let inserted = Arc::clone(&inserted);
+                let loaned = Arc::clone(&loaned);
+                let owner_removed = Arc::clone(&owner_removed);
+                loom::thread::spawn(move || {
+                    let mut entry = Box::pin(LoanListEntry::new(Value {
+                        removed: AtomicBool::new(false),
+                    }));
+                    entry.as_mut().insert(&list);
+                    inserted.store(true, Ordering::SeqCst);
+
+                    while !loaned.load(Ordering::SeqCst) {
+                        loom::thread::yield_now();
+                    }
+
+                    entry.as_mut().remove();
+                    owner_removed.store(true, Ordering::SeqCst);
+                    assert!(entry.get().removed.load(Ordering::SeqCst));
+                })
+            };
+
+            let remover = loom::thread::spawn(move || {
+                while !inserted.load(Ordering::SeqCst) {
+                    loom::thread::yield_now();
+                }
+
+                let mut items = list.extract_if(|_| ControlFlow::Continue(true));
+                let item = items.next().expect("expected loaned item");
+                assert!(items.next().is_none());
+
+                loaned.store(true, Ordering::SeqCst);
+                loom::thread::yield_now();
+                item.removed.store(true, Ordering::SeqCst);
+                drop(item);
+            });
+
+            owner.join().unwrap();
+            remover.join().unwrap();
+            assert!(owner_removed.load(Ordering::SeqCst));
+        });
+    }
+
+    #[test]
+    fn concurrent_extract_and_owner_remove() {
+        model(|| {
+            struct Value {
+                key: usize,
+            }
+
+            let list = Arc::new(LoanList::<LoomPlatform, Value>::new());
+            let mut entry1 = Box::pin(LoanListEntry::new(Value { key: 0 }));
+            let mut entry2 = Box::pin(LoanListEntry::new(Value { key: 1 }));
+
+            entry1.as_mut().insert(&list);
+            entry2.as_mut().insert(&list);
+
+            let remover = {
+                let list = Arc::clone(&list);
+                loom::thread::spawn(move || {
+                    let mut removed = 0;
+                    for item in list.extract_if(|value| ControlFlow::Continue(value.key == 0)) {
+                        assert_eq!(item.key, 0);
+                        removed += 1;
+                        loom::thread::yield_now();
+                    }
+                    assert_eq!(removed, 1);
+                })
+            };
+
+            loom::thread::yield_now();
+            entry2.as_mut().remove();
+
+            remover.join().unwrap();
+            entry1.as_mut().remove();
+        });
+    }
+}
diff --git a/litebox_platform_linux_kernel/Cargo.toml b/litebox_platform_linux_kernel/Cargo.toml
index 858cb655e..499c7657c 100644
--- a/litebox_platform_linux_kernel/Cargo.toml
+++ b/litebox_platform_linux_kernel/Cargo.toml
@@ -4,6 +4,7 @@ version = "0.1.0"
 edition = "2024"
 
 [features]
+loom = ["litebox/loom"]
 
 [build-dependencies]
 bindgen = "0.71.0"
diff --git a/litebox_platform_linux_kernel/src/lib.rs b/litebox_platform_linux_kernel/src/lib.rs
index cc207d3da..1a5fbcd39 100644
--- a/litebox_platform_linux_kernel/src/lib.rs
+++ b/litebox_platform_linux_kernel/src/lib.rs
@@ -11,10 +11,12 @@ use core::{arch::asm, sync::atomic::AtomicU32};
 
 use litebox::mm::linux::PageRange;
 use litebox::platform::RawPointerProvider;
+#[cfg(not(feature = "loom"))]
+use litebox::platform::UnblockedOrTimedOut;
 use litebox::platform::page_mgmt::FixedAddressBehavior;
 use litebox::platform::{
     IPInterfaceProvider, ImmediatelyWokenUp, PageManagementProvider, Provider, Punchthrough,
-    PunchthroughProvider, PunchthroughToken, RawMutexProvider, TimeProvider, UnblockedOrTimedOut,
+    PunchthroughProvider, PunchthroughToken, RawMutexProvider, TimeProvider,
 };
 use litebox_common_linux::PunchthroughSyscall;
 use litebox_common_linux::errno::Errno;
@@ -143,7 +145,10 @@ impl<Host: HostInterface> RawMutexProvider for LinuxKernel<Host> {
 
 /// An implementation of [`litebox::platform::RawMutex`]
 pub struct RawMutex<Host: HostInterface> {
+    #[cfg(not(feature = "loom"))]
     inner: AtomicU32,
+    #[cfg(feature = "loom")]
+    futex: litebox::platform::loom_model::LoomFutex,
     host: core::marker::PhantomData<fn(Host) -> Host>,
 }
 
@@ -151,16 +156,36 @@ unsafe impl<Host: HostInterface> Send for RawMutex<Host> {}
 unsafe impl<Host: HostInterface> Sync for RawMutex<Host> {}
 
 impl<Host: HostInterface> litebox::platform::RawMutex for RawMutex<Host> {
+    #[cfg(not(feature = "loom"))]
     const INIT: Self = Self::new();
 
-    fn underlying_atomic(&self) -> &core::sync::atomic::AtomicU32 {
-        &self.inner
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        RawMutex::new()
     }
 
+    fn underlying_atomic(&self) -> &litebox::platform::RawAtomicU32 {
+        #[cfg(feature = "loom")]
+        {
+            self.futex.word()
+        }
+        #[cfg(not(feature = "loom"))]
+        {
+            &self.inner
+        }
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn wake_many(&self, n: usize) -> usize {
         Host::wake_many(&self.inner, n).unwrap()
     }
 
+    #[cfg(feature = "loom")]
+    fn wake_many(&self, n: usize) -> usize {
+        self.futex.wake_many(n)
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
         match self.block_or_maybe_timeout(val, None) {
             Ok(UnblockedOrTimedOut::Unblocked) => Ok(()),
@@ -169,6 +194,12 @@ impl<Host: HostInterface> litebox::platform::RawMutex for RawMutex<Host> {
         }
     }
 
+    #[cfg(feature = "loom")]
+    fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
+        self.futex.block(val)
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block_or_timeout(
         &self,
         val: u32,
@@ -176,9 +207,19 @@ impl<Host: HostInterface> litebox::platform::RawMutex for RawMutex<Host> {
     ) -> Result<litebox::platform::UnblockedOrTimedOut, ImmediatelyWokenUp> {
         self.block_or_maybe_timeout(val, Some(time))
     }
+
+    #[cfg(feature = "loom")]
+    fn block_or_timeout(
+        &self,
+        val: u32,
+        time: core::time::Duration,
+    ) -> Result<litebox::platform::UnblockedOrTimedOut, ImmediatelyWokenUp> {
+        self.futex.block_or_timeout(val, time)
+    }
 }
 
 impl<Host: HostInterface> RawMutex<Host> {
+    #[cfg(not(feature = "loom"))]
     const fn new() -> Self {
         Self {
             inner: AtomicU32::new(0),
@@ -186,6 +227,15 @@ impl<Host: HostInterface> RawMutex<Host> {
         }
     }
 
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        Self {
+            futex: litebox::platform::loom_model::LoomFutex::new(0),
+            host: core::marker::PhantomData,
+        }
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block_or_maybe_timeout(
         &self,
         val: u32,
diff --git a/litebox_platform_linux_userland/Cargo.toml b/litebox_platform_linux_userland/Cargo.toml
index 1c4d96ed6..3468e9990 100644
--- a/litebox_platform_linux_userland/Cargo.toml
+++ b/litebox_platform_linux_userland/Cargo.toml
@@ -18,6 +18,7 @@ zerocopy = { version = "0.8", default-features = false }
 default = ["linux_syscall"]
 linux_syscall = []
 optee_syscall = ["dep:litebox_common_optee"]
+loom = ["litebox/loom"]
 
 [lints]
 workspace = true
diff --git a/litebox_platform_linux_userland/src/lib.rs b/litebox_platform_linux_userland/src/lib.rs
index a1ccf7fdc..7d9eee840 100644
--- a/litebox_platform_linux_userland/src/lib.rs
+++ b/litebox_platform_linux_userland/src/lib.rs
@@ -10,7 +10,9 @@
 use std::cell::Cell;
 use std::os::fd::{AsRawFd as _, FromRawFd as _};
 use std::path::PathBuf;
-use std::sync::atomic::{AtomicI32, AtomicU32, Ordering};
+#[cfg(not(feature = "loom"))]
+use std::sync::atomic::AtomicU32;
+use std::sync::atomic::{AtomicI32, Ordering};
 use std::time::Duration;
 use std::unimplemented;
 
@@ -1006,16 +1008,28 @@ impl litebox::platform::RawMutexProvider for LinuxUserland {
 
 pub struct RawMutex {
     // The `inner` is the value shown to the outside world as an underlying atomic.
+    #[cfg(not(feature = "loom"))]
     inner: AtomicU32,
+    #[cfg(feature = "loom")]
+    futex: litebox::platform::loom_model::LoomFutex,
 }
 
 impl RawMutex {
+    #[cfg(not(feature = "loom"))]
     const fn new() -> Self {
         Self {
             inner: AtomicU32::new(0),
         }
     }
 
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        Self {
+            futex: litebox::platform::loom_model::LoomFutex::new(0),
+        }
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block_or_maybe_timeout(
         &self,
         val: u32,
@@ -1041,12 +1055,26 @@ impl RawMutex {
 }
 
 impl litebox::platform::RawMutex for RawMutex {
+    #[cfg(not(feature = "loom"))]
     const INIT: Self = Self::new();
 
-    fn underlying_atomic(&self) -> &AtomicU32 {
-        &self.inner
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        RawMutex::new()
     }
 
+    fn underlying_atomic(&self) -> &litebox::platform::RawAtomicU32 {
+        #[cfg(feature = "loom")]
+        {
+            self.futex.word()
+        }
+        #[cfg(not(feature = "loom"))]
+        {
+            &self.inner
+        }
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn wake_many(&self, n: usize) -> usize {
         assert!(n > 0);
         let n: u32 = n.try_into().unwrap();
@@ -1061,6 +1089,12 @@ impl litebox::platform::RawMutex for RawMutex {
         .expect("failed to wake up waiters")
     }
 
+    #[cfg(feature = "loom")]
+    fn wake_many(&self, n: usize) -> usize {
+        self.futex.wake_many(n)
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
         match self.block_or_maybe_timeout(val, None) {
             Ok(UnblockedOrTimedOut::Unblocked) => Ok(()),
@@ -1069,6 +1103,12 @@ impl litebox::platform::RawMutex for RawMutex {
         }
     }
 
+    #[cfg(feature = "loom")]
+    fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
+        self.futex.block(val)
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block_or_timeout(
         &self,
         val: u32,
@@ -1076,6 +1116,15 @@ impl litebox::platform::RawMutex for RawMutex {
     ) -> Result<UnblockedOrTimedOut, ImmediatelyWokenUp> {
         self.block_or_maybe_timeout(val, Some(timeout))
     }
+
+    #[cfg(feature = "loom")]
+    fn block_or_timeout(
+        &self,
+        val: u32,
+        timeout: Duration,
+    ) -> Result<UnblockedOrTimedOut, ImmediatelyWokenUp> {
+        self.futex.block_or_timeout(val, timeout)
+    }
 }
 
 impl litebox::platform::IPInterfaceProvider for LinuxUserland {
@@ -1245,6 +1294,7 @@ impl litebox::platform::RawPointerProvider for LinuxUserland {
 
 /// Operations currently supported by the safer variants of the Linux futex syscall
 /// ([`futex_timeout`] and [`futex_val2`]).
+#[cfg(not(feature = "loom"))]
 #[repr(i32)]
 enum FutexOperation {
     Wait = litebox_common_linux::FUTEX_WAIT,
@@ -1252,6 +1302,7 @@ enum FutexOperation {
 }
 
 /// Safer invocation of the Linux futex syscall, with the "timeout" variant of the arguments.
+#[cfg(not(feature = "loom"))]
 #[expect(clippy::similar_names, reason = "sec/nsec are as needed by libc")]
 fn futex_timeout(
     uaddr: &AtomicU32,
@@ -1302,6 +1353,7 @@ fn futex_timeout(
 }
 
 /// Safer invocation of the Linux futex syscall, with the "val2" variant of the arguments.
+#[cfg(not(feature = "loom"))]
 fn futex_val2(
     uaddr: &AtomicU32,
     futex_op: FutexOperation,
@@ -2274,7 +2326,6 @@ impl litebox::mm::linux::VmemPageFaultHandler for LinuxUserland {
 
 #[cfg(test)]
 mod tests {
-    use core::sync::atomic::AtomicU32;
     use std::thread::sleep;
 
     use litebox::platform::RawMutex;
@@ -2286,15 +2337,13 @@ mod tests {
 
     #[test]
     fn test_raw_mutex() {
-        let mutex = std::sync::Arc::new(super::RawMutex {
-            inner: AtomicU32::new(0),
-        });
+        let mutex = std::sync::Arc::new(super::RawMutex::new());
 
         let copied_mutex = mutex.clone();
         std::thread::spawn(move || {
             sleep(core::time::Duration::from_millis(500));
             copied_mutex
-                .inner
+                .underlying_atomic()
                 .fetch_add(1, core::sync::atomic::Ordering::Relaxed);
             copied_mutex.wake_many(10);
         });
diff --git a/litebox_platform_lvbs/Cargo.toml b/litebox_platform_lvbs/Cargo.toml
index 992dc508e..2eaaf33e3 100644
--- a/litebox_platform_lvbs/Cargo.toml
+++ b/litebox_platform_lvbs/Cargo.toml
@@ -45,6 +45,7 @@ default = ["optee_syscall"]
 optee_syscall = []
 linux_syscall = []
 devbox = []
+loom = ["litebox/loom"]
 
 [lints]
 workspace = true
diff --git a/litebox_platform_lvbs/src/lib.rs b/litebox_platform_lvbs/src/lib.rs
index 56914cd75..451145a92 100644
--- a/litebox_platform_lvbs/src/lib.rs
+++ b/litebox_platform_lvbs/src/lib.rs
@@ -14,9 +14,11 @@ use core::{
 use hashbrown::HashMap;
 use litebox::platform::{
     IPInterfaceProvider, ImmediatelyWokenUp, PageManagementProvider, Punchthrough,
-    PunchthroughProvider, PunchthroughToken, RawMutex as _, RawMutexProvider, RawPointerProvider,
-    StdioProvider, TimeProvider, UnblockedOrTimedOut, page_mgmt::DeallocationError,
+    PunchthroughProvider, PunchthroughToken, RawMutexProvider, RawPointerProvider, StdioProvider,
+    TimeProvider, page_mgmt::DeallocationError,
 };
+#[cfg(not(feature = "loom"))]
+use litebox::platform::{RawMutex as _, UnblockedOrTimedOut};
 use litebox::{
     mm::linux::{PAGE_SIZE, PageRange},
     platform::page_mgmt::FixedAddressBehavior,
@@ -968,7 +970,10 @@ impl<Host: HostInterface> RawMutexProvider for LinuxKernel<Host> {
 
 /// An implementation of [`litebox::platform::RawMutex`]
 pub struct RawMutex<Host: HostInterface> {
+    #[cfg(not(feature = "loom"))]
     inner: AtomicU32,
+    #[cfg(feature = "loom")]
+    futex: litebox::platform::loom_model::LoomFutex,
     host: core::marker::PhantomData<fn(Host) -> Host>,
 }
 
@@ -977,16 +982,36 @@ unsafe impl<Host: HostInterface> Sync for RawMutex<Host> {}
 
 /// TODO: common mutex implementation could be moved to a shared crate
 impl<Host: HostInterface> litebox::platform::RawMutex for RawMutex<Host> {
+    #[cfg(not(feature = "loom"))]
     const INIT: Self = Self::new();
 
-    fn underlying_atomic(&self) -> &core::sync::atomic::AtomicU32 {
-        &self.inner
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        RawMutex::new()
     }
 
+    fn underlying_atomic(&self) -> &litebox::platform::RawAtomicU32 {
+        #[cfg(feature = "loom")]
+        {
+            self.futex.word()
+        }
+        #[cfg(not(feature = "loom"))]
+        {
+            &self.inner
+        }
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn wake_many(&self, n: usize) -> usize {
         Host::wake_many(&self.inner, n).unwrap()
     }
 
+    #[cfg(feature = "loom")]
+    fn wake_many(&self, n: usize) -> usize {
+        self.futex.wake_many(n)
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
         match self.block_or_maybe_timeout(val, None) {
             Ok(UnblockedOrTimedOut::Unblocked) => Ok(()),
@@ -995,6 +1020,12 @@ impl<Host: HostInterface> litebox::platform::RawMutex for RawMutex<Host> {
         }
     }
 
+    #[cfg(feature = "loom")]
+    fn block(&self, val: u32) -> Result<(), ImmediatelyWokenUp> {
+        self.futex.block(val)
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block_or_timeout(
         &self,
         val: u32,
@@ -1002,9 +1033,19 @@ impl<Host: HostInterface> litebox::platform::RawMutex for RawMutex<Host> {
     ) -> Result<litebox::platform::UnblockedOrTimedOut, ImmediatelyWokenUp> {
         self.block_or_maybe_timeout(val, Some(time))
     }
+
+    #[cfg(feature = "loom")]
+    fn block_or_timeout(
+        &self,
+        val: u32,
+        time: core::time::Duration,
+    ) -> Result<litebox::platform::UnblockedOrTimedOut, ImmediatelyWokenUp> {
+        self.futex.block_or_timeout(val, time)
+    }
 }
 
 impl<Host: HostInterface> RawMutex<Host> {
+    #[cfg(not(feature = "loom"))]
     const fn new() -> Self {
         Self {
             inner: AtomicU32::new(0),
@@ -1012,6 +1053,15 @@ impl<Host: HostInterface> RawMutex<Host> {
         }
     }
 
+    #[cfg(feature = "loom")]
+    fn new() -> Self {
+        Self {
+            futex: litebox::platform::loom_model::LoomFutex::new(0),
+            host: core::marker::PhantomData,
+        }
+    }
+
+    #[cfg(not(feature = "loom"))]
     fn block_or_maybe_timeout(
         &self,
         val: u32,
diff --git a/litebox_platform_multiplex/Cargo.toml b/litebox_platform_multiplex/Cargo.toml
index 1c48c3a73..e7202b321 100644
--- a/litebox_platform_multiplex/Cargo.toml
+++ b/litebox_platform_multiplex/Cargo.toml
@@ -22,6 +22,12 @@ platform_linux_userland_with_linux_syscall = ["platform_linux_userland", "litebo
 platform_linux_userland_with_optee_syscall = ["platform_linux_userland", "litebox_platform_linux_userland/optee_syscall"]
 platform_lvbs_with_linux_syscall = ["platform_lvbs", "litebox_platform_lvbs/linux_syscall"]
 platform_lvbs_with_optee_syscall = ["platform_lvbs", "litebox_platform_lvbs/optee_syscall"]
+loom = [
+	"litebox/loom",
+	"litebox_platform_linux_userland?/loom",
+	"litebox_platform_linux_kernel?/loom",
+	"litebox_platform_lvbs?/loom",
+]
 
 [lints]
 workspace = true
diff --git a/litebox_shim_linux/src/syscalls/process.rs b/litebox_shim_linux/src/syscalls/process.rs
index 69a41b70b..9cf828f57 100644
--- a/litebox_shim_linux/src/syscalls/process.rs
+++ b/litebox_shim_linux/src/syscalls/process.rs
@@ -158,7 +158,7 @@ pub(crate) enum ExitStatus {
 impl Process {
     /// Creates a new process with the given initial thread.
     fn new(pid: i32, remote: Arc<ThreadRemote>) -> Self {
-        let nr_threads = <Platform as litebox::platform::RawMutexProvider>::RawMutex::INIT;
+        let nr_threads = <Platform as litebox::platform::RawMutexProvider>::RawMutex::new();
         nr_threads.underlying_atomic().store(1, Ordering::Relaxed);
         Self {
             nr_threads,
diff --git a/litebox_shim_linux/src/syscalls/unix.rs b/litebox_shim_linux/src/syscalls/unix.rs
index 6aec592d8..a79b0530b 100644
--- a/litebox_shim_linux/src/syscalls/unix.rs
+++ b/litebox_shim_linux/src/syscalls/unix.rs
@@ -220,6 +220,7 @@ impl<FS: ShimFS> UnixInitStream<FS> {
     /// # Arguments
     ///
     /// * `backlog` - Maximum number of pending connections to queue
+    #[allow(clippy::result_large_err)]
     fn listen(
         self,
         backlog: u16,
@@ -279,6 +280,7 @@ impl<FS: ShimFS> Backlog<FS> {
     }
 
     /// Attempts to establish a connection without blocking.
+    #[allow(clippy::result_large_err)]
     fn try_connect(
         &self,
         init: UnixInitStream<FS>,