- The AxonOS Consent Specification — a solo specification by Denis Yermakou, defining the kernel-level state machine that mediates user permission for
IntentObservationflow in a conformant AxonOS deployment. - The reference Rust implementation —
#![no_std],#![forbid(unsafe_code)], targeting ARMv8-M Cortex-M. - The Kani Bounded Model Checking harnesses that produce the L1 evidence backing every timing claim.
- The conformance test vectors that any independent implementation must pass, dedicated to the public domain under CC0-1.0.
This is a standalone subsystem of the AxonOS Project. No external co-authors. No external coupling-protocol dependencies. The specification is downstream of the AxonOS Standard §6.
┌───────────┐
│ Granted │◄────────────┐
└─────┬─────┘ │
│ │
user pause│ user resume │
▼ │
┌───────────┐ │
│ Suspended │─────────────┘
└─────┬─────┘
│
user revoke (also from Granted)
▼
┌───────────┐
│ Withdrawn │ (terminal — requires new manifest install)
└───────────┘
Withdrawn is terminal. The only path back is a fresh manifest install through the trusted path. This non-reversibility is the central anti-coercion property.
Correction, published 2026-08-16. Until this revision the ≤ 1648 cycle bound was tagged
L1 (Kani-proven)here, inSPEC.md§4.1 and in thehandle_event()doc comment, and SPEC §4.1 namedhandle_withdraw_terminatesas the harness backing it. That harness proves termination and target-state correctness; it contains no cycle assertion, and Kani cannot produce one. The cycle figure is an analytical bound derived by instruction counting, and is now tagged as such. Separately, the harness exercises theGrantedstarting state only, although its doc comment said "any starting state" — corrected, and the coverage gap is recorded as open. Nothing about the measured L2 figures below changes. Per the AxonOS Standard, this notice is permanent.
| Property | Value | Evidence level |
|---|---|---|
| Cycles per transition (upper bound) | ≤ 1648 | analytical — instruction-count derived, derivation pending |
| Wall-clock per transition (upper bound) | ≤ 9.8 µs | analytical — the cycle bound at 168 MHz |
| Transition terminates, target state correct | proven | L1 — Kani handle_withdraw_terminates |
| End-to-end withdrawal → stream termination | ≤ 10 ms | composed, see SPEC §4.2 |
| Median (measured, 18-h soak, 12 × 10⁶ events) | 1098 cycles · ≈ 6.5 µs | L2 |
| 99.9th percentile (measured) | 1487 cycles · ≈ 8.85 µs | L2 |
| Worst observed (measured) | 1503 cycles · ≈ 8.95 µs | L2 |
| Soak duration with zero unsafe states | 18 h / 12 × 10⁶ events | L2 |
| Critical-path allocations | 0 | static analysis |
Source lines (src/) |
594 | — |
| Unsafe blocks | 0 | #![forbid(unsafe_code)] |
| Kani harnesses | 5 | passing in CI |
All measurements remain within the L1 bound. No Kani counterexamples are known for the current verification surface.
Every push and pull-request runs the full CI matrix in .github/workflows/ci.yml. The eight CI jobs:
| Job | What it checks | Blocking |
|---|---|---|
Format (rustfmt) |
cargo fmt --all --check — source is cargo fmt-clean |
✅ |
Lint (clippy) |
cargo clippy --all-features --all-targets — no lint errors |
✅ |
Test (ubuntu, stable) |
cargo test with both --all-features and --no-default-features |
✅ |
Build no_std (Cortex-M4F) |
cargo build --target thumbv7em-none-eabihf --no-default-features --release |
✅ |
Documentation (rustdoc) |
cargo doc --no-deps with RUSTDOCFLAGS=-D warnings (no broken intra-doc links) |
✅ |
License files & SPDX |
All five LICENSE files present with correct SPDX identifiers | ✅ |
Fuzz (build + 60s smoke) |
Builds the three cargo-fuzz targets and smoke-runs each for 60 s on nightly |
✅ |
CI (aggregate) |
Green check iff every job above passed | ✅ |
A red X on any job blocks the merge. The aggregate CI job is what the branch-protection rule watches.
axonos-consent/
├── SPEC.md ← canonical specification (this is the source of truth)
├── README.md ← this file
├── CHANGELOG.md ← version history (see the releases page for the current release)
├── Cargo.toml ← crate manifest; MSRV 1.75
├── LICENSE ← Apache-2.0 OR MIT dispatcher for code
├── LICENSE-APACHE ← Apache-2.0 full text
├── LICENSE-MIT ← MIT full text
├── LICENSE-CC-BY-SA ← CC-BY-SA-4.0 full text for the specification
├── rustfmt.toml ← formatting configuration
├── rust-toolchain.toml ← pins stable + rustfmt + clippy + thumbv7em
│
├── src/ ← reference Rust implementation (#![no_std])
│ ├── lib.rs ← crate root, exports, doctest
│ ├── state.rs ← consent FSM with AtomicU8
│ ├── wire.rs ← 16-byte little-endian wire format
│ ├── crypto.rs ← constant-time signature verification
│ ├── error.rs ← typed error taxonomy
│ ├── interlock.rs ← ObservationGate trait for kernel IPC integration
│ └── dual_control.rs ← multi-party (guardian) co-authorisation (v0.5.0)
│
├── kani/ ← Bounded-model-checking harnesses (L1 evidence)
│ ├── handle_withdraw_terminates.rs
│ ├── fsm_no_invalid_transitions.rs
│ ├── cbor_decoder_bounded.rs
│ ├── signature_verification_constant_time.rs
│ └── co_authorisation_requires_two_parties.rs
│
├── tests/ ← unit + integration + property tests
│ ├── integration.rs ← full FSM lifecycle
│ └── wire_format.rs ← wire-format roundtrip + refusal cases
│
├── benches/ ← L2 measurement harnesses
│ └── withdrawal_latency.rs
│
├── examples/ ← worked usage examples
│ ├── basic_usage.rs ← (requires the `std` feature)
│ └── dual_control.rs ← guardian co-authorisation walkthrough
│
├── vectors/ ← conformance test vectors (CC0-1.0; public domain)
│ ├── README.md
│ └── LICENSE
│
├── fuzz/ ← coverage-guided fuzz suite (cargo-fuzz; L2 evidence)
│ ├── fuzz_targets/ ← wire_decode, roundtrip, fsm_sequence
│ ├── corpus/ ← committed seed corpus
│ └── README.md ← how to build, run, and triage
│
├── docs/ ← informative companion documents
│ ├── ARCHITECTURE.md
│ ├── SECURITY-MODEL.md
│ ├── DESIGN-RATIONALE.md
│ └── citation.bib
│
└── .github/workflows/
└── ci.yml ← 8-job CI: fmt, clippy, test, no_std build, docs, license, fuzz, aggregate
Add to your Cargo.toml:
[dependencies]
axonos-consent = "0.4"Use:
use axonos_consent::{ConsentMachine, ConsentState};
let manifest_id: u16 = 1;
let trusted_path_pubkey = [0u8; 32]; // Ed25519 public key
let machine = ConsentMachine::new(manifest_id, trusted_path_pubkey);
assert_eq!(machine.state(), ConsentState::Granted);A worked example covering the full FSM lifecycle is in examples/basic_usage.rs.
# Install Kani once
cargo install --locked kani-verifier
cargo kani setup
# Run all five harnesses
cargo kani --harness handle_withdraw_terminates
cargo kani --harness fsm_no_invalid_transitions
cargo kani --harness cbor_decoder_bounded
cargo kani --harness signature_verification_constant_timeEach harness prints VERIFICATION SUCCESSFUL on a passing run. A counterexample, if any, is reported with the input that violates the bound.
Alongside the L1 Kani harnesses, the reference implementation carries a
coverage-guided fuzz suite in fuzz/, built on cargo-fuzz /
libFuzzer. Three targets search the unbounded input space for a
specification or implementation defect:
| Target | Surface | Property |
|---|---|---|
wire_decode |
§6 wire-format decoder | totality — never panics on any byte buffer |
roundtrip |
§6 encode/decode | canonical encoding — no two buffers denote one event |
fsm_sequence |
§2–§3 state machine | FSM invariants under arbitrary signed-event streams |
cargo install cargo-fuzz --locked
cargo +nightly fuzz run wire_decode # or roundtrip, fsm_sequenceThe Kani harnesses are L1 evidence (exhaustive proof over a bounded space);
fuzzing is L2-class evidence (a large, coverage-guided sample of the unbounded
space). CI builds all three targets and smoke-runs each for 60 s on every
change. See fuzz/README.md and SPEC §10.3.
Independent implementations can run the conformance vectors:
cargo test --test conformance_vectorsFor implementations in languages other than Rust, the vectors are exported in canonical binary form at vectors/ under CC0-1.0; replay with any wire-format-aware driver.
The crate is published as 0.y.z: the implementation surface is not yet locked, and a v1.0.0 release will accompany the second independent implementation. For the current release and its notes, see the releases page and CHANGELOG.md.
The single-party specification protocol is stable as of v0.3.0 and unchanged since: v0.4.0 recorded added validation evidence (SPEC §10.3) and v0.5.0 added the optional multi-party (guardian) co-authorisation profile (SPEC §12) without altering the single-party baseline. The 0.6 and 0.7 releases are implementation, licensing, and CI changes only — they do not touch the wire protocol. An implementation conformant with the v0.4.0 protocol is conformant with the current baseline profile without modification.
For clinical deployments — the ALS rehabilitation pilot in the canonical
Standard's roadmap is the motivating case — a guardian can co-authorise consent
changes together with the patient. This is the optional dual_control
layer, specified normatively in SPEC §12.
It follows the safe-direction principle:
- Either party may reduce neural-data exposure (
Suspended,Withdrawn) unilaterally. The flow can always be stopped by one signature. - Resuming the flow (
Suspended → Granted) requires both parties to authorise the same transition within a bounded window. No sequence of signatures from one party can resume it — a property proven by the Kani harnessco_authorisation_requires_two_parties.
The single-party ConsentMachine is unchanged; multi-party is opt-in by using
DualControlMachine instead. See examples/dual_control.rs.
| Layer | Repository | Role |
|---|---|---|
| Canonical standard | axonos-standard |
Architecture manual, conformance criteria, validation taxonomy |
| Engineering RFCs | axonos-rfcs |
Numbered design proposals; normative once finalised |
| Kernel substrate | axonos-kernel |
EDF scheduling, SPSC IPC, capability gate, monotonic time |
| Application boundary | axonos-sdk |
Typed intents, manifests, ABI-compatible integration |
| Consent layer | axonos-consent |
Deterministic consent FSM + optional multi-party co-authorisation (this repository) |
| Consent protocol | axonos-protocol |
Network-level consent protocol; bounded CBOR frames, exhaustive state machine |
| Conformance | axonos-conformance |
Byte-exact RFC-0005 / RFC-0006 vectors across Rust, Python, C, JavaScript, Java |
| Validation | axonos-validation |
Raw measurement traces and reproducible post-processing |
| Mesh coordination | axonos-swarm |
Distributed timing, co-availability, peer health monitoring |
| Acquisition gateway | axon-bci-gateway |
OpenBCI GUI integration fork for EEG input |
Contributions are welcome under a high bar appropriate to safety-relevant
infrastructure. See CONTRIBUTING.md for the development
environment, the local gate, the evidence discipline, and the cognitive-data
rule, and CODE_OF_CONDUCT.md. Report vulnerabilities
privately per SECURITY.md — never in a public issue.
This repository is authored solely by Denis Yermakou — AxonOS Project, Singapore.
- Specification text: SPEC.md — Denis Yermakou.
- Reference implementation: same author, same project.
- No external co-authors. No external coupling-protocol dependencies.
Inquiries: connect@axonos.org · Security: security@axonos.org.
| Surface | License |
|---|---|
Source code (src/, tests/, benches/, examples/) |
Apache-2.0 OR MIT at your option |
Specification text (SPEC.md, docs/, README.md) |
CC-BY-SA-4.0 |
Conformance test vectors (vectors/) |
CC0-1.0 — public domain dedication |
The test vectors are CC0 specifically so any independent implementation — in any language, under any license, commercial or otherwise — can use them without compatibility concerns.
axonos-consent · multi-party co-authorisation
Singapore · Zurich · Berlin · Milano · San Mateo