diff --git a/Cargo.lock b/Cargo.lock
index b155f12..8ccd3fa 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -308,6 +308,13 @@ version = "0.8.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a"
 
+[[package]]
+name = "relay-ccsds"
+version = "0.1.0"
+dependencies = [
+ "wit-bindgen 0.41.0",
+]
+
 [[package]]
 name = "relay-cs"
 version = "0.1.0"
@@ -340,9 +347,14 @@ dependencies = [
 name = "relay-lc"
 version = "0.1.0"
 dependencies = [
+ "relay-primitives",
  "wit-bindgen 0.41.0",
 ]
 
+[[package]]
+name = "relay-primitives"
+version = "0.1.0"
+
 [[package]]
 name = "relay-sch"
 version = "0.1.0"
@@ -750,6 +762,7 @@ version = "0.1.0"
 name = "wohl-hub"
 version = "0.1.0"
 dependencies = [
+ "relay-ccsds",
  "relay-cs",
  "relay-ds",
  "relay-hk",
diff --git a/Cargo.toml b/Cargo.toml
index b91a0fa..e042d6b 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -18,6 +18,9 @@ license = "Apache-2.0"
 repository = "https://github.com/pulseengine/wohl"
 rust-version = "1.85.0"
 
+[workspace.lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
 [workspace.dependencies]
 relay-lc = { path = "../relay/crates/relay-lc" }
 relay-sc = { path = "../relay/crates/relay-sc" }
@@ -28,6 +31,7 @@ relay-hk = { path = "../relay/crates/relay-hk" }
 relay-tbl = { path = "../relay/crates/relay-tbl" }
 relay-cs = { path = "../relay/crates/relay-cs" }
 relay-to = { path = "../relay/crates/relay-to" }
+relay-ccsds = { path = "../relay/crates/relay-ccsds" }
 wohl-leak = { path = "crates/wohl-leak" }
 wohl-temp = { path = "crates/wohl-temp" }
 wohl-air = { path = "crates/wohl-air" }
diff --git a/crates/wohl-air/Cargo.toml b/crates/wohl-air/Cargo.toml
index 1c2e249..d3e88ad 100644
--- a/crates/wohl-air/Cargo.toml
+++ b/crates/wohl-air/Cargo.toml
@@ -12,3 +12,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 relay-lc.workspace = true
+
+[lints]
+workspace = true
diff --git a/crates/wohl-air/plain/src/engine.rs b/crates/wohl-air/plain/src/engine.rs
index 6f09ac9..f596bd3 100644
--- a/crates/wohl-air/plain/src/engine.rs
+++ b/crates/wohl-air/plain/src/engine.rs
@@ -4,9 +4,7 @@
 //!   - relay-lc::WatchpointTable handles CO2/PM2.5/VOC thresholds (VERIFIED)
 //!   - This module adds: domain type translation, multi-metric mapping
 
-use relay_lc::engine::{
-    ComparisonOp, SensorReading, Watchpoint, WatchpointTable,
-};
+use relay_lc::engine::{ComparisonOp, SensorReading, Watchpoint, WatchpointTable};
 
 pub const MAX_ZONES: usize = 16;
 pub const MAX_ALERTS_PER_READING: usize = 6;
@@ -33,7 +31,14 @@ pub struct AirReading {
 }
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub enum AirAlertType { Co2Warning, Co2Critical, Pm25Warning, Pm25Critical, VocWarning, VocCritical }
+pub enum AirAlertType {
+    Co2Warning,
+    Co2Critical,
+    Pm25Warning,
+    Pm25Critical,
+    VocWarning,
+    VocCritical,
+}
 
 #[derive(Clone, Copy)]
 pub struct AirAlert {
@@ -51,16 +56,25 @@ pub struct AirResult {
 
 impl AirAlert {
     pub const fn empty() -> Self {
-        AirAlert { zone_id: 0, alert_type: AirAlertType::Co2Warning, value: 0, threshold: 0, time: 0 }
+        AirAlert {
+            zone_id: 0,
+            alert_type: AirAlertType::Co2Warning,
+            value: 0,
+            threshold: 0,
+            time: 0,
+        }
     }
 }
 
 // Watchpoint ID encoding: zone_id * 6 + metric_offset
 // 0=co2_warn, 1=co2_critical, 2=pm25_warn, 3=pm25_critical, 4=voc_warn, 5=voc_critical
 const ALERT_TYPES: [AirAlertType; 6] = [
-    AirAlertType::Co2Warning, AirAlertType::Co2Critical,
-    AirAlertType::Pm25Warning, AirAlertType::Pm25Critical,
-    AirAlertType::VocWarning, AirAlertType::VocCritical,
+    AirAlertType::Co2Warning,
+    AirAlertType::Co2Critical,
+    AirAlertType::Pm25Warning,
+    AirAlertType::Pm25Critical,
+    AirAlertType::VocWarning,
+    AirAlertType::VocCritical,
 ];
 
 pub struct AirMonitor {
@@ -70,31 +84,54 @@ pub struct AirMonitor {
 
 impl AirConfig {
     pub const fn empty() -> Self {
-        AirConfig { zone_id: 0, co2_warn: 0, co2_critical: 0, pm25_warn: 0, pm25_critical: 0, voc_warn: 0, voc_critical: 0, enabled: false }
+        AirConfig {
+            zone_id: 0,
+            co2_warn: 0,
+            co2_critical: 0,
+            pm25_warn: 0,
+            pm25_critical: 0,
+            voc_warn: 0,
+            voc_critical: 0,
+            enabled: false,
+        }
+    }
+}
+
+impl Default for AirMonitor {
+    fn default() -> Self {
+        Self::new()
     }
 }
 
 impl AirMonitor {
     pub fn new() -> Self {
-        AirMonitor { watchpoints: WatchpointTable::new(), zone_count: 0 }
+        AirMonitor {
+            watchpoints: WatchpointTable::new(),
+            zone_count: 0,
+        }
     }
 
     /// Register a zone. Creates 6 relay-lc watchpoints (warn+critical for each metric).
     pub fn register_zone(&mut self, config: AirConfig) -> bool {
-        if self.zone_count as usize >= MAX_ZONES { return false; }
+        if self.zone_count as usize >= MAX_ZONES {
+            return false;
+        }
 
         let base = config.zone_id * 6;
         let thresholds = [
-            config.co2_warn, config.co2_critical,
-            config.pm25_warn, config.pm25_critical,
-            config.voc_warn, config.voc_critical,
+            config.co2_warn,
+            config.co2_critical,
+            config.pm25_warn,
+            config.pm25_critical,
+            config.voc_warn,
+            config.voc_critical,
         ];
 
-        for i in 0..6 {
+        for (i, &threshold) in thresholds.iter().enumerate() {
             self.watchpoints.add_watchpoint(Watchpoint {
                 sensor_id: base + i as u32,
                 op: ComparisonOp::GreaterOrEqual,
-                threshold: thresholds[i] as i64,
+                threshold: threshold as i64,
                 enabled: config.enabled,
                 persistence: 1,
                 current_count: 0,
@@ -107,12 +144,24 @@ impl AirMonitor {
 
     /// Process an air quality reading. All threshold checks go through relay-lc.
     pub fn process_reading(&mut self, reading: AirReading) -> AirResult {
-        let mut res = AirResult { alerts: [AirAlert::empty(); MAX_ALERTS_PER_READING], alert_count: 0 };
+        let mut res = AirResult {
+            alerts: [AirAlert::empty(); MAX_ALERTS_PER_READING],
+            alert_count: 0,
+        };
         let base = reading.zone_id * 6;
-        let values = [reading.co2_ppm, reading.co2_ppm, reading.pm25, reading.pm25, reading.voc_index, reading.voc_index];
+        let values = [
+            reading.co2_ppm,
+            reading.co2_ppm,
+            reading.pm25,
+            reading.pm25,
+            reading.voc_index,
+            reading.voc_index,
+        ];
 
         for i in 0..6 {
-            if res.alert_count as usize >= MAX_ALERTS_PER_READING { break; }
+            if res.alert_count as usize >= MAX_ALERTS_PER_READING {
+                break;
+            }
             let result = self.watchpoints.evaluate(SensorReading {
                 sensor_id: base + i as u32,
                 value: values[i] as i64,
@@ -138,50 +187,112 @@ mod tests {
     use super::*;
 
     fn make_config(zone_id: u32) -> AirConfig {
-        AirConfig { zone_id, co2_warn: 1000, co2_critical: 2000, pm25_warn: 250, pm25_critical: 500, voc_warn: 200, voc_critical: 400, enabled: true }
+        AirConfig {
+            zone_id,
+            co2_warn: 1000,
+            co2_critical: 2000,
+            pm25_warn: 250,
+            pm25_critical: 500,
+            voc_warn: 200,
+            voc_critical: 400,
+            enabled: true,
+        }
     }
 
     #[test]
-    fn test_empty() { let mut m = AirMonitor::new(); let r = m.process_reading(AirReading { zone_id: 1, co2_ppm: 400, pm25: 50, voc_index: 30, time: 100 }); assert_eq!(r.alert_count, 0); }
+    fn test_empty() {
+        let mut m = AirMonitor::new();
+        let r = m.process_reading(AirReading {
+            zone_id: 1,
+            co2_ppm: 400,
+            pm25: 50,
+            voc_index: 30,
+            time: 100,
+        });
+        assert_eq!(r.alert_count, 0);
+    }
 
     #[test]
     fn test_co2_warning() {
-        let mut m = AirMonitor::new(); m.register_zone(make_config(1));
-        let r = m.process_reading(AirReading { zone_id: 1, co2_ppm: 1200, pm25: 50, voc_index: 30, time: 100 });
+        let mut m = AirMonitor::new();
+        m.register_zone(make_config(1));
+        let r = m.process_reading(AirReading {
+            zone_id: 1,
+            co2_ppm: 1200,
+            pm25: 50,
+            voc_index: 30,
+            time: 100,
+        });
         assert!(r.alert_count >= 1);
         assert_eq!(r.alerts[0].alert_type, AirAlertType::Co2Warning);
     }
 
     #[test]
     fn test_co2_critical() {
-        let mut m = AirMonitor::new(); m.register_zone(make_config(1));
-        let r = m.process_reading(AirReading { zone_id: 1, co2_ppm: 2500, pm25: 50, voc_index: 30, time: 100 });
+        let mut m = AirMonitor::new();
+        m.register_zone(make_config(1));
+        let r = m.process_reading(AirReading {
+            zone_id: 1,
+            co2_ppm: 2500,
+            pm25: 50,
+            voc_index: 30,
+            time: 100,
+        });
         // Should trigger both co2_warn AND co2_critical
         assert!(r.alert_count >= 2);
     }
 
     #[test]
     fn test_pm25_alert() {
-        let mut m = AirMonitor::new(); m.register_zone(make_config(1));
-        let r = m.process_reading(AirReading { zone_id: 1, co2_ppm: 400, pm25: 300, voc_index: 30, time: 100 });
+        let mut m = AirMonitor::new();
+        m.register_zone(make_config(1));
+        let r = m.process_reading(AirReading {
+            zone_id: 1,
+            co2_ppm: 400,
+            pm25: 300,
+            voc_index: 30,
+            time: 100,
+        });
         let mut found = false;
-        for j in 0..r.alert_count as usize { if r.alerts[j].alert_type == AirAlertType::Pm25Warning { found = true; } }
+        for j in 0..r.alert_count as usize {
+            if r.alerts[j].alert_type == AirAlertType::Pm25Warning {
+                found = true;
+            }
+        }
         assert!(found);
     }
 
     #[test]
     fn test_voc_alert() {
-        let mut m = AirMonitor::new(); m.register_zone(make_config(1));
-        let r = m.process_reading(AirReading { zone_id: 1, co2_ppm: 400, pm25: 50, voc_index: 250, time: 100 });
+        let mut m = AirMonitor::new();
+        m.register_zone(make_config(1));
+        let r = m.process_reading(AirReading {
+            zone_id: 1,
+            co2_ppm: 400,
+            pm25: 50,
+            voc_index: 250,
+            time: 100,
+        });
         let mut found = false;
-        for j in 0..r.alert_count as usize { if r.alerts[j].alert_type == AirAlertType::VocWarning { found = true; } }
+        for j in 0..r.alert_count as usize {
+            if r.alerts[j].alert_type == AirAlertType::VocWarning {
+                found = true;
+            }
+        }
         assert!(found);
     }
 
     #[test]
     fn test_normal_no_alert() {
-        let mut m = AirMonitor::new(); m.register_zone(make_config(1));
-        let r = m.process_reading(AirReading { zone_id: 1, co2_ppm: 400, pm25: 50, voc_index: 30, time: 100 });
+        let mut m = AirMonitor::new();
+        m.register_zone(make_config(1));
+        let r = m.process_reading(AirReading {
+            zone_id: 1,
+            co2_ppm: 400,
+            pm25: 50,
+            voc_index: 30,
+            time: 100,
+        });
         assert_eq!(r.alert_count, 0);
     }
 }
@@ -243,7 +354,11 @@ mod kani_proofs {
         // All values strictly below their warn thresholds
         kani::assume(co2 < co2_warn && pm25 < pm25_warn && voc < voc_warn);
         let r = m.process_reading(AirReading {
-            zone_id: 1, co2_ppm: co2, pm25, voc_index: voc, time: 100,
+            zone_id: 1,
+            co2_ppm: co2,
+            pm25,
+            voc_index: voc,
+            time: 100,
         });
         assert_eq!(r.alert_count, 0);
     }
diff --git a/crates/wohl-alert/Cargo.toml b/crates/wohl-alert/Cargo.toml
index 3a815bf..d8aba99 100644
--- a/crates/wohl-alert/Cargo.toml
+++ b/crates/wohl-alert/Cargo.toml
@@ -15,3 +15,6 @@ relay-to.workspace = true
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true
diff --git a/crates/wohl-alert/plain/src/engine.rs b/crates/wohl-alert/plain/src/engine.rs
index 60573bc..a9d75fb 100644
--- a/crates/wohl-alert/plain/src/engine.rs
+++ b/crates/wohl-alert/plain/src/engine.rs
@@ -16,13 +16,25 @@ pub const MAX_ALERTS_PER_MINUTE: u32 = 10;
 pub const MAX_CHANNELS: usize = 8;
 
 #[derive(Clone, Copy)]
-pub struct AlertEntry { pub zone_id: u32, pub alert_type: u8, pub time: u64 }
+pub struct AlertEntry {
+    pub zone_id: u32,
+    pub alert_type: u8,
+    pub time: u64,
+}
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub enum DispatchAction { Send, Deduplicated, RateLimited, NotSubscribed }
+pub enum DispatchAction {
+    Send,
+    Deduplicated,
+    RateLimited,
+    NotSubscribed,
+}
 
 #[derive(Clone, Copy)]
-pub struct DispatchResult { pub action: DispatchAction, pub queue_depth: u32 }
+pub struct DispatchResult {
+    pub action: DispatchAction,
+    pub queue_depth: u32,
+}
 
 /// Encodes an alert type + zone into a subscription message ID.
 /// Layout: upper 8 bits = alert_type, lower 24 bits = zone_id.
@@ -40,7 +52,19 @@ pub struct AlertDispatcher {
 }
 
 impl AlertEntry {
-    pub const fn empty() -> Self { AlertEntry { zone_id: 0, alert_type: 0, time: 0 } }
+    pub const fn empty() -> Self {
+        AlertEntry {
+            zone_id: 0,
+            alert_type: 0,
+            time: 0,
+        }
+    }
+}
+
+impl Default for AlertDispatcher {
+    fn default() -> Self {
+        Self::new()
+    }
 }
 
 impl AlertDispatcher {
@@ -85,7 +109,10 @@ impl AlertDispatcher {
         let msg_id = subscription_msg_id(zone_id, alert_type);
         let decision = self.subscriptions.evaluate(msg_id);
         if decision == ToDecision::Exclude || decision == ToDecision::NotSubscribed {
-            return DispatchResult { action: DispatchAction::NotSubscribed, queue_depth: self.recent_count };
+            return DispatchResult {
+                action: DispatchAction::NotSubscribed,
+                queue_depth: self.recent_count,
+            };
         }
 
         // ── Phase 1: dedup check (domain-specific) ──
@@ -105,27 +132,40 @@ impl AlertDispatcher {
                 && self.recent[idx].alert_type == alert_type
                 && time < self.recent[idx].time.saturating_add(DEDUP_COOLDOWN_SEC)
             {
-                return DispatchResult { action: DispatchAction::Deduplicated, queue_depth: self.recent_count };
+                return DispatchResult {
+                    action: DispatchAction::Deduplicated,
+                    queue_depth: self.recent_count,
+                };
             }
-            i = i + 1;
+            i += 1;
         }
 
         // ── Phase 2: rate limit check (domain-specific) ──
 
         if self.minute_count >= MAX_ALERTS_PER_MINUTE {
-            return DispatchResult { action: DispatchAction::RateLimited, queue_depth: self.recent_count };
+            return DispatchResult {
+                action: DispatchAction::RateLimited,
+                queue_depth: self.recent_count,
+            };
         }
 
         // Record in recent window
         if (self.recent_count as usize) < MAX_RECENT_ALERTS {
             let ridx = self.recent_count as usize;
-            self.recent[ridx] = AlertEntry { zone_id, alert_type, time };
-            self.recent_count = self.recent_count + 1;
+            self.recent[ridx] = AlertEntry {
+                zone_id,
+                alert_type,
+                time,
+            };
+            self.recent_count += 1;
         }
 
-        self.minute_count = self.minute_count + 1;
+        self.minute_count += 1;
 
-        DispatchResult { action: DispatchAction::Send, queue_depth: self.recent_count }
+        DispatchResult {
+            action: DispatchAction::Send,
+            queue_depth: self.recent_count,
+        }
     }
 
     pub fn clear_expired(&mut self, current_time: u64) {
@@ -139,9 +179,9 @@ impl AlertDispatcher {
                 if write != read {
                     self.recent[write as usize] = self.recent[ridx];
                 }
-                write = write + 1;
+                write += 1;
             }
-            read = read + 1;
+            read += 1;
         }
 
         self.recent_count = write;
@@ -159,19 +199,22 @@ mod tests {
         d
     }
 
-    #[test] fn test_first_alert_sends() {
+    #[test]
+    fn test_first_alert_sends() {
         let mut d = subscribed_dispatcher(1, 1);
         let r = d.process_alert(1, 1, 1000);
         assert_eq!(r.action, DispatchAction::Send);
     }
 
-    #[test] fn test_not_subscribed_rejects() {
+    #[test]
+    fn test_not_subscribed_rejects() {
         let mut d = AlertDispatcher::new();
         let r = d.process_alert(1, 1, 1000);
         assert_eq!(r.action, DispatchAction::NotSubscribed);
     }
 
-    #[test] fn test_unsubscribed_rejects() {
+    #[test]
+    fn test_unsubscribed_rejects() {
         let mut d = AlertDispatcher::new();
         d.subscribe(1, 1, 1);
         d.unsubscribe(1, 1);
@@ -179,7 +222,8 @@ mod tests {
         assert_eq!(r.action, DispatchAction::NotSubscribed);
     }
 
-    #[test] fn test_subscription_check() {
+    #[test]
+    fn test_subscription_check() {
         let mut d = AlertDispatcher::new();
         assert!(!d.is_subscribed(1, 1));
         d.subscribe(1, 1, 1);
@@ -187,7 +231,8 @@ mod tests {
         assert!(!d.is_subscribed(2, 1));
     }
 
-    #[test] fn test_active_count() {
+    #[test]
+    fn test_active_count() {
         let mut d = AlertDispatcher::new();
         d.subscribe(1, 1, 1);
         d.subscribe(2, 1, 1);
@@ -196,21 +241,24 @@ mod tests {
         assert_eq!(d.active_subscription_count(), 1);
     }
 
-    #[test] fn test_duplicate_within_cooldown() {
+    #[test]
+    fn test_duplicate_within_cooldown() {
         let mut d = subscribed_dispatcher(1, 1);
         d.process_alert(1, 1, 1000);
         let r = d.process_alert(1, 1, 1100);
         assert_eq!(r.action, DispatchAction::Deduplicated);
     }
 
-    #[test] fn test_duplicate_after_cooldown() {
+    #[test]
+    fn test_duplicate_after_cooldown() {
         let mut d = subscribed_dispatcher(1, 1);
         d.process_alert(1, 1, 1000);
         let r = d.process_alert(1, 1, 1300);
         assert_eq!(r.action, DispatchAction::Send);
     }
 
-    #[test] fn test_rate_limit_kicks_in() {
+    #[test]
+    fn test_rate_limit_kicks_in() {
         let mut d = AlertDispatcher::new();
         for i in 0..MAX_ALERTS_PER_MINUTE {
             d.subscribe(100 + i, 1, 1);
@@ -224,7 +272,8 @@ mod tests {
         assert_eq!(r.action, DispatchAction::RateLimited);
     }
 
-    #[test] fn test_rate_limit_resets_after_minute() {
+    #[test]
+    fn test_rate_limit_resets_after_minute() {
         let mut d = AlertDispatcher::new();
         for i in 0..MAX_ALERTS_PER_MINUTE {
             d.subscribe(100 + i, 1, 1);
@@ -237,7 +286,8 @@ mod tests {
         assert_eq!(r.action, DispatchAction::Send);
     }
 
-    #[test] fn test_clear_expired() {
+    #[test]
+    fn test_clear_expired() {
         let mut d = subscribed_dispatcher(1, 1);
         d.process_alert(1, 1, 1000);
         assert_eq!(d.recent_count, 1);
@@ -247,7 +297,8 @@ mod tests {
         assert_eq!(r.action, DispatchAction::Send);
     }
 
-    #[test] fn test_different_zone_not_deduplicated() {
+    #[test]
+    fn test_different_zone_not_deduplicated() {
         let mut d = AlertDispatcher::new();
         d.subscribe(1, 1, 1);
         d.subscribe(2, 1, 1);
@@ -256,7 +307,8 @@ mod tests {
         assert_eq!(r.action, DispatchAction::Send);
     }
 
-    #[test] fn test_msg_id_encoding() {
+    #[test]
+    fn test_msg_id_encoding() {
         // alert_type=1, zone_id=42 -> (1 << 24) | 42 = 0x0100_002A
         assert_eq!(subscription_msg_id(42, 1), 0x0100_002A);
         // alert_type=0xFF, zone_id=0x00FF_FFFF -> (0xFF << 24) | 0x00FF_FFFF
@@ -358,7 +410,9 @@ mod kani_proofs {
         let zone_id: u32 = kani::any();
         let alert_type: u8 = kani::any();
         // No subscriptions — relay-to should return NotSubscribed
-        let decision = d.subscriptions.evaluate(subscription_msg_id(zone_id, alert_type));
+        let decision = d
+            .subscriptions
+            .evaluate(subscription_msg_id(zone_id, alert_type));
         assert_eq!(decision, ToDecision::NotSubscribed);
     }
 
diff --git a/crates/wohl-door/Cargo.toml b/crates/wohl-door/Cargo.toml
index 411442a..8dde179 100644
--- a/crates/wohl-door/Cargo.toml
+++ b/crates/wohl-door/Cargo.toml
@@ -9,3 +9,6 @@ rust-version = "1.85.0"
 [lib]
 path = "plain/src/lib.rs"
 crate-type = ["rlib"]
+
+[lints]
+workspace = true
diff --git a/crates/wohl-door/plain/src/engine.rs b/crates/wohl-door/plain/src/engine.rs
index eedf49d..67ed94b 100644
--- a/crates/wohl-door/plain/src/engine.rs
+++ b/crates/wohl-door/plain/src/engine.rs
@@ -23,7 +23,10 @@ pub struct ContactState {
 }
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub enum DoorAlertType { OpenTooLong, OpenedAtNight }
+pub enum DoorAlertType {
+    OpenTooLong,
+    OpenedAtNight,
+}
 
 #[derive(Clone, Copy)]
 pub struct DoorAlert {
@@ -48,25 +51,52 @@ pub struct DoorWatch {
 
 impl ContactConfig {
     pub const fn empty() -> Self {
-        ContactConfig { contact_id: 0, zone_id: 0, max_open_sec: 0, night_start_hour: 0, night_end_hour: 0, enabled: false }
+        ContactConfig {
+            contact_id: 0,
+            zone_id: 0,
+            max_open_sec: 0,
+            night_start_hour: 0,
+            night_end_hour: 0,
+            enabled: false,
+        }
     }
 }
 
 impl ContactState {
     pub const fn empty() -> Self {
-        ContactState { contact_id: 0, open: false, opened_at: 0, active: false }
+        ContactState {
+            contact_id: 0,
+            open: false,
+            opened_at: 0,
+            active: false,
+        }
     }
 }
 
 impl DoorAlert {
     pub const fn empty() -> Self {
-        DoorAlert { contact_id: 0, zone_id: 0, alert_type: DoorAlertType::OpenTooLong, open_duration_sec: 0, time: 0 }
+        DoorAlert {
+            contact_id: 0,
+            zone_id: 0,
+            alert_type: DoorAlertType::OpenTooLong,
+            open_duration_sec: 0,
+            time: 0,
+        }
     }
 }
 
 impl DoorResult {
     pub const fn empty() -> Self {
-        DoorResult { alerts: [DoorAlert::empty(); MAX_ALERTS_PER_CHECK], alert_count: 0 }
+        DoorResult {
+            alerts: [DoorAlert::empty(); MAX_ALERTS_PER_CHECK],
+            alert_count: 0,
+        }
+    }
+}
+
+impl Default for DoorWatch {
+    fn default() -> Self {
+        Self::new()
     }
 }
 
@@ -80,7 +110,9 @@ impl DoorWatch {
     }
 
     pub fn register_contact(&mut self, config: ContactConfig) -> bool {
-        if self.contact_count as usize >= MAX_CONTACTS { return false; }
+        if self.contact_count as usize >= MAX_CONTACTS {
+            return false;
+        }
         let idx = self.contact_count as usize;
         self.configs[idx] = config;
         self.states[idx] = ContactState {
@@ -120,17 +152,16 @@ impl DoorWatch {
                         hour_of_day,
                         self.configs[idx].night_start_hour,
                         self.configs[idx].night_end_hour,
-                    ) {
-                        if (res.alert_count as usize) < MAX_ALERTS_PER_CHECK {
-                            res.alerts[res.alert_count as usize] = DoorAlert {
-                                contact_id,
-                                zone_id: self.configs[idx].zone_id,
-                                alert_type: DoorAlertType::OpenedAtNight,
-                                open_duration_sec: 0,
-                                time,
-                            };
-                            res.alert_count += 1;
-                        }
+                    ) && (res.alert_count as usize) < MAX_ALERTS_PER_CHECK
+                    {
+                        res.alerts[res.alert_count as usize] = DoorAlert {
+                            contact_id,
+                            zone_id: self.configs[idx].zone_id,
+                            alert_type: DoorAlertType::OpenedAtNight,
+                            open_duration_sec: 0,
+                            time,
+                        };
+                        res.alert_count += 1;
                     }
                 } else {
                     self.states[idx].open = false;
@@ -150,24 +181,21 @@ impl DoorWatch {
         let mut i: u32 = 0;
         while i < count {
             let idx = i as usize;
-            if self.states[idx].active
-                && self.configs[idx].enabled
-                && self.states[idx].open
-            {
+            if self.states[idx].active && self.configs[idx].enabled && self.states[idx].open {
                 let opened_at = self.states[idx].opened_at;
                 if current_time >= opened_at {
                     let duration = current_time - opened_at;
-                    if duration > self.configs[idx].max_open_sec as u64 {
-                        if (res.alert_count as usize) < MAX_ALERTS_PER_CHECK {
-                            res.alerts[res.alert_count as usize] = DoorAlert {
-                                contact_id: self.configs[idx].contact_id,
-                                zone_id: self.configs[idx].zone_id,
-                                alert_type: DoorAlertType::OpenTooLong,
-                                open_duration_sec: duration,
-                                time: current_time,
-                            };
-                            res.alert_count += 1;
-                        }
+                    if duration > self.configs[idx].max_open_sec as u64
+                        && (res.alert_count as usize) < MAX_ALERTS_PER_CHECK
+                    {
+                        res.alerts[res.alert_count as usize] = DoorAlert {
+                            contact_id: self.configs[idx].contact_id,
+                            zone_id: self.configs[idx].zone_id,
+                            alert_type: DoorAlertType::OpenTooLong,
+                            open_duration_sec: duration,
+                            time: current_time,
+                        };
+                        res.alert_count += 1;
                     }
                 }
             }
@@ -183,15 +211,65 @@ mod tests {
     use super::*;
 
     fn make_config(contact_id: u32, zone_id: u32) -> ContactConfig {
-        ContactConfig { contact_id, zone_id, max_open_sec: 300, night_start_hour: 22, night_end_hour: 6, enabled: true }
+        ContactConfig {
+            contact_id,
+            zone_id,
+            max_open_sec: 300,
+            night_start_hour: 22,
+            night_end_hour: 6,
+            enabled: true,
+        }
     }
 
-    #[test] fn test_open_close() { let mut w = DoorWatch::new(); w.register_contact(make_config(1, 10)); let r = w.process_event(1, true, 43200); assert_eq!(r.alert_count, 0); let r = w.process_event(1, false, 43260); assert_eq!(r.alert_count, 0); }
-    #[test] fn test_open_too_long() { let mut w = DoorWatch::new(); w.register_contact(make_config(1, 10)); w.process_event(1, true, 43200); let r = w.check_timeouts(43200 + 400); assert_eq!(r.alert_count, 1); assert_eq!(r.alerts[0].alert_type, DoorAlertType::OpenTooLong); }
-    #[test] fn test_opened_at_night() { let mut w = DoorWatch::new(); w.register_contact(make_config(1, 10)); let r = w.process_event(1, true, 82800); assert_eq!(r.alert_count, 1); assert_eq!(r.alerts[0].alert_type, DoorAlertType::OpenedAtNight); }
-    #[test] fn test_normal_day() { let mut w = DoorWatch::new(); w.register_contact(make_config(1, 10)); let r = w.process_event(1, true, 50400); assert_eq!(r.alert_count, 0); }
-    #[test] fn test_unknown_contact() { let mut w = DoorWatch::new(); let r = w.process_event(99, true, 1000); assert_eq!(r.alert_count, 0); }
-    #[test] fn test_multiple_contacts() { let mut w = DoorWatch::new(); w.register_contact(make_config(1, 10)); w.register_contact(make_config(2, 20)); w.process_event(1, true, 43200); w.process_event(2, true, 43200); let r = w.check_timeouts(43200 + 400); assert_eq!(r.alert_count, 2); }
+    #[test]
+    fn test_open_close() {
+        let mut w = DoorWatch::new();
+        w.register_contact(make_config(1, 10));
+        let r = w.process_event(1, true, 43200);
+        assert_eq!(r.alert_count, 0);
+        let r = w.process_event(1, false, 43260);
+        assert_eq!(r.alert_count, 0);
+    }
+    #[test]
+    fn test_open_too_long() {
+        let mut w = DoorWatch::new();
+        w.register_contact(make_config(1, 10));
+        w.process_event(1, true, 43200);
+        let r = w.check_timeouts(43200 + 400);
+        assert_eq!(r.alert_count, 1);
+        assert_eq!(r.alerts[0].alert_type, DoorAlertType::OpenTooLong);
+    }
+    #[test]
+    fn test_opened_at_night() {
+        let mut w = DoorWatch::new();
+        w.register_contact(make_config(1, 10));
+        let r = w.process_event(1, true, 82800);
+        assert_eq!(r.alert_count, 1);
+        assert_eq!(r.alerts[0].alert_type, DoorAlertType::OpenedAtNight);
+    }
+    #[test]
+    fn test_normal_day() {
+        let mut w = DoorWatch::new();
+        w.register_contact(make_config(1, 10));
+        let r = w.process_event(1, true, 50400);
+        assert_eq!(r.alert_count, 0);
+    }
+    #[test]
+    fn test_unknown_contact() {
+        let mut w = DoorWatch::new();
+        let r = w.process_event(99, true, 1000);
+        assert_eq!(r.alert_count, 0);
+    }
+    #[test]
+    fn test_multiple_contacts() {
+        let mut w = DoorWatch::new();
+        w.register_contact(make_config(1, 10));
+        w.register_contact(make_config(2, 20));
+        w.process_event(1, true, 43200);
+        w.process_event(2, true, 43200);
+        let r = w.check_timeouts(43200 + 400);
+        assert_eq!(r.alert_count, 2);
+    }
 }
 
 // ── Kani bounded model checking harnesses ────────────────────
diff --git a/crates/wohl-hub/Cargo.toml b/crates/wohl-hub/Cargo.toml
index bdf4deb..4c2f724 100644
--- a/crates/wohl-hub/Cargo.toml
+++ b/crates/wohl-hub/Cargo.toml
@@ -28,8 +28,12 @@ relay-hk.workspace = true
 relay-tbl.workspace = true
 relay-cs.workspace = true
 relay-to.workspace = true
+relay-ccsds.workspace = true
 
 # Runtime
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"
 toml = "0.8"
+
+[lints]
+workspace = true
diff --git a/crates/wohl-hub/src/main.rs b/crates/wohl-hub/src/main.rs
index cee3bb1..f9f3425 100644
--- a/crates/wohl-hub/src/main.rs
+++ b/crates/wohl-hub/src/main.rs
@@ -2,13 +2,21 @@
 //!
 //! Reads sensor data from stdin (JSON lines), routes through monitors,
 //! dispatches alerts through dedup/rate-limiter, prints alerts to stdout.
+//!
+//! With `--ccsds` (or `WOHL_INPUT=ccsds`), reads binary CCSDS sensor packets
+//! instead — 14 bytes per reading, matching what Wohl sensor nodes emit.
 
-use std::io::BufRead;
+use std::io::{BufRead, Read};
 
+use relay_ccsds::sensor_wire;
 use serde::{Deserialize, Serialize};
 
 // ── Configuration types ────────────────────────────────────────
 
+#[allow(
+    dead_code,
+    reason = "TOML schema; `scheduler` wired when firmware-AADL scheduler thread lands, `alerts` wired by Track D (wohl-alert Verus dedup)"
+)]
 #[derive(Deserialize, Clone, Debug)]
 struct HubConfig {
     scheduler: Option<SchedulerConfig>,
@@ -19,11 +27,19 @@ struct HubConfig {
     alerts: Option<AlertConfig>,
 }
 
+#[allow(
+    dead_code,
+    reason = "wired when scheduler thread (spar/wohl_system.aadl:207) lands"
+)]
 #[derive(Deserialize, Clone, Debug)]
 struct SchedulerConfig {
     tick_rate_ms: Option<u32>,
 }
 
+#[allow(
+    dead_code,
+    reason = "TOML schema; `name` is for CLI display, remaining fields are mostly already consumed"
+)]
 #[derive(Deserialize, Clone, Debug)]
 struct ZoneConfig {
     id: u32,
@@ -39,6 +55,7 @@ struct ZoneConfig {
     power_spike: Option<u32>,
 }
 
+#[allow(dead_code, reason = "TOML schema; `name` is for CLI display")]
 #[derive(Deserialize, Clone, Debug)]
 struct ContactConfigToml {
     id: u32,
@@ -49,6 +66,10 @@ struct ContactConfigToml {
     night_end: Option<u8>,
 }
 
+#[allow(
+    dead_code,
+    reason = "Track D: rate_limit_per_minute and dedup_cooldown_sec will be applied to AlertDispatcher when the Verus dedup invariant work lands"
+)]
 #[derive(Deserialize, Clone, Debug)]
 struct AlertConfig {
     rate_limit_per_minute: Option<u32>,
@@ -65,7 +86,13 @@ enum SensorEvent {
     #[serde(rename = "water")]
     Water { zone: u32, wet: bool, time: u64 },
     #[serde(rename = "air")]
-    Air { zone: u32, co2: u32, pm25: Option<u32>, voc: Option<u32>, time: u64 },
+    Air {
+        zone: u32,
+        co2: u32,
+        pm25: Option<u32>,
+        voc: Option<u32>,
+        time: u64,
+    },
     #[serde(rename = "contact")]
     Contact { id: u32, open: bool, time: u64 },
     #[serde(rename = "power")]
@@ -111,6 +138,10 @@ const ALERT_DOOR_OPEN_TOO_LONG: u8 = 12;
 const ALERT_DOOR_NIGHT: u8 = 13;
 const ALERT_OVERCONSUMPTION: u8 = 14;
 const ALERT_POWER_SPIKE: u8 = 15;
+#[allow(
+    dead_code,
+    reason = "reserved alert ID slot for upcoming health-monitor work; deleting would collapse the audit-trail numbering"
+)]
 const ALERT_HEALTH_MISS: u8 = 16;
 
 // ── Monitor app IDs for health tracking ────────────────────────
@@ -254,23 +285,29 @@ impl WohlHub {
 
             // Track contact -> zone mapping
             if (self.contact_zone_count as usize) < self.contact_zones.len() {
-                self.contact_zones[self.contact_zone_count as usize] =
-                    (contact.id, contact.zone);
+                self.contact_zones[self.contact_zone_count as usize] = (contact.id, contact.zone);
                 self.contact_zone_count += 1;
             }
 
             // Subscribe door alert types for the contact's zone
-            self.alert.subscribe(contact.zone, ALERT_DOOR_OPEN_TOO_LONG, 1);
+            self.alert
+                .subscribe(contact.zone, ALERT_DOOR_OPEN_TOO_LONG, 1);
             self.alert.subscribe(contact.zone, ALERT_DOOR_NIGHT, 1);
         }
 
         // Register health monitors for each app
-        self.health.register_app(APP_TEMP, 3, relay_hs::engine::HsAction::Event);
-        self.health.register_app(APP_LEAK, 3, relay_hs::engine::HsAction::Event);
-        self.health.register_app(APP_AIR, 3, relay_hs::engine::HsAction::Event);
-        self.health.register_app(APP_DOOR, 3, relay_hs::engine::HsAction::Event);
-        self.health.register_app(APP_POWER, 3, relay_hs::engine::HsAction::Event);
-        self.health.register_app(APP_SCHEDULER, 3, relay_hs::engine::HsAction::Event);
+        self.health
+            .register_app(APP_TEMP, 3, relay_hs::engine::HsAction::Event);
+        self.health
+            .register_app(APP_LEAK, 3, relay_hs::engine::HsAction::Event);
+        self.health
+            .register_app(APP_AIR, 3, relay_hs::engine::HsAction::Event);
+        self.health
+            .register_app(APP_DOOR, 3, relay_hs::engine::HsAction::Event);
+        self.health
+            .register_app(APP_POWER, 3, relay_hs::engine::HsAction::Event);
+        self.health
+            .register_app(APP_SCHEDULER, 3, relay_hs::engine::HsAction::Event);
 
         // Set up scheduler slot: minor_frame=0, major_frame=0 (every tick)
         // Channel 1 = health check, Channel 2 = door timeout check
@@ -305,15 +342,6 @@ impl WohlHub {
         self.checksummer.register_region(1, config_crc);
     }
 
-    fn contact_zone(&self, contact_id: u32) -> u32 {
-        for i in 0..self.contact_zone_count as usize {
-            if self.contact_zones[i].0 == contact_id {
-                return self.contact_zones[i].1;
-            }
-        }
-        0
-    }
-
     fn try_dispatch(&mut self, zone_id: u32, alert_type: u8, time: u64) -> bool {
         let result = self.alert.process_alert(zone_id, alert_type, time);
         result.action == wohl_alert::engine::DispatchAction::Send
@@ -325,7 +353,8 @@ impl WohlHub {
         match event {
             SensorEvent::Temp { zone, value, time } => {
                 self.monitor_counters[0] += 1;
-                self.health.update_counter(APP_TEMP, self.monitor_counters[0]);
+                self.health
+                    .update_counter(APP_TEMP, self.monitor_counters[0]);
 
                 let result = self.temp.process_reading(zone, value, time);
                 for i in 0..result.alert_count as usize {
@@ -333,8 +362,12 @@ impl WohlHub {
                     let (alert_name, alert_code) = match a.alert_type {
                         wohl_temp::engine::TempAlertType::Freeze => ("freeze", ALERT_FREEZE),
                         wohl_temp::engine::TempAlertType::Overheat => ("overheat", ALERT_OVERHEAT),
-                        wohl_temp::engine::TempAlertType::RapidDrop => ("rapid_drop", ALERT_RAPID_DROP),
-                        wohl_temp::engine::TempAlertType::RapidRise => ("rapid_rise", ALERT_RAPID_RISE),
+                        wohl_temp::engine::TempAlertType::RapidDrop => {
+                            ("rapid_drop", ALERT_RAPID_DROP)
+                        }
+                        wohl_temp::engine::TempAlertType::RapidRise => {
+                            ("rapid_rise", ALERT_RAPID_RISE)
+                        }
                     };
                     if self.try_dispatch(zone, alert_code, time) {
                         alerts.push(AlertOutput {
@@ -353,28 +386,36 @@ impl WohlHub {
 
             SensorEvent::Water { zone, wet, time } => {
                 self.monitor_counters[1] += 1;
-                self.health.update_counter(APP_LEAK, self.monitor_counters[1]);
+                self.health
+                    .update_counter(APP_LEAK, self.monitor_counters[1]);
 
                 let action = self.leak.process_event(zone, wet, time);
-                if action == wohl_leak::engine::LeakAction::NewLeak {
-                    if self.try_dispatch(zone, ALERT_WATER_LEAK, time) {
-                        alerts.push(AlertOutput {
-                            alert: "water_leak".to_string(),
-                            zone: Some(zone),
-                            circuit: None,
-                            contact: None,
-                            value: None,
-                            threshold: None,
-                            duration: None,
-                            time,
-                        });
-                    }
+                if action == wohl_leak::engine::LeakAction::NewLeak
+                    && self.try_dispatch(zone, ALERT_WATER_LEAK, time)
+                {
+                    alerts.push(AlertOutput {
+                        alert: "water_leak".to_string(),
+                        zone: Some(zone),
+                        circuit: None,
+                        contact: None,
+                        value: None,
+                        threshold: None,
+                        duration: None,
+                        time,
+                    });
                 }
             }
 
-            SensorEvent::Air { zone, co2, pm25, voc, time } => {
+            SensorEvent::Air {
+                zone,
+                co2,
+                pm25,
+                voc,
+                time,
+            } => {
                 self.monitor_counters[2] += 1;
-                self.health.update_counter(APP_AIR, self.monitor_counters[2]);
+                self.health
+                    .update_counter(APP_AIR, self.monitor_counters[2]);
 
                 let reading = wohl_air::engine::AirReading {
                     zone_id: zone,
@@ -387,12 +428,24 @@ impl WohlHub {
                 for i in 0..result.alert_count as usize {
                     let a = &result.alerts[i];
                     let (alert_name, alert_code) = match a.alert_type {
-                        wohl_air::engine::AirAlertType::Co2Warning => ("co2_warning", ALERT_CO2_WARNING),
-                        wohl_air::engine::AirAlertType::Co2Critical => ("co2_critical", ALERT_CO2_CRITICAL),
-                        wohl_air::engine::AirAlertType::Pm25Warning => ("pm25_warning", ALERT_PM25_WARNING),
-                        wohl_air::engine::AirAlertType::Pm25Critical => ("pm25_critical", ALERT_PM25_CRITICAL),
-                        wohl_air::engine::AirAlertType::VocWarning => ("voc_warning", ALERT_VOC_WARNING),
-                        wohl_air::engine::AirAlertType::VocCritical => ("voc_critical", ALERT_VOC_CRITICAL),
+                        wohl_air::engine::AirAlertType::Co2Warning => {
+                            ("co2_warning", ALERT_CO2_WARNING)
+                        }
+                        wohl_air::engine::AirAlertType::Co2Critical => {
+                            ("co2_critical", ALERT_CO2_CRITICAL)
+                        }
+                        wohl_air::engine::AirAlertType::Pm25Warning => {
+                            ("pm25_warning", ALERT_PM25_WARNING)
+                        }
+                        wohl_air::engine::AirAlertType::Pm25Critical => {
+                            ("pm25_critical", ALERT_PM25_CRITICAL)
+                        }
+                        wohl_air::engine::AirAlertType::VocWarning => {
+                            ("voc_warning", ALERT_VOC_WARNING)
+                        }
+                        wohl_air::engine::AirAlertType::VocCritical => {
+                            ("voc_critical", ALERT_VOC_CRITICAL)
+                        }
                     };
                     if self.try_dispatch(zone, alert_code, time) {
                         alerts.push(AlertOutput {
@@ -411,7 +464,8 @@ impl WohlHub {
 
             SensorEvent::Contact { id, open, time } => {
                 self.monitor_counters[3] += 1;
-                self.health.update_counter(APP_DOOR, self.monitor_counters[3]);
+                self.health
+                    .update_counter(APP_DOOR, self.monitor_counters[3]);
 
                 let result = self.door.process_event(id, open, time);
                 for i in 0..result.alert_count as usize {
@@ -440,9 +494,14 @@ impl WohlHub {
                 }
             }
 
-            SensorEvent::Power { circuit, watts, time } => {
+            SensorEvent::Power {
+                circuit,
+                watts,
+                time,
+            } => {
                 self.monitor_counters[4] += 1;
-                self.health.update_counter(APP_POWER, self.monitor_counters[4]);
+                self.health
+                    .update_counter(APP_POWER, self.monitor_counters[4]);
 
                 let result = self.power.process_reading(circuit, watts, time);
                 for i in 0..result.alert_count as usize {
@@ -476,7 +535,8 @@ impl WohlHub {
 
             SensorEvent::Tick { time } => {
                 self.monitor_counters[5] += 1;
-                self.health.update_counter(APP_SCHEDULER, self.monitor_counters[5]);
+                self.health
+                    .update_counter(APP_SCHEDULER, self.monitor_counters[5]);
                 self.last_tick = time;
 
                 // Compute minor frame from time (wrapping tick counter)
@@ -511,11 +571,7 @@ impl WohlHub {
                             for j in 0..door_result.alert_count as usize {
                                 let da = &door_result.alerts[j];
                                 let zone = da.zone_id;
-                                if self.try_dispatch(
-                                    zone,
-                                    ALERT_DOOR_OPEN_TOO_LONG,
-                                    time,
-                                ) {
+                                if self.try_dispatch(zone, ALERT_DOOR_OPEN_TOO_LONG, time) {
                                     alerts.push(AlertOutput {
                                         alert: "door_open_too_long".to_string(),
                                         zone: Some(zone),
@@ -623,16 +679,101 @@ fn default_config() -> HubConfig {
     }
 }
 
+#[cfg(test)]
 fn config_from_str(s: &str) -> Result<HubConfig, toml::de::Error> {
     toml::from_str(s)
 }
 
-// ── Main ───────────────────────────────────────────────────────
+// ── CCSDS sensor packet → SensorEvent mapping ──────────────────
+
+/// Translate a decoded CCSDS sensor packet into a wohl-hub SensorEvent.
+///
+/// `time` is supplied by the caller (usually wall-clock seconds on arrival)
+/// since CCSDS packets don't carry a timestamp field.
+/// Returns None for sensor types the hub does not currently handle.
+fn packet_to_event(pkt: &sensor_wire::SensorPacket, time: u64) -> Option<SensorEvent> {
+    match pkt.sensor_type {
+        sensor_wire::SENSOR_TEMP => Some(SensorEvent::Temp {
+            zone: pkt.zone_id as u32,
+            value: pkt.value,
+            time,
+        }),
+        sensor_wire::SENSOR_WATER => Some(SensorEvent::Water {
+            zone: pkt.zone_id as u32,
+            wet: pkt.value != 0,
+            time,
+        }),
+        sensor_wire::SENSOR_CONTACT => Some(SensorEvent::Contact {
+            // device_id is the physical contact identifier
+            id: pkt.device_id as u32,
+            open: pkt.value != 0,
+            time,
+        }),
+        sensor_wire::SENSOR_CO2 => Some(SensorEvent::Air {
+            zone: pkt.zone_id as u32,
+            co2: pkt.value.max(0) as u32,
+            pm25: None,
+            voc: None,
+            time,
+        }),
+        sensor_wire::SENSOR_POWER => Some(SensorEvent::Power {
+            // device_id is the circuit identifier
+            circuit: pkt.device_id as u32,
+            watts: (pkt.value.max(0) / 10) as u32, // value is watts × 10
+            time,
+        }),
+        // PM25, VOC, HUMIDITY, MOTION, ENERGY, LUX, PRESSURE, WIND, RAIN
+        // not yet wired to monitors — dropped silently.
+        _ => None,
+    }
+}
 
-fn main() {
-    let config = load_config();
-    let mut hub = WohlHub::new(&config);
+fn now_seconds() -> u64 {
+    std::time::SystemTime::now()
+        .duration_since(std::time::UNIX_EPOCH)
+        .map(|d| d.as_secs())
+        .unwrap_or(0)
+}
+
+fn run_ccsds_mode(hub: &mut WohlHub) {
+    eprintln!("[wohl-hub] ready — reading CCSDS sensor packets from stdin (14 bytes each)");
+
+    let mut stdin = std::io::stdin().lock();
+    let mut buf = [0u8; sensor_wire::PACKET_SIZE];
+
+    loop {
+        match stdin.read_exact(&mut buf) {
+            Ok(()) => {}
+            Err(e) if e.kind() == std::io::ErrorKind::UnexpectedEof => break,
+            Err(e) => {
+                eprintln!("[wohl-hub] stdin error: {}", e);
+                break;
+            }
+        }
+
+        let pkt = match sensor_wire::decode_packet(&buf) {
+            Ok(p) => p,
+            Err(e) => {
+                eprintln!("[wohl-hub] ccsds decode error: {:?}", e);
+                continue;
+            }
+        };
+
+        let Some(event) = packet_to_event(&pkt, now_seconds()) else {
+            continue;
+        };
+
+        let alerts = hub.process_event(event);
+        for alert in &alerts {
+            match serde_json::to_string(alert) {
+                Ok(json) => println!("{}", json),
+                Err(e) => eprintln!("[wohl-hub] serialize error: {}", e),
+            }
+        }
+    }
+}
 
+fn run_json_mode(hub: &mut WohlHub) {
     eprintln!("[wohl-hub] ready — reading sensor events from stdin");
 
     let stdin = std::io::stdin();
@@ -666,6 +807,26 @@ fn main() {
             }
         }
     }
+}
+
+fn input_mode_is_ccsds() -> bool {
+    if std::env::args().any(|a| a == "--ccsds") {
+        return true;
+    }
+    matches!(std::env::var("WOHL_INPUT").as_deref(), Ok("ccsds"))
+}
+
+// ── Main ───────────────────────────────────────────────────────
+
+fn main() {
+    let config = load_config();
+    let mut hub = WohlHub::new(&config);
+
+    if input_mode_is_ccsds() {
+        run_ccsds_mode(&mut hub);
+    } else {
+        run_json_mode(&mut hub);
+    }
 
     eprintln!("[wohl-hub] done");
 }
@@ -869,10 +1030,7 @@ dedup_cooldown_sec = 60
             time: 1004,
         };
         let alerts = hub.process_event(event);
-        assert!(
-            alerts.is_empty(),
-            "normal power should produce no alert"
-        );
+        assert!(alerts.is_empty(), "normal power should produce no alert");
     }
 
     #[test]
@@ -899,9 +1057,7 @@ dedup_cooldown_sec = 60
         // Actually: minor = (time / 1000) % 60. For minor=0, time must be
         // a multiple of 60000. Use time=360000: (360000/1000)%60 = 360%60 = 0.
         // Duration since door open: 360000 - 43200 = 316800 > 300 (the max_open_sec).
-        let alerts = hub.process_event(SensorEvent::Tick {
-            time: 360000,
-        });
+        let alerts = hub.process_event(SensorEvent::Tick { time: 360000 });
 
         // The tick drives scheduler, which checks door timeouts
         let door_alerts: Vec<_> = alerts
@@ -1020,10 +1176,7 @@ dedup_cooldown_sec = 60
         let alerts = hub.process_event(SensorEvent::Tick { time: 1000 });
 
         // Health check should not produce alerts since monitors are active
-        let health_alerts: Vec<_> = alerts
-            .iter()
-            .filter(|a| a.alert == "health_miss")
-            .collect();
+        let health_alerts: Vec<_> = alerts.iter().filter(|a| a.alert == "health_miss").collect();
         // Some monitors (air, power, door) were not exercised,
         // but they start at 0/0 so first check increments miss counter.
         // With max_miss=3 they should not alert on first check.
@@ -1083,26 +1236,183 @@ dedup_cooldown_sec = 60
     fn test_sensor_event_parsing() {
         let temp: SensorEvent =
             serde_json::from_str(r#"{"type":"temp","zone":1,"value":2150,"time":1000}"#).unwrap();
-        assert!(matches!(temp, SensorEvent::Temp { zone: 1, value: 2150, time: 1000 }));
+        assert!(matches!(
+            temp,
+            SensorEvent::Temp {
+                zone: 1,
+                value: 2150,
+                time: 1000
+            }
+        ));
 
         let water: SensorEvent =
             serde_json::from_str(r#"{"type":"water","zone":2,"wet":true,"time":1001}"#).unwrap();
-        assert!(matches!(water, SensorEvent::Water { zone: 2, wet: true, time: 1001 }));
-
-        let air: SensorEvent =
-            serde_json::from_str(r#"{"type":"air","zone":1,"co2":1200,"pm25":50,"voc":30,"time":1002}"#).unwrap();
-        assert!(matches!(air, SensorEvent::Air { zone: 1, co2: 1200, .. }));
+        assert!(matches!(
+            water,
+            SensorEvent::Water {
+                zone: 2,
+                wet: true,
+                time: 1001
+            }
+        ));
+
+        let air: SensorEvent = serde_json::from_str(
+            r#"{"type":"air","zone":1,"co2":1200,"pm25":50,"voc":30,"time":1002}"#,
+        )
+        .unwrap();
+        assert!(matches!(
+            air,
+            SensorEvent::Air {
+                zone: 1,
+                co2: 1200,
+                ..
+            }
+        ));
 
         let contact: SensorEvent =
             serde_json::from_str(r#"{"type":"contact","id":1,"open":true,"time":1003}"#).unwrap();
-        assert!(matches!(contact, SensorEvent::Contact { id: 1, open: true, time: 1003 }));
+        assert!(matches!(
+            contact,
+            SensorEvent::Contact {
+                id: 1,
+                open: true,
+                time: 1003
+            }
+        ));
 
         let power: SensorEvent =
-            serde_json::from_str(r#"{"type":"power","circuit":1,"watts":1500,"time":1004}"#).unwrap();
-        assert!(matches!(power, SensorEvent::Power { circuit: 1, watts: 1500, time: 1004 }));
+            serde_json::from_str(r#"{"type":"power","circuit":1,"watts":1500,"time":1004}"#)
+                .unwrap();
+        assert!(matches!(
+            power,
+            SensorEvent::Power {
+                circuit: 1,
+                watts: 1500,
+                time: 1004
+            }
+        ));
 
-        let tick: SensorEvent =
-            serde_json::from_str(r#"{"type":"tick","time":2000}"#).unwrap();
+        let tick: SensorEvent = serde_json::from_str(r#"{"type":"tick","time":2000}"#).unwrap();
         assert!(matches!(tick, SensorEvent::Tick { time: 2000 }));
     }
+
+    #[test]
+    fn test_packet_to_event_temp() {
+        let pkt = sensor_wire::SensorPacket {
+            device_id: 10,
+            sequence: 0,
+            sensor_type: sensor_wire::SENSOR_TEMP,
+            quality: sensor_wire::QUALITY_GOOD,
+            zone_id: 1,
+            value: -100,
+        };
+        let ev = packet_to_event(&pkt, 500).unwrap();
+        assert!(matches!(
+            ev,
+            SensorEvent::Temp {
+                zone: 1,
+                value: -100,
+                time: 500
+            }
+        ));
+    }
+
+    #[test]
+    fn test_packet_to_event_water() {
+        let pkt = sensor_wire::SensorPacket {
+            device_id: 7,
+            sequence: 0,
+            sensor_type: sensor_wire::SENSOR_WATER,
+            quality: sensor_wire::QUALITY_GOOD,
+            zone_id: 2,
+            value: 1,
+        };
+        let ev = packet_to_event(&pkt, 900).unwrap();
+        assert!(matches!(
+            ev,
+            SensorEvent::Water {
+                zone: 2,
+                wet: true,
+                time: 900
+            }
+        ));
+    }
+
+    #[test]
+    fn test_packet_to_event_contact_uses_device_id() {
+        let pkt = sensor_wire::SensorPacket {
+            device_id: 42,
+            sequence: 0,
+            sensor_type: sensor_wire::SENSOR_CONTACT,
+            quality: sensor_wire::QUALITY_GOOD,
+            zone_id: 1,
+            value: 1,
+        };
+        let ev = packet_to_event(&pkt, 0).unwrap();
+        assert!(matches!(
+            ev,
+            SensorEvent::Contact {
+                id: 42,
+                open: true,
+                ..
+            }
+        ));
+    }
+
+    #[test]
+    fn test_packet_to_event_power_scales() {
+        let pkt = sensor_wire::SensorPacket {
+            device_id: 3,
+            sequence: 0,
+            sensor_type: sensor_wire::SENSOR_POWER,
+            quality: sensor_wire::QUALITY_GOOD,
+            zone_id: 1,
+            value: 15230, // 1523.0W × 10
+        };
+        let ev = packet_to_event(&pkt, 0).unwrap();
+        assert!(matches!(
+            ev,
+            SensorEvent::Power {
+                circuit: 3,
+                watts: 1523,
+                ..
+            }
+        ));
+    }
+
+    #[test]
+    fn test_packet_to_event_unknown_returns_none() {
+        let pkt = sensor_wire::SensorPacket {
+            device_id: 1,
+            sequence: 0,
+            sensor_type: sensor_wire::SENSOR_WIND,
+            quality: sensor_wire::QUALITY_GOOD,
+            zone_id: 1,
+            value: 0,
+        };
+        assert!(packet_to_event(&pkt, 0).is_none());
+    }
+
+    #[test]
+    fn test_end_to_end_ccsds_freeze() {
+        // Encode a below-freeze temp reading, decode, translate, feed to hub.
+        let pkt = sensor_wire::SensorPacket {
+            device_id: 10,
+            sequence: 0,
+            sensor_type: sensor_wire::SENSOR_TEMP,
+            quality: sensor_wire::QUALITY_GOOD,
+            zone_id: 1,
+            value: -100,
+        };
+        let mut buf = [0u8; sensor_wire::PACKET_SIZE];
+        sensor_wire::encode_packet(&pkt, &mut buf);
+        let decoded = sensor_wire::decode_packet(&buf).unwrap();
+        let event = packet_to_event(&decoded, 1000).unwrap();
+
+        let mut hub = test_hub();
+        let alerts = hub.process_event(event);
+        assert!(!alerts.is_empty());
+        assert_eq!(alerts[0].alert, "freeze");
+        assert_eq!(alerts[0].zone, Some(1));
+    }
 }
diff --git a/crates/wohl-integration/Cargo.toml b/crates/wohl-integration/Cargo.toml
index e56a604..f3d6240 100644
--- a/crates/wohl-integration/Cargo.toml
+++ b/crates/wohl-integration/Cargo.toml
@@ -19,3 +19,6 @@ wohl-air.workspace = true
 wohl-door.workspace = true
 wohl-power.workspace = true
 wohl-alert.workspace = true
+
+[lints]
+workspace = true
diff --git a/crates/wohl-integration/src/lib.rs b/crates/wohl-integration/src/lib.rs
index d3106ce..6fb751b 100644
--- a/crates/wohl-integration/src/lib.rs
+++ b/crates/wohl-integration/src/lib.rs
@@ -5,12 +5,12 @@
 
 #[cfg(test)]
 mod tests {
-    use wohl_temp::engine::{TemperatureMonitor, ZoneConfig as TempZoneConfig, TempAlertType};
-    use wohl_leak::engine::{LeakDetector, LeakAction};
-    use wohl_air::engine::{AirMonitor, AirConfig, AirReading, AirAlertType};
-    use wohl_door::engine::{DoorWatch, ContactConfig, DoorAlertType};
-    use wohl_power::engine::{PowerMonitor, CircuitConfig, PowerAlertType};
+    use wohl_air::engine::{AirAlertType, AirConfig, AirMonitor, AirReading};
     use wohl_alert::engine::{AlertDispatcher, DispatchAction};
+    use wohl_door::engine::{ContactConfig, DoorAlertType, DoorWatch};
+    use wohl_leak::engine::{LeakAction, LeakDetector};
+    use wohl_power::engine::{CircuitConfig, PowerAlertType, PowerMonitor};
+    use wohl_temp::engine::{TempAlertType, TemperatureMonitor, ZoneConfig as TempZoneConfig};
 
     // ── Alert type encoding constants ──
     // These map component alert types to u8 values for the dispatcher.
@@ -43,9 +43,9 @@ mod tests {
             let mut temp = TemperatureMonitor::new();
             temp.register_zone(TempZoneConfig {
                 zone_id: 1,
-                freeze_threshold: 0,        // 0.00 C
-                overheat_threshold: 4000,    // 40.00 C
-                rate_threshold: 500,         // 5.00 C/reading
+                freeze_threshold: 0,      // 0.00 C
+                overheat_threshold: 4000, // 40.00 C
+                rate_threshold: 500,      // 5.00 C/reading
                 enabled: true,
             });
 
@@ -87,16 +87,32 @@ mod tests {
             let mut dispatcher = AlertDispatcher::new();
             // Subscribe all alert types for zone 1 and zone 2
             for &at in &[
-                ALERT_FREEZE, ALERT_OVERHEAT, ALERT_RAPID_DROP, ALERT_RAPID_RISE,
-                ALERT_LEAK, ALERT_CO2_WARN, ALERT_CO2_CRIT, ALERT_PM25_WARN,
-                ALERT_VOC_WARN, ALERT_DOOR_NIGHT, ALERT_DOOR_LONG,
-                ALERT_POWER_OVER, ALERT_POWER_SPIKE,
+                ALERT_FREEZE,
+                ALERT_OVERHEAT,
+                ALERT_RAPID_DROP,
+                ALERT_RAPID_RISE,
+                ALERT_LEAK,
+                ALERT_CO2_WARN,
+                ALERT_CO2_CRIT,
+                ALERT_PM25_WARN,
+                ALERT_VOC_WARN,
+                ALERT_DOOR_NIGHT,
+                ALERT_DOOR_LONG,
+                ALERT_POWER_OVER,
+                ALERT_POWER_SPIKE,
             ] {
                 dispatcher.subscribe(1, at, 1);
                 dispatcher.subscribe(2, at, 1);
             }
 
-            Pipeline { temp, leak, air, door, power, dispatcher }
+            Pipeline {
+                temp,
+                leak,
+                air,
+                door,
+                power,
+                dispatcher,
+            }
         }
     }
 
@@ -118,7 +134,11 @@ mod tests {
 
         // Normal air quality
         let air_result = p.air.process_reading(AirReading {
-            zone_id: 1, co2_ppm: 400, pm25: 50, voc_index: 30, time: 1000,
+            zone_id: 1,
+            co2_ppm: 400,
+            pm25: 50,
+            voc_index: 30,
+            time: 1000,
         });
         assert_eq!(air_result.alert_count, 0);
 
@@ -190,7 +210,11 @@ mod tests {
 
         // High CO2 (1200 ppm, above 1000 warn threshold)
         let air_result = p.air.process_reading(AirReading {
-            zone_id: 1, co2_ppm: 1200, pm25: 50, voc_index: 30, time: 2000,
+            zone_id: 1,
+            co2_ppm: 1200,
+            pm25: 50,
+            voc_index: 30,
+            time: 2000,
         });
         assert!(air_result.alert_count >= 1);
         assert_eq!(air_result.alerts[0].alert_type, AirAlertType::Co2Warning);
@@ -226,8 +250,13 @@ mod tests {
 
         for (zone, atype) in alert_combos.iter() {
             let r = p.dispatcher.process_alert(*zone, *atype, base_time);
-            assert_eq!(r.action, DispatchAction::Send,
-                "alert ({}, {}) should have been sent", zone, atype);
+            assert_eq!(
+                r.action,
+                DispatchAction::Send,
+                "alert ({}, {}) should have been sent",
+                zone,
+                atype
+            );
         }
 
         // 11th alert in same minute -> rate limited
@@ -235,7 +264,9 @@ mod tests {
         assert_eq!(r.action, DispatchAction::RateLimited);
 
         // After the minute window resets, alerts flow again
-        let r = p.dispatcher.process_alert(1, ALERT_POWER_OVER, base_time + 61);
+        let r = p
+            .dispatcher
+            .process_alert(1, ALERT_POWER_OVER, base_time + 61);
         assert_eq!(r.action, DispatchAction::Send);
     }
 
@@ -251,7 +282,10 @@ mod tests {
         // 23:00 = 82800 seconds from midnight
         let door_result = p.door.process_event(1, true, 82800);
         assert_eq!(door_result.alert_count, 1);
-        assert_eq!(door_result.alerts[0].alert_type, DoorAlertType::OpenedAtNight);
+        assert_eq!(
+            door_result.alerts[0].alert_type,
+            DoorAlertType::OpenedAtNight
+        );
 
         // Route through dispatcher
         let dispatch = p.dispatcher.process_alert(
@@ -285,8 +319,11 @@ mod tests {
         // Overheat still subscribed — use a fresh monitor to avoid rate-of-change
         let mut temp2 = TemperatureMonitor::new();
         temp2.register_zone(TempZoneConfig {
-            zone_id: 1, freeze_threshold: 0, overheat_threshold: 4000,
-            rate_threshold: 500, enabled: true,
+            zone_id: 1,
+            freeze_threshold: 0,
+            overheat_threshold: 4000,
+            rate_threshold: 500,
+            enabled: true,
         });
         let temp_result2 = temp2.process_reading(1, 4500, 3100);
         assert!(temp_result2.alert_count >= 1);
@@ -314,7 +351,11 @@ mod tests {
 
         // High CO2
         let air_r = p.air.process_reading(AirReading {
-            zone_id: 1, co2_ppm: 2500, pm25: 50, voc_index: 30, time,
+            zone_id: 1,
+            co2_ppm: 2500,
+            pm25: 50,
+            voc_index: 30,
+            time,
         });
         assert!(air_r.alert_count >= 1);
 
@@ -408,11 +449,9 @@ mod tests {
         assert_eq!(timeout_r.alerts[0].alert_type, DoorAlertType::OpenTooLong);
 
         // Route through dispatcher
-        let dispatch = p.dispatcher.process_alert(
-            timeout_r.alerts[0].zone_id,
-            ALERT_DOOR_LONG,
-            43200 + 400,
-        );
+        let dispatch =
+            p.dispatcher
+                .process_alert(timeout_r.alerts[0].zone_id, ALERT_DOOR_LONG, 43200 + 400);
         assert_eq!(dispatch.action, DispatchAction::Send);
     }
 
@@ -448,7 +487,7 @@ mod tests {
                     DispatchAction::Send => total_alerts += 1,
                     DispatchAction::Deduplicated => total_dedups += 1,
                     DispatchAction::RateLimited => _total_rate_limited += 1,
-                    DispatchAction::NotSubscribed => {},
+                    DispatchAction::NotSubscribed => {}
                 }
             }
         }
@@ -499,7 +538,11 @@ mod tests {
 
         // t=1300: CO2 rises
         let r = p.air.process_reading(AirReading {
-            zone_id: 1, co2_ppm: 1500, pm25: 50, voc_index: 30, time: 1300,
+            zone_id: 1,
+            co2_ppm: 1500,
+            pm25: 50,
+            voc_index: 30,
+            time: 1300,
         });
         assert!(r.alert_count >= 1);
         let d = p.dispatcher.process_alert(1, ALERT_CO2_WARN, 1300);
diff --git a/crates/wohl-leak/Cargo.toml b/crates/wohl-leak/Cargo.toml
index 6277594..890aade 100644
--- a/crates/wohl-leak/Cargo.toml
+++ b/crates/wohl-leak/Cargo.toml
@@ -12,3 +12,6 @@ crate-type = ["rlib"]
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true
diff --git a/crates/wohl-leak/plain/src/engine.rs b/crates/wohl-leak/plain/src/engine.rs
index 4629f74..8ca7286 100644
--- a/crates/wohl-leak/plain/src/engine.rs
+++ b/crates/wohl-leak/plain/src/engine.rs
@@ -4,25 +4,64 @@
 pub const MAX_ZONES: usize = 32;
 
 #[derive(Clone, Copy)]
-pub struct ZoneState { pub zone_id: u32, pub wet: bool, pub detected_at: u64, pub active: bool }
+pub struct ZoneState {
+    pub zone_id: u32,
+    pub wet: bool,
+    pub detected_at: u64,
+    pub active: bool,
+}
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub enum LeakAction { NewLeak, AlreadyWet, Cleared, AlreadyDry, Unknown }
+pub enum LeakAction {
+    NewLeak,
+    AlreadyWet,
+    Cleared,
+    AlreadyDry,
+    Unknown,
+}
 
-pub struct LeakDetector { zones: [ZoneState; MAX_ZONES], zone_count: u32 }
+pub struct LeakDetector {
+    zones: [ZoneState; MAX_ZONES],
+    zone_count: u32,
+}
 
 impl ZoneState {
-    pub const fn empty() -> Self { ZoneState { zone_id: 0, wet: false, detected_at: 0, active: false } }
+    pub const fn empty() -> Self {
+        ZoneState {
+            zone_id: 0,
+            wet: false,
+            detected_at: 0,
+            active: false,
+        }
+    }
+}
+
+impl Default for LeakDetector {
+    fn default() -> Self {
+        Self::new()
+    }
 }
 
 impl LeakDetector {
-    pub fn new() -> Self { LeakDetector { zones: [ZoneState::empty(); MAX_ZONES], zone_count: 0 } }
+    pub fn new() -> Self {
+        LeakDetector {
+            zones: [ZoneState::empty(); MAX_ZONES],
+            zone_count: 0,
+        }
+    }
 
     pub fn register_zone(&mut self, zone_id: u32) -> bool {
-        if self.zone_count as usize >= MAX_ZONES { return false; }
+        if self.zone_count as usize >= MAX_ZONES {
+            return false;
+        }
         let idx = self.zone_count as usize;
-        self.zones[idx] = ZoneState { zone_id, wet: false, detected_at: 0, active: true };
-        self.zone_count = self.zone_count + 1;
+        self.zones[idx] = ZoneState {
+            zone_id,
+            wet: false,
+            detected_at: 0,
+            active: true,
+        };
+        self.zone_count += 1;
         true
     }
 
@@ -34,14 +73,23 @@ impl LeakDetector {
             if self.zones[idx].active && self.zones[idx].zone_id == zone_id {
                 let was_wet = self.zones[idx].wet;
                 if wet {
-                    if was_wet { return LeakAction::AlreadyWet; }
-                    else { self.zones[idx].wet = true; self.zones[idx].detected_at = timestamp_sec; return LeakAction::NewLeak; }
+                    if was_wet {
+                        return LeakAction::AlreadyWet;
+                    } else {
+                        self.zones[idx].wet = true;
+                        self.zones[idx].detected_at = timestamp_sec;
+                        return LeakAction::NewLeak;
+                    }
                 } else {
-                    if was_wet { self.zones[idx].wet = false; return LeakAction::Cleared; }
-                    else { return LeakAction::AlreadyDry; }
+                    if was_wet {
+                        self.zones[idx].wet = false;
+                        return LeakAction::Cleared;
+                    } else {
+                        return LeakAction::AlreadyDry;
+                    }
                 }
             }
-            i = i + 1;
+            i += 1;
         }
         LeakAction::Unknown
     }
@@ -50,8 +98,10 @@ impl LeakDetector {
         let count = self.zone_count;
         let mut i: u32 = 0;
         while i < count {
-            if self.zones[i as usize].active && self.zones[i as usize].wet { return true; }
-            i = i + 1;
+            if self.zones[i as usize].active && self.zones[i as usize].wet {
+                return true;
+            }
+            i += 1;
         }
         false
     }
@@ -60,13 +110,52 @@ impl LeakDetector {
 #[cfg(test)]
 mod tests {
     use super::*;
-    #[test] fn test_new_leak() { let mut d = LeakDetector::new(); d.register_zone(1); assert_eq!(d.process_event(1, true, 1000), LeakAction::NewLeak); }
-    #[test] fn test_already_wet() { let mut d = LeakDetector::new(); d.register_zone(1); d.process_event(1, true, 1000); assert_eq!(d.process_event(1, true, 1001), LeakAction::AlreadyWet); }
-    #[test] fn test_cleared() { let mut d = LeakDetector::new(); d.register_zone(1); d.process_event(1, true, 1000); assert_eq!(d.process_event(1, false, 2000), LeakAction::Cleared); }
-    #[test] fn test_no_auto_clear() { let mut d = LeakDetector::new(); d.register_zone(1); d.process_event(1, true, 1000); assert!(d.any_wet()); }
-    #[test] fn test_unknown() { let mut d = LeakDetector::new(); assert_eq!(d.process_event(99, true, 1000), LeakAction::Unknown); }
-    #[test] fn test_multi_zone() { let mut d = LeakDetector::new(); d.register_zone(1); d.register_zone(2); assert_eq!(d.process_event(2, true, 100), LeakAction::NewLeak); assert_eq!(d.process_event(2, false, 200), LeakAction::Cleared); }
-    #[test] fn test_already_dry() { let mut d = LeakDetector::new(); d.register_zone(1); assert_eq!(d.process_event(1, false, 1000), LeakAction::AlreadyDry); }
+    #[test]
+    fn test_new_leak() {
+        let mut d = LeakDetector::new();
+        d.register_zone(1);
+        assert_eq!(d.process_event(1, true, 1000), LeakAction::NewLeak);
+    }
+    #[test]
+    fn test_already_wet() {
+        let mut d = LeakDetector::new();
+        d.register_zone(1);
+        d.process_event(1, true, 1000);
+        assert_eq!(d.process_event(1, true, 1001), LeakAction::AlreadyWet);
+    }
+    #[test]
+    fn test_cleared() {
+        let mut d = LeakDetector::new();
+        d.register_zone(1);
+        d.process_event(1, true, 1000);
+        assert_eq!(d.process_event(1, false, 2000), LeakAction::Cleared);
+    }
+    #[test]
+    fn test_no_auto_clear() {
+        let mut d = LeakDetector::new();
+        d.register_zone(1);
+        d.process_event(1, true, 1000);
+        assert!(d.any_wet());
+    }
+    #[test]
+    fn test_unknown() {
+        let mut d = LeakDetector::new();
+        assert_eq!(d.process_event(99, true, 1000), LeakAction::Unknown);
+    }
+    #[test]
+    fn test_multi_zone() {
+        let mut d = LeakDetector::new();
+        d.register_zone(1);
+        d.register_zone(2);
+        assert_eq!(d.process_event(2, true, 100), LeakAction::NewLeak);
+        assert_eq!(d.process_event(2, false, 200), LeakAction::Cleared);
+    }
+    #[test]
+    fn test_already_dry() {
+        let mut d = LeakDetector::new();
+        d.register_zone(1);
+        assert_eq!(d.process_event(1, false, 1000), LeakAction::AlreadyDry);
+    }
 }
 
 #[cfg(test)]
diff --git a/crates/wohl-power/Cargo.toml b/crates/wohl-power/Cargo.toml
index 50f9e0b..83283cf 100644
--- a/crates/wohl-power/Cargo.toml
+++ b/crates/wohl-power/Cargo.toml
@@ -12,3 +12,6 @@ crate-type = ["rlib"]
 
 [dependencies]
 relay-lc.workspace = true
+
+[lints]
+workspace = true
diff --git a/crates/wohl-power/plain/src/engine.rs b/crates/wohl-power/plain/src/engine.rs
index 97a991b..a27146e 100644
--- a/crates/wohl-power/plain/src/engine.rs
+++ b/crates/wohl-power/plain/src/engine.rs
@@ -4,26 +4,48 @@
 //!   - relay-lc::WatchpointTable handles overconsumption threshold (VERIFIED)
 //!   - This module adds: spike detection (rate-of-change), domain types
 
-use relay_lc::engine::{
-    ComparisonOp, SensorReading, Watchpoint, WatchpointTable,
-};
+use relay_lc::engine::{ComparisonOp, SensorReading, Watchpoint, WatchpointTable};
 
 pub const MAX_CIRCUITS: usize = 16;
 pub const MAX_ALERTS_PER_READING: usize = 4;
 
 #[derive(Clone, Copy)]
-pub struct CircuitConfig { pub circuit_id: u32, pub max_watts: u32, pub idle_watts: u32, pub spike_threshold: u32, pub enabled: bool }
+pub struct CircuitConfig {
+    pub circuit_id: u32,
+    pub max_watts: u32,
+    pub idle_watts: u32,
+    pub spike_threshold: u32,
+    pub enabled: bool,
+}
 
 #[derive(Clone, Copy)]
-pub struct CircuitState { pub circuit_id: u32, pub last_watts: u32, pub last_time: u64, pub active: bool }
+pub struct CircuitState {
+    pub circuit_id: u32,
+    pub last_watts: u32,
+    pub last_time: u64,
+    pub active: bool,
+}
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub enum PowerAlertType { OverConsumption, Spike, DeviceLeftOn }
+pub enum PowerAlertType {
+    OverConsumption,
+    Spike,
+    DeviceLeftOn,
+}
 
 #[derive(Clone, Copy)]
-pub struct PowerAlert { pub circuit_id: u32, pub alert_type: PowerAlertType, pub value: u32, pub threshold: u32, pub time: u64 }
+pub struct PowerAlert {
+    pub circuit_id: u32,
+    pub alert_type: PowerAlertType,
+    pub value: u32,
+    pub threshold: u32,
+    pub time: u64,
+}
 
-pub struct PowerResult { pub alerts: [PowerAlert; MAX_ALERTS_PER_READING], pub alert_count: u32 }
+pub struct PowerResult {
+    pub alerts: [PowerAlert; MAX_ALERTS_PER_READING],
+    pub alert_count: u32,
+}
 
 pub struct PowerMonitor {
     watchpoints: WatchpointTable,
@@ -32,9 +54,44 @@ pub struct PowerMonitor {
     circuit_count: u32,
 }
 
-impl CircuitConfig { pub const fn empty() -> Self { CircuitConfig { circuit_id: 0, max_watts: 0, idle_watts: 0, spike_threshold: 0, enabled: false } } }
-impl CircuitState { pub const fn empty() -> Self { CircuitState { circuit_id: 0, last_watts: 0, last_time: 0, active: false } } }
-impl PowerAlert { pub const fn empty() -> Self { PowerAlert { circuit_id: 0, alert_type: PowerAlertType::OverConsumption, value: 0, threshold: 0, time: 0 } } }
+impl CircuitConfig {
+    pub const fn empty() -> Self {
+        CircuitConfig {
+            circuit_id: 0,
+            max_watts: 0,
+            idle_watts: 0,
+            spike_threshold: 0,
+            enabled: false,
+        }
+    }
+}
+impl CircuitState {
+    pub const fn empty() -> Self {
+        CircuitState {
+            circuit_id: 0,
+            last_watts: 0,
+            last_time: 0,
+            active: false,
+        }
+    }
+}
+impl PowerAlert {
+    pub const fn empty() -> Self {
+        PowerAlert {
+            circuit_id: 0,
+            alert_type: PowerAlertType::OverConsumption,
+            value: 0,
+            threshold: 0,
+            time: 0,
+        }
+    }
+}
+
+impl Default for PowerMonitor {
+    fn default() -> Self {
+        Self::new()
+    }
+}
 
 impl PowerMonitor {
     pub fn new() -> Self {
@@ -47,10 +104,17 @@ impl PowerMonitor {
     }
 
     pub fn register_circuit(&mut self, config: CircuitConfig) -> bool {
-        if self.circuit_count as usize >= MAX_CIRCUITS { return false; }
+        if self.circuit_count as usize >= MAX_CIRCUITS {
+            return false;
+        }
         let idx = self.circuit_count as usize;
         self.configs[idx] = config;
-        self.states[idx] = CircuitState { circuit_id: config.circuit_id, last_watts: 0, last_time: 0, active: true };
+        self.states[idx] = CircuitState {
+            circuit_id: config.circuit_id,
+            last_watts: 0,
+            last_time: 0,
+            active: true,
+        };
 
         // Overconsumption watchpoint via relay-lc (VERIFIED)
         self.watchpoints.add_watchpoint(Watchpoint {
@@ -67,14 +131,23 @@ impl PowerMonitor {
     }
 
     pub fn process_reading(&mut self, circuit_id: u32, watts: u32, time: u64) -> PowerResult {
-        let mut res = PowerResult { alerts: [PowerAlert::empty(); MAX_ALERTS_PER_READING], alert_count: 0 };
+        let mut res = PowerResult {
+            alerts: [PowerAlert::empty(); MAX_ALERTS_PER_READING],
+            alert_count: 0,
+        };
 
         // Phase 1: overconsumption via relay-lc (VERIFIED)
-        let oc_result = self.watchpoints.evaluate(SensorReading { sensor_id: circuit_id, value: watts as i64 });
+        let oc_result = self.watchpoints.evaluate(SensorReading {
+            sensor_id: circuit_id,
+            value: watts as i64,
+        });
         if oc_result.violation_count > 0 && (res.alert_count as usize) < MAX_ALERTS_PER_READING {
             res.alerts[res.alert_count as usize] = PowerAlert {
-                circuit_id, alert_type: PowerAlertType::OverConsumption,
-                value: watts, threshold: oc_result.violations[0].threshold as u32, time,
+                circuit_id,
+                alert_type: PowerAlertType::OverConsumption,
+                value: watts,
+                threshold: oc_result.violations[0].threshold as u32,
+                time,
             };
             res.alert_count += 1;
         }
@@ -84,14 +157,22 @@ impl PowerMonitor {
         let mut i: u32 = 0;
         while i < count {
             let idx = i as usize;
-            if self.states[idx].active && self.configs[idx].circuit_id == circuit_id && self.configs[idx].enabled {
+            if self.states[idx].active
+                && self.configs[idx].circuit_id == circuit_id
+                && self.configs[idx].enabled
+            {
                 if self.states[idx].last_time > 0 {
                     let last = self.states[idx].last_watts;
-                    let diff = if watts > last { watts - last } else { last - watts };
-                    if diff > self.configs[idx].spike_threshold && (res.alert_count as usize) < MAX_ALERTS_PER_READING {
+                    let diff = watts.abs_diff(last);
+                    if diff > self.configs[idx].spike_threshold
+                        && (res.alert_count as usize) < MAX_ALERTS_PER_READING
+                    {
                         res.alerts[res.alert_count as usize] = PowerAlert {
-                            circuit_id, alert_type: PowerAlertType::Spike,
-                            value: watts, threshold: self.configs[idx].spike_threshold, time,
+                            circuit_id,
+                            alert_type: PowerAlertType::Spike,
+                            value: watts,
+                            threshold: self.configs[idx].spike_threshold,
+                            time,
                         };
                         res.alert_count += 1;
                     }
@@ -110,7 +191,9 @@ impl PowerMonitor {
         let mut i: u32 = 0;
         while i < self.circuit_count {
             let idx = i as usize;
-            if self.configs[idx].circuit_id == circuit_id { return current_watts <= self.configs[idx].idle_watts; }
+            if self.configs[idx].circuit_id == circuit_id {
+                return current_watts <= self.configs[idx].idle_watts;
+            }
             i += 1;
         }
         false
@@ -122,30 +205,64 @@ mod tests {
     use super::*;
 
     fn make_config(id: u32) -> CircuitConfig {
-        CircuitConfig { circuit_id: id, max_watts: 30000, idle_watts: 100, spike_threshold: 10000, enabled: true }
+        CircuitConfig {
+            circuit_id: id,
+            max_watts: 30000,
+            idle_watts: 100,
+            spike_threshold: 10000,
+            enabled: true,
+        }
     }
 
-    #[test] fn test_empty() { let mut m = PowerMonitor::new(); let r = m.process_reading(1, 1000, 100); assert_eq!(r.alert_count, 0); }
+    #[test]
+    fn test_empty() {
+        let mut m = PowerMonitor::new();
+        let r = m.process_reading(1, 1000, 100);
+        assert_eq!(r.alert_count, 0);
+    }
 
-    #[test] fn test_overconsumption_via_relay_lc() {
-        let mut m = PowerMonitor::new(); m.register_circuit(make_config(1));
+    #[test]
+    fn test_overconsumption_via_relay_lc() {
+        let mut m = PowerMonitor::new();
+        m.register_circuit(make_config(1));
         let r = m.process_reading(1, 35000, 100);
         assert!(r.alert_count >= 1);
         assert_eq!(r.alerts[0].alert_type, PowerAlertType::OverConsumption);
     }
 
-    #[test] fn test_spike() {
-        let mut m = PowerMonitor::new(); m.register_circuit(make_config(1));
+    #[test]
+    fn test_spike() {
+        let mut m = PowerMonitor::new();
+        m.register_circuit(make_config(1));
         m.process_reading(1, 1000, 100);
         let r = m.process_reading(1, 15000, 200);
         let mut found = false;
-        for j in 0..r.alert_count as usize { if r.alerts[j].alert_type == PowerAlertType::Spike { found = true; } }
+        for j in 0..r.alert_count as usize {
+            if r.alerts[j].alert_type == PowerAlertType::Spike {
+                found = true;
+            }
+        }
         assert!(found);
     }
 
-    #[test] fn test_normal() { let mut m = PowerMonitor::new(); m.register_circuit(make_config(1)); assert_eq!(m.process_reading(1, 1500, 100).alert_count, 0); }
-    #[test] fn test_unknown() { let mut m = PowerMonitor::new(); assert_eq!(m.process_reading(99, 50000, 100).alert_count, 0); }
-    #[test] fn test_idle() { let mut m = PowerMonitor::new(); m.register_circuit(make_config(1)); assert!(m.check_idle(1, 50)); assert!(!m.check_idle(1, 200)); }
+    #[test]
+    fn test_normal() {
+        let mut m = PowerMonitor::new();
+        m.register_circuit(make_config(1));
+        assert_eq!(m.process_reading(1, 1500, 100).alert_count, 0);
+    }
+    #[test]
+    fn test_unknown() {
+        let mut m = PowerMonitor::new();
+        assert_eq!(m.process_reading(99, 50000, 100).alert_count, 0);
+    }
+    #[test]
+    fn test_idle() {
+        let mut m = PowerMonitor::new();
+        m.register_circuit(make_config(1));
+        assert!(m.check_idle(1, 50));
+        assert!(!m.check_idle(1, 200));
+    }
 }
 
 // ── Kani bounded model checking harnesses ────────────────────
diff --git a/crates/wohl-temp/Cargo.toml b/crates/wohl-temp/Cargo.toml
index 85b8ea8..993a709 100644
--- a/crates/wohl-temp/Cargo.toml
+++ b/crates/wohl-temp/Cargo.toml
@@ -15,3 +15,6 @@ relay-lc.workspace = true
 
 [dev-dependencies]
 proptest.workspace = true
+
+[lints]
+workspace = true
diff --git a/crates/wohl-temp/plain/src/engine.rs b/crates/wohl-temp/plain/src/engine.rs
index 792a1b8..38a2282 100644
--- a/crates/wohl-temp/plain/src/engine.rs
+++ b/crates/wohl-temp/plain/src/engine.rs
@@ -7,9 +7,7 @@
 //! Wohl provides CONFIGURATION + DOMAIN GLUE.
 //! Relay provides VERIFIED THRESHOLD ENGINE.
 
-use relay_lc::engine::{
-    ComparisonOp, SensorReading, Watchpoint, WatchpointTable,
-};
+use relay_lc::engine::{ComparisonOp, SensorReading, Watchpoint, WatchpointTable};
 
 pub const MAX_ZONES: usize = 32;
 pub const MAX_ALERTS_PER_READING: usize = 4;
@@ -18,9 +16,9 @@ pub const MAX_ALERTS_PER_READING: usize = 4;
 #[derive(Clone, Copy)]
 pub struct ZoneConfig {
     pub zone_id: u32,
-    pub freeze_threshold: i32,    // centidegrees (e.g., 0 = 0.00°C)
-    pub overheat_threshold: i32,  // centidegrees (e.g., 4000 = 40.00°C)
-    pub rate_threshold: i32,      // max change per reading in centidegrees
+    pub freeze_threshold: i32,   // centidegrees (e.g., 0 = 0.00°C)
+    pub overheat_threshold: i32, // centidegrees (e.g., 4000 = 40.00°C)
+    pub rate_threshold: i32,     // max change per reading in centidegrees
     pub enabled: bool,
 }
 
@@ -34,7 +32,12 @@ pub struct ZoneState {
 }
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub enum TempAlertType { Freeze, Overheat, RapidDrop, RapidRise }
+pub enum TempAlertType {
+    Freeze,
+    Overheat,
+    RapidDrop,
+    RapidRise,
+}
 
 #[derive(Clone, Copy)]
 pub struct TempAlert {
@@ -63,27 +66,54 @@ pub struct TemperatureMonitor {
 
 impl ZoneConfig {
     pub const fn empty() -> Self {
-        ZoneConfig { zone_id: 0, freeze_threshold: 0, overheat_threshold: 0, rate_threshold: 0, enabled: false }
+        ZoneConfig {
+            zone_id: 0,
+            freeze_threshold: 0,
+            overheat_threshold: 0,
+            rate_threshold: 0,
+            enabled: false,
+        }
     }
 }
 
 impl ZoneState {
     pub const fn empty() -> Self {
-        ZoneState { zone_id: 0, last_value: 0, last_time: 0, active: false }
+        ZoneState {
+            zone_id: 0,
+            last_value: 0,
+            last_time: 0,
+            active: false,
+        }
     }
 }
 
 impl TempAlert {
     pub const fn empty() -> Self {
-        TempAlert { zone_id: 0, alert_type: TempAlertType::Freeze, value: 0, threshold: 0, time: 0 }
+        TempAlert {
+            zone_id: 0,
+            alert_type: TempAlertType::Freeze,
+            value: 0,
+            threshold: 0,
+            time: 0,
+        }
     }
 }
 
 // Watchpoint ID encoding: zone_id * 2 + offset
 // offset 0 = freeze watchpoint (LessOrEqual)
 // offset 1 = overheat watchpoint (GreaterOrEqual)
-fn freeze_wp_id(zone_id: u32) -> u32 { zone_id * 2 }
-fn overheat_wp_id(zone_id: u32) -> u32 { zone_id * 2 + 1 }
+fn freeze_wp_id(zone_id: u32) -> u32 {
+    zone_id * 2
+}
+fn overheat_wp_id(zone_id: u32) -> u32 {
+    zone_id * 2 + 1
+}
+
+impl Default for TemperatureMonitor {
+    fn default() -> Self {
+        Self::new()
+    }
+}
 
 impl TemperatureMonitor {
     pub fn new() -> Self {
@@ -97,12 +127,17 @@ impl TemperatureMonitor {
 
     /// Register a zone. Creates relay-lc watchpoints for freeze and overheat.
     pub fn register_zone(&mut self, config: ZoneConfig) -> bool {
-        if self.zone_count as usize >= MAX_ZONES { return false; }
+        if self.zone_count as usize >= MAX_ZONES {
+            return false;
+        }
 
         let idx = self.zone_count as usize;
         self.configs[idx] = config;
         self.states[idx] = ZoneState {
-            zone_id: config.zone_id, last_value: 0, last_time: 0, active: true,
+            zone_id: config.zone_id,
+            last_value: 0,
+            last_time: 0,
+            active: true,
         };
 
         // Create relay-lc watchpoints — VERIFIED threshold evaluation
@@ -123,7 +158,7 @@ impl TemperatureMonitor {
             current_count: 0,
         });
 
-        self.zone_count = self.zone_count + 1;
+        self.zone_count += 1;
         true
     }
 
@@ -143,10 +178,14 @@ impl TemperatureMonitor {
             sensor_id: freeze_wp_id(zone_id),
             value: value as i64,
         });
-        if freeze_result.violation_count > 0 && (res.alert_count as usize) < MAX_ALERTS_PER_READING {
+        if freeze_result.violation_count > 0 && (res.alert_count as usize) < MAX_ALERTS_PER_READING
+        {
             res.alerts[res.alert_count as usize] = TempAlert {
-                zone_id, alert_type: TempAlertType::Freeze, value,
-                threshold: freeze_result.violations[0].threshold as i32, time,
+                zone_id,
+                alert_type: TempAlertType::Freeze,
+                value,
+                threshold: freeze_result.violations[0].threshold as i32,
+                time,
             };
             res.alert_count += 1;
         }
@@ -156,10 +195,15 @@ impl TemperatureMonitor {
             sensor_id: overheat_wp_id(zone_id),
             value: value as i64,
         });
-        if overheat_result.violation_count > 0 && (res.alert_count as usize) < MAX_ALERTS_PER_READING {
+        if overheat_result.violation_count > 0
+            && (res.alert_count as usize) < MAX_ALERTS_PER_READING
+        {
             res.alerts[res.alert_count as usize] = TempAlert {
-                zone_id, alert_type: TempAlertType::Overheat, value,
-                threshold: overheat_result.violations[0].threshold as i32, time,
+                zone_id,
+                alert_type: TempAlertType::Overheat,
+                value,
+                threshold: overheat_result.violations[0].threshold as i32,
+                time,
             };
             res.alert_count += 1;
         }
@@ -170,21 +214,36 @@ impl TemperatureMonitor {
         let mut i: u32 = 0;
         while i < count {
             let idx = i as usize;
-            if self.states[idx].active && self.configs[idx].zone_id == zone_id && self.configs[idx].enabled {
+            if self.states[idx].active
+                && self.configs[idx].zone_id == zone_id
+                && self.configs[idx].enabled
+            {
                 if self.states[idx].last_time > 0 {
                     let last = self.states[idx].last_value;
                     let rate_thr = self.configs[idx].rate_threshold;
 
-                    if last.saturating_sub(value) > rate_thr && (res.alert_count as usize) < MAX_ALERTS_PER_READING {
+                    if last.saturating_sub(value) > rate_thr
+                        && (res.alert_count as usize) < MAX_ALERTS_PER_READING
+                    {
                         res.alerts[res.alert_count as usize] = TempAlert {
-                            zone_id, alert_type: TempAlertType::RapidDrop, value, threshold: rate_thr, time,
+                            zone_id,
+                            alert_type: TempAlertType::RapidDrop,
+                            value,
+                            threshold: rate_thr,
+                            time,
                         };
                         res.alert_count += 1;
                     }
 
-                    if value.saturating_sub(last) > rate_thr && (res.alert_count as usize) < MAX_ALERTS_PER_READING {
+                    if value.saturating_sub(last) > rate_thr
+                        && (res.alert_count as usize) < MAX_ALERTS_PER_READING
+                    {
                         res.alerts[res.alert_count as usize] = TempAlert {
-                            zone_id, alert_type: TempAlertType::RapidRise, value, threshold: rate_thr, time,
+                            zone_id,
+                            alert_type: TempAlertType::RapidRise,
+                            value,
+                            threshold: rate_thr,
+                            time,
                         };
                         res.alert_count += 1;
                     }
@@ -206,7 +265,13 @@ mod tests {
     use super::*;
 
     fn make_config(zone_id: u32) -> ZoneConfig {
-        ZoneConfig { zone_id, freeze_threshold: 0, overheat_threshold: 4000, rate_threshold: 500, enabled: true }
+        ZoneConfig {
+            zone_id,
+            freeze_threshold: 0,
+            overheat_threshold: 4000,
+            rate_threshold: 500,
+            enabled: true,
+        }
     }
 
     #[test]
@@ -250,7 +315,12 @@ mod tests {
         let r = m.process_reading(1, 1500, 200);
         let mut found = false;
         let mut j = 0u32;
-        while j < r.alert_count { if r.alerts[j as usize].alert_type == TempAlertType::RapidDrop { found = true; } j += 1; }
+        while j < r.alert_count {
+            if r.alerts[j as usize].alert_type == TempAlertType::RapidDrop {
+                found = true;
+            }
+            j += 1;
+        }
         assert!(found);
     }
 
@@ -262,7 +332,12 @@ mod tests {
         let r = m.process_reading(1, 2500, 200);
         let mut found = false;
         let mut j = 0u32;
-        while j < r.alert_count { if r.alerts[j as usize].alert_type == TempAlertType::RapidRise { found = true; } j += 1; }
+        while j < r.alert_count {
+            if r.alerts[j as usize].alert_type == TempAlertType::RapidRise {
+                found = true;
+            }
+            j += 1;
+        }
         assert!(found);
     }
 
diff --git a/spar/wohl_firmware.aadl b/spar/wohl_firmware.aadl
new file mode 100644
index 0000000..95f8748
--- /dev/null
+++ b/spar/wohl_firmware.aadl
@@ -0,0 +1,343 @@
+-- Wohl node firmware threads.
+-- Each sensor node runs one firmware thread that reads its physical
+-- sensors and emits CCSDS packets over the radio. Plus a bootloader
+-- that receives CFDP image transfers from the hub.
+
+package Wohl_Firmware
+public
+  with Wohl_Hardware;
+  with Wohl_Properties;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Data types carried between threads
+  -- ══════════════════════════════════════════════════════════════
+
+  data SensorPacket
+    -- 14 bytes: CCSDS header (6) + sensor payload (8)
+    properties
+      Data_Size => 14 Bytes;
+  end SensorPacket;
+
+  data FirmwareImage
+    -- Signed firmware image delivered via CFDP.
+    -- Typical size 64-256 KB per node class.
+    properties
+      Data_Size => 256 KByte;
+  end FirmwareImage;
+
+  data AttestationReport
+    -- Signed post-boot firmware hash + version report.
+    properties
+      Data_Size => 96 Bytes; -- 32-byte hash + 32-byte sig + metadata
+  end AttestationReport;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Node firmware threads (what runs on each MCU)
+  -- ══════════════════════════════════════════════════════════════
+
+  thread DoorFirmware
+    -- Reed-switch edge triggers interrupt → encode CCSDS → TX over Thread.
+    -- Deep-sleep the rest of the time. Backed by wohl-door sensor node.
+    features
+      reed_in: in event data port;
+      packet_out: out event data port SensorPacket;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Compute_Execution_Time => 0 ms .. 2 ms;
+      Deadline => 100 ms;
+      Priority => 5;
+      Stack_Size => 2048 Bytes;
+  end DoorFirmware;
+
+  thread ClimateFirmware
+    -- 1 sample/min: wake, read I2C sensors, encode CCSDS, TX, sleep.
+    -- Also reacts to PIR motion edge (sporadic).
+    features
+      temp_rh_in: in data port;
+      pressure_in: in data port;
+      motion_in: in event data port;
+      packet_out: out event data port SensorPacket;
+    properties
+      Dispatch_Protocol => Periodic;
+      Period => 60000 ms;
+      Compute_Execution_Time => 0 ms .. 10 ms;
+      Deadline => 5000 ms;
+      Priority => 3;
+      Stack_Size => 4096 Bytes;
+  end ClimateFirmware;
+
+  thread AirFirmware
+    -- Mains-powered: continuous sampling of CO2 + PM.
+    -- Emits one CCSDS packet per sensor reading (multiple per minute).
+    features
+      co2_in: in data port;
+      pm_in: in data port;
+      packet_out: out event data port SensorPacket;
+    properties
+      Dispatch_Protocol => Periodic;
+      Period => 30000 ms;
+      Compute_Execution_Time => 0 ms .. 20 ms;
+      Deadline => 5000 ms;
+      Priority => 3;
+      Stack_Size => 4096 Bytes;
+  end AirFirmware;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Bootloader / OTA threads
+  -- ══════════════════════════════════════════════════════════════
+
+  thread NodeBootloader
+    -- gale-boot placeholder: verifies signature, swaps A/B slot.
+    -- Runs only on reset and during active OTA receive.
+    features
+      image_in: in event data port FirmwareImage;
+      attest_out: out event data port AttestationReport;
+    properties
+      Dispatch_Protocol => Aperiodic;
+      Compute_Execution_Time => 0 ms .. 2000 ms;
+      Priority => 15; -- highest (runs pre-Gale, not scheduled with others)
+      Stack_Size => 8192 Bytes;
+  end NodeBootloader;
+
+  thread OTAManager
+    -- On the hub: reads update manifests, streams firmware via CFDP,
+    -- tracks per-node version state, handles attestation replies.
+    features
+      manifest_in: in event data port;
+      image_out: out event data port FirmwareImage;
+      attest_in: in event data port AttestationReport;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Compute_Execution_Time => 0 ms .. 100 ms;
+      Deadline => 1000 ms;
+      Priority => 10;
+      Stack_Size => 8192 Bytes;
+  end OTAManager;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Node firmware processes (firmware + bootloader per node class)
+  -- ══════════════════════════════════════════════════════════════
+
+  process DoorFirmwareProcess
+    features
+      reed_in: in event data port;
+      packet_out: out event data port SensorPacket;
+      image_in: in event data port FirmwareImage;
+      attest_out: out event data port AttestationReport;
+  end DoorFirmwareProcess;
+
+  process implementation DoorFirmwareProcess.Impl
+    subcomponents
+      firmware: thread DoorFirmware;
+      bootloader: thread NodeBootloader;
+    connections
+      c_reed: port reed_in -> firmware.reed_in;
+      c_packet: port firmware.packet_out -> packet_out;
+      c_image: port image_in -> bootloader.image_in;
+      c_attest: port bootloader.attest_out -> attest_out;
+  end DoorFirmwareProcess.Impl;
+
+  process ClimateFirmwareProcess
+    features
+      temp_rh_in: in data port;
+      pressure_in: in data port;
+      motion_in: in event data port;
+      packet_out: out event data port SensorPacket;
+      image_in: in event data port FirmwareImage;
+      attest_out: out event data port AttestationReport;
+  end ClimateFirmwareProcess;
+
+  process implementation ClimateFirmwareProcess.Impl
+    subcomponents
+      firmware: thread ClimateFirmware;
+      bootloader: thread NodeBootloader;
+    connections
+      c_temp: port temp_rh_in -> firmware.temp_rh_in;
+      c_pres: port pressure_in -> firmware.pressure_in;
+      c_motion: port motion_in -> firmware.motion_in;
+      c_packet: port firmware.packet_out -> packet_out;
+      c_image: port image_in -> bootloader.image_in;
+      c_attest: port bootloader.attest_out -> attest_out;
+  end ClimateFirmwareProcess.Impl;
+
+  process AirFirmwareProcess
+    features
+      co2_in: in data port;
+      pm_in: in data port;
+      packet_out: out event data port SensorPacket;
+      image_in: in event data port FirmwareImage;
+      attest_out: out event data port AttestationReport;
+  end AirFirmwareProcess;
+
+  process implementation AirFirmwareProcess.Impl
+    subcomponents
+      firmware: thread AirFirmware;
+      bootloader: thread NodeBootloader;
+    connections
+      c_co2: port co2_in -> firmware.co2_in;
+      c_pm: port pm_in -> firmware.pm_in;
+      c_packet: port firmware.packet_out -> packet_out;
+      c_image: port image_in -> bootloader.image_in;
+      c_attest: port bootloader.attest_out -> attest_out;
+  end AirFirmwareProcess.Impl;
+
+  -- Hub-side OTA process (wraps the OTAManager thread so it can be a
+  -- subcomponent of the Hub system).
+  process OTAManagerProcess
+    features
+      manifest_in: in event data port;
+      image_out: out event data port FirmwareImage;
+      attest_in: in event data port AttestationReport;
+  end OTAManagerProcess;
+
+  process implementation OTAManagerProcess.Impl
+    subcomponents
+      mgr: thread OTAManager;
+    connections
+      c_manifest: port manifest_in -> mgr.manifest_in;
+      c_image: port mgr.image_out -> image_out;
+      c_attest: port attest_in -> mgr.attest_in;
+  end OTAManagerProcess.Impl;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Hub-side monitor threads (Verus-verified WASM components in Kiln)
+  -- Simpler hardware-integrated view of the threads modeled at the
+  -- logical level in wohl_system.aadl.
+  -- ══════════════════════════════════════════════════════════════
+
+  thread PacketRouter
+    -- Receives CCSDS packets from the radio, dispatches to monitors
+    -- based on sensor_type field. Backed by wohl-hub packet_to_event.
+    -- Periodic sensors (temp, air, power) route through data ports;
+    -- sporadic (water, contact) through event data ports.
+    features
+      packet_in: in event data port SensorPacket;
+      water_out: out event data port;
+      temp_out: out data port;
+      air_out: out data port;
+      contact_out: out event data port;
+      power_out: out data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Compute_Execution_Time => 0 ms .. 1 ms;
+      Deadline => 10 ms;
+      Priority => 2;
+      Stack_Size => 2048 Bytes;
+  end PacketRouter;
+
+  thread HubWaterMonitor
+    features
+      water_in: in event data port;
+      alert_out: out event data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Compute_Execution_Time => 0 ms .. 1 ms;
+      Deadline => 5 ms; -- SYSREQ-WOHL-001
+      Priority => 1;
+      Stack_Size => 1024 Bytes;
+  end HubWaterMonitor;
+
+  thread HubTempMonitor
+    features
+      temp_in: in data port;
+      alert_out: out event data port;
+    properties
+      Dispatch_Protocol => Periodic;
+      Period => 1000 ms;
+      Compute_Execution_Time => 0 ms .. 2 ms;
+      Deadline => 100 ms;
+      Priority => 3;
+      Stack_Size => 1024 Bytes;
+  end HubTempMonitor;
+
+  thread HubAirMonitor
+    features
+      air_in: in data port;
+      alert_out: out event data port;
+    properties
+      Dispatch_Protocol => Periodic;
+      Period => 5000 ms;
+      Compute_Execution_Time => 0 ms .. 1 ms;
+      Deadline => 500 ms;
+      Priority => 5;
+      Stack_Size => 1024 Bytes;
+  end HubAirMonitor;
+
+  thread HubDoorMonitor
+    features
+      contact_in: in event data port;
+      alert_out: out event data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Compute_Execution_Time => 0 ms .. 1 ms;
+      Deadline => 50 ms;
+      Priority => 4;
+      Stack_Size => 1024 Bytes;
+  end HubDoorMonitor;
+
+  thread HubPowerMonitor
+    features
+      power_in: in data port;
+      alert_out: out event data port;
+    properties
+      Dispatch_Protocol => Periodic;
+      Period => 10000 ms;
+      Compute_Execution_Time => 0 ms .. 1 ms;
+      Deadline => 1000 ms;
+      Priority => 6;
+      Stack_Size => 1024 Bytes;
+  end HubPowerMonitor;
+
+  thread HubAlertDispatcher
+    -- Dedup + rate-limit + notification delivery.
+    features
+      alert_in: in event data port;
+      notification_out: out event data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Compute_Execution_Time => 0 ms .. 5 ms;
+      Deadline => 100 ms;
+      Priority => 2;
+      Stack_Size => 2048 Bytes;
+  end HubAlertDispatcher;
+
+  -- Hub monitor process composes all monitors into one process the
+  -- HubNode system can contain.
+  process HubMonitorProcess
+    features
+      packet_in: in event data port SensorPacket;
+      notification_out: out event data port;
+  end HubMonitorProcess;
+
+  process implementation HubMonitorProcess.Impl
+    subcomponents
+      router: thread PacketRouter;
+      water_mon: thread HubWaterMonitor;
+      temp_mon: thread HubTempMonitor;
+      air_mon: thread HubAirMonitor;
+      door_mon: thread HubDoorMonitor;
+      power_mon: thread HubPowerMonitor;
+      dispatcher: thread HubAlertDispatcher;
+    connections
+      -- Packet in → router
+      c_pkt: port packet_in -> router.packet_in;
+
+      -- Router → monitors
+      c_water: port router.water_out -> water_mon.water_in;
+      c_temp: port router.temp_out -> temp_mon.temp_in;
+      c_air: port router.air_out -> air_mon.air_in;
+      c_contact: port router.contact_out -> door_mon.contact_in;
+      c_power: port router.power_out -> power_mon.power_in;
+
+      -- Monitors → dispatcher
+      c_a_water: port water_mon.alert_out -> dispatcher.alert_in;
+      c_a_temp: port temp_mon.alert_out -> dispatcher.alert_in;
+      c_a_air: port air_mon.alert_out -> dispatcher.alert_in;
+      c_a_door: port door_mon.alert_out -> dispatcher.alert_in;
+      c_a_power: port power_mon.alert_out -> dispatcher.alert_in;
+
+      -- Dispatcher → notifications
+      c_notif: port dispatcher.notification_out -> notification_out;
+  end HubMonitorProcess.Impl;
+
+end Wohl_Firmware;
diff --git a/spar/wohl_hardware.aadl b/spar/wohl_hardware.aadl
new file mode 100644
index 0000000..878bd9b
--- /dev/null
+++ b/spar/wohl_hardware.aadl
@@ -0,0 +1,283 @@
+-- Wohl hardware component library.
+-- Specific parts from the starter shopping list. Each declaration maps
+-- 1:1 to a buyable part and carries a Zephyr_Binding for Gale/Zephyr
+-- devicetree generation.
+
+package Wohl_Hardware
+public
+  with Data_Model;
+  with Deployment;
+  with Wohl_Properties;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Buses
+  -- ══════════════════════════════════════════════════════════════
+
+  bus I2C_Bus
+    -- Standard-mode 100 kHz, fast-mode 400 kHz.
+    -- Used for SHT30, BMP280, SCD41, SPS30, BH1750, VEML7700.
+    properties
+      Transmission_Type => push;
+      Wohl_Properties::Zephyr_Binding => "i2c";
+  end I2C_Bus;
+
+  bus UART_Bus
+    -- For PMS5003, PZEM-004T, SPS30 (UART mode).
+    properties
+      Transmission_Type => push;
+      Wohl_Properties::Zephyr_Binding => "uart";
+  end UART_Bus;
+
+  bus GPIO_Line
+    -- Single-bit digital line for reed switches, PIR, water probe.
+    -- Edge-triggered wake source for deep-sleep MCUs.
+    properties
+      Transmission_Type => push;
+      Wohl_Properties::Zephyr_Binding => "gpio";
+  end GPIO_Line;
+
+  bus Thread_Mesh
+    -- IEEE 802.15.4 + OpenThread.
+    -- 2.4 GHz, 250 kbps, ~127-byte PHY frame. Fits Wohl's 14-byte sensor packet.
+    properties
+      Transmission_Type => push;
+      Wohl_Properties::Radio_Protocol => "thread";
+      Wohl_Properties::Zephyr_Binding => "openthread";
+  end Thread_Mesh;
+
+  bus LoRa_Link
+    -- Semtech SX1262, sub-GHz (868/915 MHz depending on region).
+    -- ~1-10 km LOS, 20 mA TX, duty-cycle-limited.
+    properties
+      Transmission_Type => push;
+      Wohl_Properties::Radio_Protocol => "lora";
+      Wohl_Properties::Zephyr_Binding => "semtech,sx1262";
+  end LoRa_Link;
+
+  bus Ethernet_LAN
+    properties
+      Transmission_Type => push;
+      Wohl_Properties::Zephyr_Binding => "ethernet";
+  end Ethernet_LAN;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Memories (MCU-local)
+  -- ══════════════════════════════════════════════════════════════
+
+  memory SRAM_nRF52840
+    -- 256 KB SRAM on Nordic nRF52840.
+    properties
+      Word_Size => 32 bits;
+      Memory_Size => 256 KByte;
+  end SRAM_nRF52840;
+
+  memory Flash_nRF52840
+    -- 1 MB on-chip flash on Nordic nRF52840.
+    properties
+      Word_Size => 32 bits;
+      Memory_Size => 1 MByte;
+  end Flash_nRF52840;
+
+  memory SRAM_ESP32S3
+    -- 512 KB SRAM on ESP32-S3.
+    properties
+      Word_Size => 32 bits;
+      Memory_Size => 512 KByte;
+  end SRAM_ESP32S3;
+
+  memory Flash_ESP32S3
+    -- 8 MB external QSPI flash on most S3 boards.
+    properties
+      Word_Size => 32 bits;
+      Memory_Size => 8 MByte;
+  end Flash_ESP32S3;
+
+  memory RAM_RaspberryPi
+    properties
+      Word_Size => 64 bits;
+      Memory_Size => 2 GByte;
+  end RAM_RaspberryPi;
+
+  memory SDCard_32G
+    properties
+      Word_Size => 8 bits;
+      Memory_Size => 32 GByte;
+  end SDCard_32G;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Processors (specific MCUs + host)
+  -- ══════════════════════════════════════════════════════════════
+
+  processor NRF52840
+    -- Nordic nRF52840: Cortex-M4F, 64 MHz, 256 KB RAM, 1 MB flash.
+    -- Integrated 802.15.4 + BLE 5.0 radio.
+    -- Zephyr board: xiao_ble / nrf52840dk/nrf52840.
+    features
+      thread_radio: requires bus access Thread_Mesh;
+    properties
+      Deployment::Execution_Platform => Native;
+      Scheduling_Protocol => (Rate_Monotonic_Protocol);
+      Clock_Period => 15625 ps; -- 64 MHz
+      Wohl_Properties::Sleep_Current_uA => 2.0;
+      Wohl_Properties::Active_Current_uA => 6000.0;
+      Wohl_Properties::Zephyr_Binding => "nordic,nrf52840";
+  end NRF52840;
+
+  processor ESP32_S3
+    -- Espressif ESP32-S3: Xtensa LX7 dual-core, 240 MHz, 512 KB SRAM.
+    -- Integrated WiFi + BLE. Used for mains-powered nodes.
+    -- Zephyr board: esp32s3_devkitm.
+    features
+      wifi: requires bus access Ethernet_LAN;
+    properties
+      Deployment::Execution_Platform => Native;
+      Scheduling_Protocol => (Rate_Monotonic_Protocol);
+      Clock_Period => 4167 ps; -- 240 MHz
+      Wohl_Properties::Sleep_Current_uA => 10.0;
+      Wohl_Properties::Active_Current_uA => 80000.0;
+      Wohl_Properties::Zephyr_Binding => "espressif,esp32s3";
+  end ESP32_S3;
+
+  processor RaspberryPi4
+    -- BCM2711, 1.5 GHz quad-core Cortex-A72, 2 GB RAM.
+    -- Hub target — runs Kiln WASM interpreter under Linux.
+    features
+      lan: requires bus access Ethernet_LAN;
+    properties
+      Deployment::Execution_Platform => Native;
+      Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
+      Clock_Period => 667 ps; -- 1.5 GHz
+      Wohl_Properties::Active_Current_uA => 600000.0; -- @5V
+      Wohl_Properties::Zephyr_Binding => "brcm,bcm2711";
+  end RaspberryPi4;
+
+  processor IntelN100
+    -- Intel N100: 4-core x86-64, up to 3.4 GHz burst, 6 W TDP.
+    -- Used by GMKtec Nucbox, Beelink S12, Minisforum UN100 mini PCs.
+    -- Headroom for local ML (occupancy, anomaly detection) or local LLM.
+    features
+      lan: requires bus access Ethernet_LAN;
+    properties
+      Deployment::Execution_Platform => Native;
+      Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
+      Clock_Period => 294 ps; -- 3.4 GHz burst
+      Wohl_Properties::Active_Current_uA => 1200000.0; -- ~6 W @ 5 V
+      Wohl_Properties::Zephyr_Binding => "intel,alderlake-n";
+  end IntelN100;
+
+  memory RAM_MiniPC
+    properties
+      Word_Size => 64 bits;
+      Memory_Size => 16 GByte;
+  end RAM_MiniPC;
+
+  memory SSD_NVMe_256G
+    properties
+      Word_Size => 8 bits;
+      Memory_Size => 256 GByte;
+  end SSD_NVMe_256G;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- Sensor devices (specific parts)
+  -- ══════════════════════════════════════════════════════════════
+
+  device SHT30
+    -- Sensirion SHT30: temp ±0.3 °C, RH ±3 %, I2C addr 0x44.
+    features
+      i2c: requires bus access I2C_Bus;
+      reading: out data port;
+    properties
+      Period => 60000 ms; -- 1 sample/min on battery
+      Wohl_Properties::Sleep_Current_uA => 1.5;
+      Wohl_Properties::Active_Current_uA => 800.0;
+      Wohl_Properties::Sampling_Period_Sec => 60.0;
+      Wohl_Properties::Zephyr_Binding => "sensirion,sht3xd";
+  end SHT30;
+
+  device BMP280
+    -- Bosch BMP280: pressure ±1 hPa, temp ±1 °C, I2C addr 0x76/0x77.
+    features
+      i2c: requires bus access I2C_Bus;
+      reading: out data port;
+    properties
+      Period => 60000 ms;
+      Wohl_Properties::Sleep_Current_uA => 0.1;
+      Wohl_Properties::Active_Current_uA => 2.7;
+      Wohl_Properties::Sampling_Period_Sec => 60.0;
+      Wohl_Properties::Zephyr_Binding => "bosch,bme280";
+  end BMP280;
+
+  device BH1750
+    -- ROHM BH1750: lux, I2C addr 0x23.
+    features
+      i2c: requires bus access I2C_Bus;
+      reading: out data port;
+    properties
+      Period => 60000 ms;
+      Wohl_Properties::Active_Current_uA => 120.0;
+      Wohl_Properties::Sampling_Period_Sec => 60.0;
+      Wohl_Properties::Zephyr_Binding => "rohm,bh1750";
+  end BH1750;
+
+  device SCD41
+    -- Sensirion SCD41: true NDIR CO2, ±50 ppm + 5 %, I2C addr 0x62.
+    -- Mains-only sensor (low-power mode still 0.4 mA avg).
+    features
+      i2c: requires bus access I2C_Bus;
+      reading: out data port;
+    properties
+      Period => 30000 ms;
+      Wohl_Properties::Sleep_Current_uA => 15.0;
+      Wohl_Properties::Active_Current_uA => 15000.0;
+      Wohl_Properties::Sampling_Period_Sec => 30.0;
+      Wohl_Properties::Zephyr_Binding => "sensirion,scd4x";
+  end SCD41;
+
+  device SPS30
+    -- Sensirion SPS30: PM1/PM2.5/PM4/PM10, I2C or UART, 60 mA fan.
+    -- Mains-only. 8-year design life, upstream Zephyr driver.
+    features
+      i2c: requires bus access I2C_Bus;
+      reading: out data port;
+    properties
+      Period => 60000 ms;
+      Wohl_Properties::Active_Current_uA => 60000.0;
+      Wohl_Properties::Sampling_Period_Sec => 60.0;
+      Wohl_Properties::Zephyr_Binding => "sensirion,sps30";
+  end SPS30;
+
+  device AM312_PIR
+    -- Generic PIR motion sensor, 3.3 V, ~3 m cone.
+    -- Drives a GPIO line; edge interrupt wakes MCU.
+    features
+      gpio: requires bus access GPIO_Line;
+      event_out: out event data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Wohl_Properties::Sleep_Current_uA => 50.0;
+      Wohl_Properties::Active_Current_uA => 50.0;
+  end AM312_PIR;
+
+  device ReedSwitch_MC38
+    -- Surface-mount magnetic reed (window/door contact).
+    -- Passive — zero current draw at rest.
+    features
+      gpio: requires bus access GPIO_Line;
+      event_out: out event data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Wohl_Properties::Sleep_Current_uA => 0.0;
+      Wohl_Properties::Active_Current_uA => 0.0;
+  end ReedSwitch_MC38;
+
+  device WaterProbe
+    -- Gold-finger conductivity probe. Pulse-powered (GPIO-driven).
+    features
+      gpio: requires bus access GPIO_Line;
+      event_out: out event data port;
+    properties
+      Dispatch_Protocol => Sporadic;
+      Wohl_Properties::Active_Current_uA => 100.0; -- during pulse
+  end WaterProbe;
+
+end Wohl_Hardware;
diff --git a/spar/wohl_home.aadl b/spar/wohl_home.aadl
new file mode 100644
index 0000000..018758a
--- /dev/null
+++ b/spar/wohl_home.aadl
@@ -0,0 +1,103 @@
+-- Wohl deployed home system.
+-- 3 door/window + 1 climate + 1 air-quality + 1 hub, wired through the
+-- Thread mesh. Sensor packets flow node→hub; OTA images flow hub→node;
+-- attestation reports flow node→hub.
+
+package Wohl_Home
+public
+  with Wohl_Hardware;
+  with Wohl_Firmware;
+  with Wohl_Nodes;
+  with Wohl_Properties;
+
+  system StarterHome
+    features
+      notification_out: out event data port;
+  end StarterHome;
+
+  system implementation StarterHome.Deployed
+    subcomponents
+      hub: system Wohl_Nodes::HubNode.RPi;
+
+      door_front: system Wohl_Nodes::DoorWindowNode.Battery
+        { Wohl_Properties::Zone_Id => 1;
+          Wohl_Properties::Zone_Name => "front_door";
+          Wohl_Properties::Location => "ground_floor/entry";
+          Wohl_Properties::Role => "door"; };
+
+      door_back: system Wohl_Nodes::DoorWindowNode.Battery
+        { Wohl_Properties::Zone_Id => 2;
+          Wohl_Properties::Zone_Name => "back_door";
+          Wohl_Properties::Location => "ground_floor/utility";
+          Wohl_Properties::Role => "door"; };
+
+      window_bedroom: system Wohl_Nodes::DoorWindowNode.Battery
+        { Wohl_Properties::Zone_Id => 3;
+          Wohl_Properties::Zone_Name => "bedroom_window";
+          Wohl_Properties::Location => "first_floor/bedroom";
+          Wohl_Properties::Role => "window"; };
+
+      living_room: system Wohl_Nodes::ClimateNode.Battery
+        { Wohl_Properties::Zone_Id => 4;
+          Wohl_Properties::Zone_Name => "living_room";
+          Wohl_Properties::Location => "ground_floor/living_room"; };
+
+      kitchen_air: system Wohl_Nodes::AirQualityNode.Mains
+        { Wohl_Properties::Zone_Id => 5;
+          Wohl_Properties::Zone_Name => "kitchen";
+          Wohl_Properties::Location => "ground_floor/kitchen"; };
+    connections
+      -- Sensor data: node → hub
+      s_door_front: port door_front.packet_out -> hub.packet_in;
+      s_door_back: port door_back.packet_out -> hub.packet_in;
+      s_window_bedroom: port window_bedroom.packet_out -> hub.packet_in;
+      s_living_room: port living_room.packet_out -> hub.packet_in;
+      s_kitchen_air: port kitchen_air.packet_out -> hub.packet_in;
+
+      -- OTA images: hub → node
+      o_door_front: port hub.image_out -> door_front.image_in;
+      o_door_back: port hub.image_out -> door_back.image_in;
+      o_window_bedroom: port hub.image_out -> window_bedroom.image_in;
+      o_living_room: port hub.image_out -> living_room.image_in;
+      o_kitchen_air: port hub.image_out -> kitchen_air.image_in;
+
+      -- Attestation: node → hub
+      a_door_front: port door_front.attest_out -> hub.attest_in;
+      a_door_back: port door_back.attest_out -> hub.attest_in;
+      a_window_bedroom: port window_bedroom.attest_out -> hub.attest_in;
+      a_living_room: port living_room.attest_out -> hub.attest_in;
+      a_kitchen_air: port kitchen_air.attest_out -> hub.attest_in;
+
+      -- Notifications leave the home
+      n_out: port hub.notification_out -> notification_out;
+  end StarterHome.Deployed;
+
+  -- Alternate deployment using the MiniPC hub variant.
+  system implementation StarterHome.DeployedMiniPC
+    subcomponents
+      hub: system Wohl_Nodes::HubNode.MiniPC;
+      door_front: system Wohl_Nodes::DoorWindowNode.Battery;
+      door_back: system Wohl_Nodes::DoorWindowNode.Battery;
+      window_bedroom: system Wohl_Nodes::DoorWindowNode.Battery;
+      living_room: system Wohl_Nodes::ClimateNode.Battery;
+      kitchen_air: system Wohl_Nodes::AirQualityNode.Mains;
+    connections
+      s_door_front: port door_front.packet_out -> hub.packet_in;
+      s_door_back: port door_back.packet_out -> hub.packet_in;
+      s_window_bedroom: port window_bedroom.packet_out -> hub.packet_in;
+      s_living_room: port living_room.packet_out -> hub.packet_in;
+      s_kitchen_air: port kitchen_air.packet_out -> hub.packet_in;
+      o_door_front: port hub.image_out -> door_front.image_in;
+      o_door_back: port hub.image_out -> door_back.image_in;
+      o_window_bedroom: port hub.image_out -> window_bedroom.image_in;
+      o_living_room: port hub.image_out -> living_room.image_in;
+      o_kitchen_air: port hub.image_out -> kitchen_air.image_in;
+      a_door_front: port door_front.attest_out -> hub.attest_in;
+      a_door_back: port door_back.attest_out -> hub.attest_in;
+      a_window_bedroom: port window_bedroom.attest_out -> hub.attest_in;
+      a_living_room: port living_room.attest_out -> hub.attest_in;
+      a_kitchen_air: port kitchen_air.attest_out -> hub.attest_in;
+      n_out: port hub.notification_out -> notification_out;
+  end StarterHome.DeployedMiniPC;
+
+end Wohl_Home;
diff --git a/spar/wohl_nodes.aadl b/spar/wohl_nodes.aadl
new file mode 100644
index 0000000..80f4823
--- /dev/null
+++ b/spar/wohl_nodes.aadl
@@ -0,0 +1,208 @@
+-- Wohl node system implementations.
+-- Each `system implementation` describes one physical node:
+-- MCU + sensors + firmware process + bus + memory. Nodes are battery
+-- or mains depending on the sensors they carry.
+
+package Wohl_Nodes
+public
+  with Wohl_Hardware;
+  with Wohl_Firmware;
+  with Wohl_Properties;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- DoorWindowNode.Battery
+  -- MC-38 reed on a XIAO nRF52840, CR2032 coin cell, ~2-3 yr life.
+  -- Event-driven — wakes on reed edge, sends Thread packet.
+  -- ══════════════════════════════════════════════════════════════
+
+  system DoorWindowNode
+    features
+      packet_out: out event data port Wohl_Firmware::SensorPacket;
+      image_in: in event data port Wohl_Firmware::FirmwareImage;
+      attest_out: out event data port Wohl_Firmware::AttestationReport;
+  end DoorWindowNode;
+
+  system implementation DoorWindowNode.Battery
+    subcomponents
+      mcu: processor Wohl_Hardware::NRF52840;
+      ram: memory Wohl_Hardware::SRAM_nRF52840;
+      rom: memory Wohl_Hardware::Flash_nRF52840;
+      reed: device Wohl_Hardware::ReedSwitch_MC38;
+      fw: process Wohl_Firmware::DoorFirmwareProcess.Impl;
+      gpio: bus Wohl_Hardware::GPIO_Line;
+      radio: bus Wohl_Hardware::Thread_Mesh;
+    connections
+      c_reed_bus: bus access gpio -> reed.gpio;
+      c_radio_bus: bus access radio -> mcu.thread_radio;
+      c_reed_to_fw: port reed.event_out -> fw.firmware.reed_in;
+      c_fw_out: port fw.firmware.packet_out -> packet_out;
+      c_ota_in: port image_in -> fw.image_in;
+      c_attest_out: port fw.attest_out -> attest_out;
+    properties
+      Actual_Processor_Binding => (reference (mcu)) applies to fw.firmware;
+      Actual_Processor_Binding => (reference (mcu)) applies to fw.bootloader;
+      Actual_Memory_Binding => (reference (ram)) applies to fw;
+      Actual_Memory_Binding => (reference (ram)) applies to fw.firmware;
+      Actual_Memory_Binding => (reference (ram)) applies to fw.bootloader;
+      Wohl_Properties::Battery_Capacity_mAh => 220.0;  -- CR2032
+      Wohl_Properties::Expected_Battery_Life_Years => 2.5;
+  end DoorWindowNode.Battery;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- ClimateNode.Battery
+  -- SHT30 + BMP280 + AM312 on a XIAO nRF52840, 2×AA lithium.
+  -- Periodic (1 sample/min) + motion event. ~7-10 yr life.
+  -- ══════════════════════════════════════════════════════════════
+
+  system ClimateNode
+    features
+      packet_out: out event data port Wohl_Firmware::SensorPacket;
+      image_in: in event data port Wohl_Firmware::FirmwareImage;
+      attest_out: out event data port Wohl_Firmware::AttestationReport;
+  end ClimateNode;
+
+  system implementation ClimateNode.Battery
+    subcomponents
+      mcu: processor Wohl_Hardware::NRF52840;
+      ram: memory Wohl_Hardware::SRAM_nRF52840;
+      rom: memory Wohl_Hardware::Flash_nRF52840;
+      temp_rh: device Wohl_Hardware::SHT30;
+      pressure: device Wohl_Hardware::BMP280;
+      motion: device Wohl_Hardware::AM312_PIR;
+      fw: process Wohl_Firmware::ClimateFirmwareProcess.Impl;
+      i2c: bus Wohl_Hardware::I2C_Bus;
+      gpio: bus Wohl_Hardware::GPIO_Line;
+      radio: bus Wohl_Hardware::Thread_Mesh;
+    connections
+      c_i2c_temp: bus access i2c -> temp_rh.i2c;
+      c_i2c_pres: bus access i2c -> pressure.i2c;
+      c_gpio_pir: bus access gpio -> motion.gpio;
+      c_radio_bus: bus access radio -> mcu.thread_radio;
+      c_temp_to_fw: port temp_rh.reading -> fw.temp_rh_in;
+      c_pres_to_fw: port pressure.reading -> fw.pressure_in;
+      c_motion_to_fw: port motion.event_out -> fw.motion_in;
+      c_fw_out: port fw.packet_out -> packet_out;
+      c_ota_in: port image_in -> fw.image_in;
+      c_attest_out: port fw.attest_out -> attest_out;
+    properties
+      Actual_Processor_Binding => (reference (mcu)) applies to fw.firmware;
+      Actual_Processor_Binding => (reference (mcu)) applies to fw.bootloader;
+      Actual_Memory_Binding => (reference (ram)) applies to fw.firmware;
+      Actual_Memory_Binding => (reference (ram)) applies to fw.bootloader;
+      Wohl_Properties::Battery_Capacity_mAh => 5000.0;  -- 2×AA lithium
+      Wohl_Properties::Expected_Battery_Life_Years => 8.0;
+  end ClimateNode.Battery;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- AirQualityNode.Mains
+  -- SCD41 + SPS30 on an ESP32-S3, USB-C wall power.
+  -- Continuous sampling — not battery-viable.
+  -- ══════════════════════════════════════════════════════════════
+
+  system AirQualityNode
+    features
+      packet_out: out event data port Wohl_Firmware::SensorPacket;
+      image_in: in event data port Wohl_Firmware::FirmwareImage;
+      attest_out: out event data port Wohl_Firmware::AttestationReport;
+  end AirQualityNode;
+
+  system implementation AirQualityNode.Mains
+    subcomponents
+      mcu: processor Wohl_Hardware::ESP32_S3;
+      ram: memory Wohl_Hardware::SRAM_ESP32S3;
+      rom: memory Wohl_Hardware::Flash_ESP32S3;
+      co2: device Wohl_Hardware::SCD41;
+      pm: device Wohl_Hardware::SPS30;
+      fw: process Wohl_Firmware::AirFirmwareProcess.Impl;
+      i2c: bus Wohl_Hardware::I2C_Bus;
+      lan: bus Wohl_Hardware::Ethernet_LAN;
+    connections
+      c_i2c_co2: bus access i2c -> co2.i2c;
+      c_i2c_pm: bus access i2c -> pm.i2c;
+      c_lan_bus: bus access lan -> mcu.wifi;
+      c_co2_to_fw: port co2.reading -> fw.co2_in;
+      c_pm_to_fw: port pm.reading -> fw.pm_in;
+      c_fw_out: port fw.packet_out -> packet_out;
+      c_ota_in: port image_in -> fw.image_in;
+      c_attest_out: port fw.attest_out -> attest_out;
+    properties
+      Actual_Processor_Binding => (reference (mcu)) applies to fw.firmware;
+      Actual_Processor_Binding => (reference (mcu)) applies to fw.bootloader;
+      Actual_Memory_Binding => (reference (ram)) applies to fw.firmware;
+      Actual_Memory_Binding => (reference (ram)) applies to fw.bootloader;
+  end AirQualityNode.Mains;
+
+  -- ══════════════════════════════════════════════════════════════
+  -- HubNode.RPi
+  -- Raspberry Pi 4 2 GB running Kiln WASM interpreter under Linux.
+  -- Collects all sensor streams, runs monitors, dispatches alerts,
+  -- and runs the OTAManager for node firmware distribution.
+  -- ══════════════════════════════════════════════════════════════
+
+  system HubNode
+    features
+      packet_in: in event data port Wohl_Firmware::SensorPacket;
+      image_out: out event data port Wohl_Firmware::FirmwareImage;
+      attest_in: in event data port Wohl_Firmware::AttestationReport;
+      notification_out: out event data port;
+  end HubNode;
+
+  -- HubNode.RPi — budget/fanless: Raspberry Pi 4/5, Kiln WASM runtime.
+  system implementation HubNode.RPi
+    subcomponents
+      cpu: processor Wohl_Hardware::RaspberryPi4;
+      ram: memory Wohl_Hardware::RAM_RaspberryPi;
+      rom: memory Wohl_Hardware::SDCard_32G;
+      monitors: process Wohl_Firmware::HubMonitorProcess.Impl;
+      ota: process Wohl_Firmware::OTAManagerProcess.Impl;
+      lan: bus Wohl_Hardware::Ethernet_LAN;
+    connections
+      c_lan_bus: bus access lan -> cpu.lan;
+      c_pkt_in: port packet_in -> monitors.packet_in;
+      c_notif_out: port monitors.notification_out -> notification_out;
+      c_image_out: port ota.image_out -> image_out;
+      c_attest_in: port attest_in -> ota.attest_in;
+    properties
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.router;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.water_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.temp_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.air_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.door_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.power_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.dispatcher;
+      Actual_Processor_Binding => (reference (cpu)) applies to ota.mgr;
+      Actual_Memory_Binding => (reference (ram)) applies to monitors;
+      Actual_Memory_Binding => (reference (ram)) applies to ota;
+  end HubNode.RPi;
+
+  -- HubNode.MiniPC — upgrade path for local ML, larger histories.
+  -- Intel N100 in a GMKtec/Beelink/Minisforum chassis, 16 GB RAM, NVMe.
+  -- Same software, more ceiling.
+  system implementation HubNode.MiniPC
+    subcomponents
+      cpu: processor Wohl_Hardware::IntelN100;
+      ram: memory Wohl_Hardware::RAM_MiniPC;
+      rom: memory Wohl_Hardware::SSD_NVMe_256G;
+      monitors: process Wohl_Firmware::HubMonitorProcess.Impl;
+      ota: process Wohl_Firmware::OTAManagerProcess.Impl;
+      lan: bus Wohl_Hardware::Ethernet_LAN;
+    connections
+      c_lan_bus: bus access lan -> cpu.lan;
+      c_pkt_in: port packet_in -> monitors.packet_in;
+      c_notif_out: port monitors.notification_out -> notification_out;
+      c_image_out: port ota.image_out -> image_out;
+      c_attest_in: port attest_in -> ota.attest_in;
+    properties
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.router;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.water_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.temp_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.air_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.door_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.power_mon;
+      Actual_Processor_Binding => (reference (cpu)) applies to monitors.dispatcher;
+      Actual_Processor_Binding => (reference (cpu)) applies to ota.mgr;
+      Actual_Memory_Binding => (reference (ram)) applies to monitors;
+      Actual_Memory_Binding => (reference (ram)) applies to ota;
+  end HubNode.MiniPC;
+
+end Wohl_Nodes;
diff --git a/spar/wohl_properties.aadl b/spar/wohl_properties.aadl
new file mode 100644
index 0000000..84cc4d1
--- /dev/null
+++ b/spar/wohl_properties.aadl
@@ -0,0 +1,45 @@
+-- Wohl custom property set.
+-- Hardware-level properties for power/battery/radio analysis.
+-- Units are encoded in property names because spar's property-set
+-- subset doesn't yet accept inline `units (...)` declarations.
+
+property set Wohl_Properties is
+
+  -- Power: current in microamps.
+  Sleep_Current_uA: aadlreal applies to (device, processor, system);
+  Active_Current_uA: aadlreal applies to (device, processor, system);
+
+  -- Battery capacity in milliamp-hours.
+  Battery_Capacity_mAh: aadlreal applies to (system);
+
+  -- Sampling period in seconds.
+  Sampling_Period_Sec: aadlreal applies to (device);
+
+  -- Radio protocol: use a plain string ("thread", "lora", "ble", "wifi", "ethernet").
+  Radio_Protocol: aadlstring applies to (bus, processor);
+
+  -- Zephyr/Gale devicetree-compatible string.
+  Zephyr_Binding: aadlstring applies to (device, processor, bus);
+
+  -- Expected battery lifetime estimate (years).
+  Expected_Battery_Life_Years: aadlreal applies to (system);
+
+  -- ── Deployment-time metadata (sensor-to-location mapping) ──
+  -- These carry the same information as wohl.toml but live in the
+  -- AADL model so fault-tree and deployment analyses can reason about
+  -- which zone loses coverage when a node fails.
+
+  -- Numeric zone ID that matches relay-lc watchpoint indices and the
+  -- CCSDS packet zone_id field.
+  Zone_Id: aadlinteger applies to (system, device);
+
+  -- Human-readable zone/room name for reports and dashboards.
+  Zone_Name: aadlstring applies to (system, device);
+
+  -- Physical location hint (e.g., "first_floor/kitchen/window_east").
+  Location: aadlstring applies to (system, device);
+
+  -- Sensor role within the zone (e.g., "door", "window", "leak_probe").
+  Role: aadlstring applies to (system, device);
+
+end Wohl_Properties;