AxonOS is the hard real-time layer between neural hardware and the applications
that use it: an open-source kernel in #![no_std] Rust on ARM Cortex-M, with
worst-case response times that are proven rather than benchmarked, and
privacy enforced below the application layer, where no application can
bypass it.
Applications receive typed, consent-bound intent events — never raw neural streams.
It is not an AI-agent framework, a chatbot runtime or a token project. Every guarantee it makes is specified, openly licensed, and built to be checked by someone else.
|
Build — AxonOS |
Measure — dy-wcet |
|
Discover — Radar |
Verify — DY Research |
Timing analysis that refuses rather than rounds. Worst-case response time for real-time systems, computed exactly in integer arithmetic — and a named refusal wherever a bound cannot be justified.
Two tasks. A runs 100 µs every 400 µs at higher priority; B runs 200 µs every 1,000 µs. The common answer for B is 400 µs. The correct one is 300 µs — and with other periods, the same mistake reports a deadline as met that is missed on hardware.
The schedule, drawn by simulating the scheduler rather than the formula. On 5,000 random task pairs it lands exactly on the analysis's answer.
| 0 | dependencies, and no floating point anywhere |
| 8 | Kani proofs, every one closing in CI |
| 100 | tests, fifteen of them derived by hand |
| 6 | named refusals — a bound is never guessed |
Try it live → · Source · The method · The bounty
Every figure published here, its evidence level, and the artefact it derives
from. L1 formally proven · L2 measured on reference hardware · L3
independently reproduced · CI checked mechanically on every push ·
analytical derived by hand from a reference. Graded as in
CLAIMS.md, which this table follows. A figure
absent from this table is not claimed.
| Figure | Value | Source |
|---|---|---|
| End-to-end WCRT, proven upper bound | ≤ 1,000 µs · L1 | scheduler BMC harnesses |
| End-to-end WCRT, worst observed | 972 µs · L2 | RFC-0001 · 12 h, 10.8 M epochs, 0 misses · raw traces pending |
| IPC slot latency, proven upper bound | ≤ 0.5 µs · L1 | SPSC BMC harnesses |
| Consent withdrawal terminates, in the correct state | proven · L1 | handle_withdraw_terminates.rs · covers the Granted starting state; the rest is an open gap |
| Consent withdrawal, transition time | ≤ 1,648 cycles · analytical | instruction count against the ISA timing reference, ≈ 9.8 µs at 168 MHz · not a Kani output; derivation pending |
| Release jitter, σ | 2.1 µs · L2 | RFC-0001 · raw traces pending |
| Kani proofs re-run in CI | 47 · L1 | kernel 30 · signal pipeline 9 · dy-wcet 8 · consent's 6 are in its repository, not yet in CI |
unsafe in the kernel |
one crate · CI | confined to axonos-spsc; #![forbid(unsafe_code)] in consent, protocol and five kernel crates |
| Wire format, reference against SDK | byte-identical · CI | conformance: Python reference and Rust SDK on every push; C header by _Static_assert |
| Projects on the live map | 100+ · live | data/radar.json, refreshed every 3 h |
≤ 1,000 µs is proven; 972 µs is the worst anyone has seen. A proof and an
observation are different kinds of statement. Until the raw traces land in
axonos-validation, every L2
row is held as pending and graded in
CLAIMS.md.
L3 independent reproduction is not claimed for anything.
Not in this table, and therefore not claimed: classification accuracy, information transfer rate, power draw, on-hardware latency in a deployment, session length, electrode count in real use.
One command, ninety seconds, no account:
git clone https://github.com/AxonOS-org/axonos-stack && cd axonos-stack
cargo run --locked --bin session -- --seed 7 --frames 3000 | diff - reference/session-7.txtSilence means the whole chain — electrode to conditioning to privacy boundary to the right to act — reproduced byte for byte on your machine. The session is not a happy path: an electrode lifts partway through, and the transcript records the system withdrawing the right to actuate 96 ms later while it keeps recording.
More to run — the path, the kernel proofs, the signal chain, the timing analysis
# the full path, electrode to typed intent, verified bit for bit
git clone https://github.com/AxonOS-org/axonos-e2e-demo && cd axonos-e2e-demo && ./run.sh --verify
# the kernel: its tests, then a machine-checked proof
git clone https://github.com/AxonOS-org/axonos-kernel && cd axonos-kernel
cargo test --workspace
cargo kani setup && ( cd axonos-spsc/kani-proofs && cargo kani )
# the signal chain, bit-exact against conformance vectors
git clone https://github.com/AxonOS-org/axonos-signal-pipeline && cd axonos-signal-pipeline && cargo test
# the timing analysis, and every number it states against its source
git clone https://github.com/DYResearch/dy-wcet && cd dy-wcet && cargo test && ./audit.shWhere to push, if you want to prove this wrong
- The 1,000 µs bound. Run the scheduler harnesses. A counterexample from Kani falsifies it outright.
- The 972 µs observation. It is L2 and pending until the raw traces are published; until then, treat it as a claim with its evidence outstanding.
- Consent withdrawal. Run
handle_withdraw_terminates.rsundercargo kani: it proves termination and the target state, fromGrantedonly, and it is the one proof here not yet re-run in CI. The 1,648-cycle figure is analytical; an execution above it on the reference hardware falsifies it. - dy-wcet. Find a task set where it returns a bound the recurrence does not support. There is a bounty for the first one.
- The Radar's scores. Every score is published with the evidence it rests on. Recompute any of them.
A living map of every open-source brain–computer-interface project, tool and team, scored from public evidence and refreshed every three hours. AxonOS is ranked by the same formula as everyone else, with no boosting.
The State of Open BCI — read the full report →
Leading by reach: omi · wukong-robot · mne-python · NeuroKit · 15 languages · last refreshed 27 Sep 2026, 17:17 UTC
The discipline behind AxonOS, applied to your system. DY Research carries out independent technical due diligence for investors, founders and engineering teams: every claim traced to its code, its tests and its evidence, ending in a written verdict.
| Engagement | The question it answers |
|---|---|
| Snapshot · 5 business days | What does this technology actually do, and what does its evidence support? |
| Focused Audit · 2–3 weeks | Does one critical property — timing, determinism, concurrency — actually hold? |
| Due Diligence · 3–4 weeks | Is the technology what the company says it is, and what could break the investment? |
Fixed price, from $5,000, agreed in writing before any work begins. Revenue funds AxonOS. Engagements and full scope →
| Repository | Role |
|---|---|
axonos-kernel |
Scheduler, lock-free SPSC IPC, capabilities, intent, time — #![no_std] |
axonos-signal-pipeline |
Conditioning, DSP and classification, bit-exact against conformance vectors |
axonos-consent |
The consent state machine, with a bounded withdrawal |
axonos-protocol · axonos-sdk |
The wire format and the application interface |
axonos-hal |
Hardware abstraction for ARM Cortex-M |
axonos-stack · axonos-e2e-demo |
The layers running as one system, reproducible from a seed |
axonos-standard · axonos-rfcs |
The specification, its claims ledger and its design records |
axonos-conformance · axonos-validation |
Test vectors and bindings; measurement campaigns and their traces |
DYResearch/dy-wcet |
Worst-case response-time analysis, standalone |
AxonOS-BCI/axonos-community-radar |
The live map of open neurotech |
AxonOS does not currently claim, and this organisation must not be read as claiming: FDA clearance, CE marking or medical-device approval in any jurisdiction; clinical efficacy or independent clinical validation; certified medical-device status or production-implant readiness; complete compliance with IEC 62304, ISO 14971 or ISO 13485. These are possible future milestones, not present facts.
Five problems nobody has solved, AxonOS included
- Calibration-free decoding across subjects
- Worst-case execution time on a modern core
- Long-session non-stationarity
- Enforcing consent at the point of use
- Establishing that a signal is voluntary
@article{axonos2026microkernel,
title = {An Analytical Microkernel Design for Safety-Critical
Brain--Computer Interfaces: Schedulability, Capability
Isolation, and Falsifiable Predictions},
author = {Yermakou, Denis},
year = {2026},
doi = {10.5281/zenodo.20552007},
url = {https://doi.org/10.5281/zenodo.20552007},
note = {Analytical bounds; predictions P1--P5; no measurement claims},
license = {CC-BY-4.0}
}Every repository exposes Cite this repository through CITATION.cff.
| Artefact | License |
|---|---|
| Kernel, SDK, consent, swarm, gateway | Apache-2.0 OR MIT |
| RFCs and specifications | CC-BY-SA-4.0 |
axon-bci-gateway |
MIT, preserved from upstream OpenBCI_GUI |
neural-boundary-game |
AGPL-3.0-only OR AxonOS Commercial |
© The AxonOS Project / Denis Yermakou
connect@axonos.org · security@axonos.org · LinkedIn · axonos.org
日本語 · 中文 · Italiano · Français · Deutsch · Español · العربية — translations summarise this page; the English page is canonical.