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 analysed before they run, not benchmarked
after, 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.
Note
axonos-consent 0.9.2. Consent now changes only on a verified Ed25519 signature, never twice for the same sequence number, and a withdrawal is final the instant it is stored. Ten Kani proofs, three loom models, twenty conformance vectors and three fuzz targets run on every push. The line closes AXC-2026-001, a critical advisory against our own consent layer, published with its fix. Release notes · Specification
|
Build — AxonOS |
Measure — DY-WCET |
|
Discover — Radar |
Verify — DY Research |
|
Prove — DY PROOF |
|
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, upper bound | ≤ 1,000 µs · analytical | response-time analysis over analytical per-task WCETs · derivation pending · the scheduler harnesses prove admission and EDF selection, not a time |
| 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, upper bound | ≤ 0.5 µs · analytical | derivation pending · the SPSC harnesses prove the slot loop-free and FIFO, not a time |
| Consent changes only on an authenticated frame; withdrawal is final | proven · L1 | src/proofs.rs · ten harnesses, a blocking CI job · the former kani/ harnesses never compiled and are removed |
| Consent withdrawal, transition time | retracted at consent 0.9.0 | the 1,648-cycle figure was derived for a tag path that no longer exists; Ed25519 verification now dominates admission · SPEC §4.1 |
| Release jitter, σ | 2.1 µs · L2 | RFC-0001 · raw traces pending |
| Kani proofs re-run in CI | 57 · L1 | kernel 30 · consent 10 · signal pipeline 9 · DY-WCET 8 |
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 derived; 972 µs is the worst anyone has seen. A derivation, 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. It is analytical: check the derivation when it is published, or run the reference hardware past it. The scheduler harnesses falsify something narrower, the admission and EDF logic, and a counterexample from Kani does that 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. Run
cargo kaniinaxonos-consent: the ten harnesses insrc/proofs.rs, the job CI runs on every push. Or forge a frame: theauth_forgeryfuzz target verifies against a key whose secret no one holds, so any frame it admits is a forgery. - 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 · 18 languages · last refreshed 02 Oct 2026, 20:07 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 |
Consent enforced by the kernel: Ed25519-authenticated, replay-proof, final the instant it is withdrawn |
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
Offices and a headquarters are under consideration for the future.
日本語 · 中文 · Italiano · Français · Deutsch · Español · العربية — translations summarise this page; the English page is canonical.