Wohl wahrt. — Maintains the well-being of your home.
Verified embedded sensor monitoring on the PulseEngine toolchain. Built on Relay stream transformers. Sensor nodes publish typed streams over CCSDS; a hub routes them through six verified monitor components and dispatches alerts.
Verified. Always on.
| Component | Input | Output | Safety |
|---|---|---|---|
| Water Leak | stream<water-event> | stream<alert> | CRITICAL — immediate, no delay |
| Temperature | stream<temperature> | stream<alert> | Freeze/overheat protection |
| Air Quality | stream<air-quality> | stream<alert> | CO2/PM2.5/VOC monitoring |
| Door Watch | stream<contact-event> | stream<alert> | Open door/window detection |
| Power Meter | stream<power-reading> | stream<alert> | Usage + anomaly detection |
| Alert Dispatcher | stream<alert> | notifications | Dedup, rate-limit, deliver |
All component cores are no_std, no_alloc, and verified by Kani bounded model checking.
- Sensor nodes — ESP32-C3 / STM32G0 firmware, CCSDS-framed streams
- Hub — Raspberry Pi or STM32H7, runs the six monitors as Relay stream transformers
- System model — AADL specification in
spar/(firmware threads, hardware nodes, deployed home topology) - Traceability — ASPICE artifacts in
artifacts/{sysreq,swreq,swarch,swdd,verification}/, validated by Rivet
# Workspace tests + proptest
cargo test --workspace
# Kani bounded model checking (per component)
for c in wohl-leak wohl-temp wohl-air wohl-door wohl-power wohl-alert; do
cargo kani -p "$c"
done
# Cargo-fuzz smoke (60s per target — coverage currently `fuzz_leak`, `fuzz_temp`)
cargo fuzz run fuzz_leak -- -max_total_time=60
cargo fuzz run fuzz_temp -- -max_total_time=60
# ASPICE artifact traceability
rivet validateToolchain: see rust-version in workspace Cargo.toml.
The relay and rivet repositories must be cloned as siblings of wohl/ for path-dependencies to resolve.
| Track | Status |
|---|---|
| Kani BMC (all components) | gated by CI |
| proptest suites | gated by CI |
| cargo-fuzz | smoke gated by CI; coverage expansion tracked via issues |
| Verus deductive proofs | planned for wohl-alert dispatcher dedup invariant |
| AADL system model | active in spar/ |
| Rivet ASPICE validation | gated by CI |
Licensed under the Apache License, Version 2.0. See LICENSE for the full text.
- PulseEngine — umbrella project
- Relay — stream transformers
- Rivet — ASPICE traceability
- Issue #1 — CI initiative