diff --git a/Cargo.lock b/Cargo.lock
index b155f12..292f7c8 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"
@@ -750,6 +757,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..7474648 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -28,6 +28,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-hub/Cargo.toml b/crates/wohl-hub/Cargo.toml
index bdf4deb..8b2272c 100644
--- a/crates/wohl-hub/Cargo.toml
+++ b/crates/wohl-hub/Cargo.toml
@@ -28,6 +28,7 @@ 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"] }
diff --git a/crates/wohl-hub/src/main.rs b/crates/wohl-hub/src/main.rs
index cee3bb1..667a5df 100644
--- a/crates/wohl-hub/src/main.rs
+++ b/crates/wohl-hub/src/main.rs
@@ -2,9 +2,13 @@
 //!
 //! 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 ────────────────────────────────────────
@@ -627,12 +631,96 @@ 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 +754,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");
 }
@@ -1105,4 +1213,96 @@ dedup_cooldown_sec = 60
             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/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;