The kernel-side foundation of AxonOS: seven Rust crates that compose into the real-time scheduling, capability isolation, time, inter-process communication and wire-format layer a brain-computer interface signal pipeline needs to meet hard deadlines on a Cortex-M microcontroller, plus a reference firmware crate for the STM32F407. No heap and no allocator on the hot path. Five crates carry Kani bounded-model-checking harnesses, 30 in all, and unsafe code is confined to three documented operations of the single-producer single-consumer ring and its handles' Send and Sync impls; every other module forbids it. no_std builds are checked in CI against thumbv7em and thumbv8m.main, not asserted. Funding pays for a year of development and for the first instrumented timing measurement on reference hardware, published with its trace.
Fund this project