diff --git a/crates/lore-tui/tests/nav_property_tests.rs b/crates/lore-tui/tests/nav_property_tests.rs
new file mode 100644
index 0000000..95ffe44
--- /dev/null
+++ b/crates/lore-tui/tests/nav_property_tests.rs
@@ -0,0 +1,392 @@
+//! Property tests for NavigationStack invariants (bd-3eis).
+//!
+//! Verifies that NavigationStack maintains its invariants under arbitrary
+//! sequences of push/pop/forward/jump/reset operations, using deterministic
+//! seeded random generation for reproducibility.
+//!
+//! All properties are tested across 10,000+ generated operation sequences.
+
+use lore_tui::message::{EntityKey, Screen};
+use lore_tui::navigation::NavigationStack;
+
+// ---------------------------------------------------------------------------
+// Seeded PRNG (xorshift64) — same as stress_tests.rs
+// ---------------------------------------------------------------------------
+
+struct Rng(u64);
+
+impl Rng {
+    fn new(seed: u64) -> Self {
+        Self(seed.wrapping_add(1))
+    }
+
+    fn next(&mut self) -> u64 {
+        let mut x = self.0;
+        x ^= x << 13;
+        x ^= x >> 7;
+        x ^= x << 17;
+        self.0 = x;
+        x
+    }
+
+    fn range(&mut self, max: u64) -> u64 {
+        self.next() % max
+    }
+}
+
+// ---------------------------------------------------------------------------
+// Random Screen and Operation generators
+// ---------------------------------------------------------------------------
+
+fn random_screen(rng: &mut Rng) -> Screen {
+    match rng.range(12) {
+        0 => Screen::Dashboard,
+        1 => Screen::IssueList,
+        2 => Screen::IssueDetail(EntityKey::issue(1, rng.range(100) as i64)),
+        3 => Screen::MrList,
+        4 => Screen::MrDetail(EntityKey::mr(1, rng.range(100) as i64)),
+        5 => Screen::Search,
+        6 => Screen::Timeline,
+        7 => Screen::Who,
+        8 => Screen::Trace,
+        9 => Screen::FileHistory,
+        10 => Screen::Sync,
+        _ => Screen::Stats,
+    }
+}
+
+#[derive(Debug)]
+enum NavOp {
+    Push(Screen),
+    Pop,
+    GoForward,
+    JumpBack,
+    JumpForward,
+    ResetTo(Screen),
+}
+
+fn random_op(rng: &mut Rng) -> NavOp {
+    match rng.range(10) {
+        // Push is the most common operation.
+        0..=4 => NavOp::Push(random_screen(rng)),
+        5 | 6 => NavOp::Pop,
+        7 => NavOp::GoForward,
+        8 => NavOp::JumpBack,
+        9 => NavOp::JumpForward,
+        _ => NavOp::ResetTo(random_screen(rng)),
+    }
+}
+
+fn apply_op(nav: &mut NavigationStack, op: &NavOp) {
+    match op {
+        NavOp::Push(screen) => {
+            nav.push(screen.clone());
+        }
+        NavOp::Pop => {
+            nav.pop();
+        }
+        NavOp::GoForward => {
+            nav.go_forward();
+        }
+        NavOp::JumpBack => {
+            nav.jump_back();
+        }
+        NavOp::JumpForward => {
+            nav.jump_forward();
+        }
+        NavOp::ResetTo(screen) => {
+            nav.reset_to(screen.clone());
+        }
+    }
+}
+
+// ---------------------------------------------------------------------------
+// Properties
+// ---------------------------------------------------------------------------
+
+/// Property 1: Stack depth is always >= 1.
+///
+/// The NavigationStack always has at least one screen (the root).
+/// No sequence of operations can empty it.
+#[test]
+fn prop_depth_always_at_least_one() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        for step in 0..100 {
+            let op = random_op(&mut rng);
+            apply_op(&mut nav, &op);
+
+            assert!(
+                nav.depth() >= 1,
+                "depth < 1 at seed={seed}, step={step}, op={op:?}"
+            );
+        }
+    }
+}
+
+/// Property 2: After push(X), current() == X.
+///
+/// Pushing a screen always makes it the current screen.
+#[test]
+fn prop_push_sets_current() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        for step in 0..100 {
+            let screen = random_screen(&mut rng);
+            nav.push(screen.clone());
+            assert_eq!(
+                nav.current(),
+                &screen,
+                "push didn't set current at seed={seed}, step={step}"
+            );
+
+            // Also do some random ops to make sequences varied.
+            if rng.range(3) == 0 {
+                let op = random_op(&mut rng);
+                apply_op(&mut nav, &op);
+            }
+        }
+    }
+}
+
+/// Property 3: After push(X) then pop(), current returns to previous.
+///
+/// Push-then-pop is identity on current() when no intermediate ops occur.
+#[test]
+fn prop_push_pop_returns_to_previous() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        // Do some random setup ops.
+        for _ in 0..rng.range(20) {
+            let op = random_op(&mut rng);
+            apply_op(&mut nav, &op);
+        }
+
+        let before = nav.current().clone();
+        let screen = random_screen(&mut rng);
+        nav.push(screen);
+
+        let pop_result = nav.pop();
+        assert!(pop_result.is_some(), "pop after push should succeed");
+        assert_eq!(
+            nav.current(),
+            &before,
+            "push-pop should restore previous at seed={seed}"
+        );
+    }
+}
+
+/// Property 4: Forward stack is cleared after any push.
+///
+/// Browser semantics: navigating to a new page clears the forward history.
+#[test]
+fn prop_forward_cleared_after_push() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        // Build up some forward stack via push-pop sequences.
+        for _ in 0..rng.range(10) + 2 {
+            nav.push(random_screen(&mut rng));
+        }
+        for _ in 0..rng.range(5) + 1 {
+            nav.pop();
+        }
+        // Now we might have forward entries.
+
+        // Push clears forward.
+        nav.push(random_screen(&mut rng));
+        assert!(
+            !nav.can_go_forward(),
+            "forward stack should be empty after push at seed={seed}"
+        );
+    }
+}
+
+/// Property 5: Jump list only records detail/entity screens.
+///
+/// The jump list (vim Ctrl+O/Ctrl+I) only tracks IssueDetail and MrDetail.
+/// After many operations, every jump_back/jump_forward target should be
+/// a detail screen.
+#[test]
+fn prop_jump_list_only_details() {
+    for seed in 0..500 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        // Do many operations to build up jump list.
+        for _ in 0..200 {
+            let op = random_op(&mut rng);
+            apply_op(&mut nav, &op);
+        }
+
+        // Walk the jump list backward and forward — every screen reached
+        // should be a detail screen.
+        let saved_current = nav.current().clone();
+
+        let mut visited = Vec::new();
+        while let Some(screen) = nav.jump_back() {
+            visited.push(screen.clone());
+        }
+        while let Some(screen) = nav.jump_forward() {
+            visited.push(screen.clone());
+        }
+
+        for screen in &visited {
+            assert!(
+                screen.is_detail_or_entity(),
+                "jump list contained non-detail screen {screen:?} at seed={seed}"
+            );
+        }
+
+        // Restore (this is a property test, not behavior test — we don't
+        // care about restoring, just checking the invariant).
+        let _ = saved_current;
+    }
+}
+
+/// Property 6: reset_to(X) clears all history, current() == X.
+///
+/// After reset, depth == 1, no back, no forward, empty jump list.
+#[test]
+fn prop_reset_clears_all() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        // Build up complex state.
+        for _ in 0..rng.range(50) + 10 {
+            let op = random_op(&mut rng);
+            apply_op(&mut nav, &op);
+        }
+
+        let target = random_screen(&mut rng);
+        nav.reset_to(target.clone());
+
+        assert_eq!(
+            nav.current(),
+            &target,
+            "reset didn't set current at seed={seed}"
+        );
+        assert_eq!(
+            nav.depth(),
+            1,
+            "reset didn't clear back stack at seed={seed}"
+        );
+        assert!(!nav.can_go_back(), "reset didn't clear back at seed={seed}");
+        assert!(
+            !nav.can_go_forward(),
+            "reset didn't clear forward at seed={seed}"
+        );
+    }
+}
+
+/// Property 7: Breadcrumbs length == depth.
+///
+/// breadcrumbs() always returns exactly as many entries as the navigation
+/// depth (back_stack + 1 for current).
+#[test]
+fn prop_breadcrumbs_match_depth() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        for step in 0..100 {
+            let op = random_op(&mut rng);
+            apply_op(&mut nav, &op);
+
+            assert_eq!(
+                nav.breadcrumbs().len(),
+                nav.depth(),
+                "breadcrumbs length != depth at seed={seed}, step={step}, op={op:?}"
+            );
+        }
+    }
+}
+
+/// Property 8: No panic for any sequence of operations.
+///
+/// This is the "chaos monkey" property — the most important invariant.
+#[test]
+fn prop_no_panic_any_sequence() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        for _ in 0..200 {
+            let op = random_op(&mut rng);
+            apply_op(&mut nav, &op);
+        }
+
+        // If we got here, no panic occurred.
+        assert!(nav.depth() >= 1);
+    }
+}
+
+/// Property 9: Pop at root is always safe and returns None.
+///
+/// Repeated pops from any state eventually reach root and stop.
+#[test]
+fn prop_repeated_pop_reaches_root() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        // Push random depth.
+        let pushes = rng.range(20) + 1;
+        for _ in 0..pushes {
+            nav.push(random_screen(&mut rng));
+        }
+
+        // Pop until we can't.
+        let mut pops = 0;
+        while nav.pop().is_some() {
+            pops += 1;
+            assert!(pops <= pushes, "more pops than pushes at seed={seed}");
+        }
+
+        assert_eq!(
+            nav.depth(),
+            1,
+            "should be at root after exhaustive pop at seed={seed}"
+        );
+        // One more pop should be None.
+        assert!(nav.pop().is_none());
+    }
+}
+
+/// Property 10: Go forward after go back restores screen.
+///
+/// Pop-then-forward is identity (when no intermediate push).
+#[test]
+fn prop_pop_forward_identity() {
+    for seed in 0..1000 {
+        let mut rng = Rng::new(seed);
+        let mut nav = NavigationStack::new();
+
+        // Build some state.
+        for _ in 0..rng.range(10) + 2 {
+            nav.push(random_screen(&mut rng));
+        }
+
+        let before_pop = nav.current().clone();
+        if nav.pop().is_some() {
+            let result = nav.go_forward();
+            assert!(
+                result.is_some(),
+                "forward should succeed after pop at seed={seed}"
+            );
+            assert_eq!(
+                nav.current(),
+                &before_pop,
+                "pop-forward should restore screen at seed={seed}"
+            );
+        }
+    }
+}