diff --git a/v2/crates/wifi-densepose-sensing-server/src/semantic/bus.rs b/v2/crates/wifi-densepose-sensing-server/src/semantic/bus.rs
index d5212f62..b5b168cd 100644
--- a/v2/crates/wifi-densepose-sensing-server/src/semantic/bus.rs
+++ b/v2/crates/wifi-densepose-sensing-server/src/semantic/bus.rs
@@ -226,4 +226,132 @@ mod tests {
         // it indirectly via primitives.
         let _ = Reason::empty();
     }
+
+    // ─── Property-based invariants ─────────────────────────────────
+    //
+    // The example-based tests above hit the obvious FSM transitions.
+    // These proptest cases throw random snapshot sequences at the bus
+    // and assert no primitive panics, every emitted state carries a
+    // reason payload, and the bus never returns Idle events (Idle is
+    // explicitly filtered).
+
+    use proptest::prelude::*;
+
+    fn arb_snapshot() -> impl Strategy<Value = RawSnapshot> {
+        // proptest only impls Strategy for tuples up to length 12, so
+        // we split into two nested tuples and merge in the prop_map.
+        let core = (
+            0u64..86400,                             // since_start secs
+            0i64..(1u64 << 40) as i64,               // timestamp_ms
+            any::<bool>(),                           // presence
+            any::<bool>(),                           // fall_detected
+            -0.5f64..2.0,                            // motion (incl. out-of-range)
+            -1000.0f64..10000.0,                     // motion_energy
+            proptest::option::of(0.0f64..200.0),     // breathing_rate_bpm
+        );
+        let extra = (
+            proptest::option::of(0.0f64..250.0),     // heart_rate_bpm
+            0u32..10,                                // n_persons
+            proptest::option::of(-120.0f64..0.0),    // rssi_dbm
+            0.0f64..1.0,                             // vital_confidence
+            0u32..86400,                             // local_seconds_since_midnight
+            prop::collection::vec("[a-z]{3,8}", 0..4), // active_zones
+        );
+        (core, extra).prop_map(
+            |((secs, ts, presence, fall, motion, energy, br),
+              (hr, n, rssi, conf, tod, zones))| {
+                RawSnapshot {
+                    node_id: "fuzz".into(),
+                    since_start: std::time::Duration::from_secs(secs),
+                    timestamp_ms: ts,
+                    presence,
+                    fall_detected: fall,
+                    motion,
+                    motion_energy: energy,
+                    breathing_rate_bpm: br,
+                    heart_rate_bpm: hr,
+                    n_persons: n,
+                    rssi_dbm: rssi,
+                    vital_confidence: conf,
+                    active_zones: zones,
+                    bed_zones: vec!["bedroom".into()],
+                    local_seconds_since_midnight: tod,
+                }
+            },
+        )
+    }
+
+    proptest! {
+        /// The bus never panics on any single snapshot, even with
+        /// pathological inputs (motion>1.0, NaN-prone HRs, empty
+        /// zones, etc).
+        #[test]
+        fn bus_tick_never_panics_on_arbitrary_snapshot(snap in arb_snapshot()) {
+            let mut bus = SemanticBus::new(PrimitiveConfig::default());
+            let _events = bus.tick(&snap);
+        }
+
+        /// Every emitted SemanticEvent carries a populated `node_id`
+        /// and the same `timestamp_ms` as the input snapshot. The bus
+        /// MUST NOT manufacture events with empty node IDs.
+        #[test]
+        fn bus_events_carry_node_id_and_ts(snap in arb_snapshot()) {
+            let mut bus = SemanticBus::new(PrimitiveConfig::default());
+            for ev in bus.tick(&snap) {
+                prop_assert!(!ev.node_id.is_empty(), "empty node_id in event {:?}", ev);
+                prop_assert_eq!(ev.timestamp_ms, snap.timestamp_ms);
+            }
+        }
+
+        /// No primitive emits a SemanticState::Boolean without
+        /// populating its `reason` field — the explainability contract
+        /// is enforced at the wire boundary.
+        #[test]
+        fn boolean_states_always_have_reason_tags(snap in arb_snapshot()) {
+            let mut bus = SemanticBus::new(PrimitiveConfig::default());
+            for ev in bus.tick(&snap) {
+                match &ev.state {
+                    PrimitiveState::Boolean { reason, changed, .. } => {
+                        if *changed {
+                            prop_assert!(
+                                !reason.tags.is_empty(),
+                                "changed Boolean must have reason tags: {:?}", ev,
+                            );
+                        }
+                    }
+                    _ => {}
+                }
+            }
+        }
+
+        /// A randomly-sequenced run of snapshots never makes the bus
+        /// produce more events than primitives it owns (currently 10).
+        /// This is the upper-bound invariant — each primitive emits at
+        /// most one event per tick.
+        #[test]
+        fn per_tick_event_count_bounded_by_primitive_count(snap in arb_snapshot()) {
+            let mut bus = SemanticBus::new(PrimitiveConfig::default());
+            let events = bus.tick(&snap);
+            prop_assert!(events.len() <= 10, "too many events: {}", events.len());
+        }
+
+        /// Replaying the same snapshot N times to a fresh bus produces
+        /// monotonic / consistent state (no jitter). This catches FSMs
+        /// that accidentally use uninitialised internal state.
+        #[test]
+        fn replay_same_snapshot_is_deterministic_per_fresh_bus(
+            snap in arb_snapshot(),
+            replays in 1usize..5,
+        ) {
+            let mut last: Option<Vec<SemanticKind>> = None;
+            for _ in 0..replays {
+                let mut bus = SemanticBus::new(PrimitiveConfig::default());
+                let kinds: Vec<_> = bus.tick(&snap).into_iter().map(|e| e.kind).collect();
+                if let Some(prev) = &last {
+                    prop_assert_eq!(prev, &kinds, "non-deterministic tick from fresh bus");
+                }
+                last = Some(kinds);
+            }
+        }
+    }
 }