axiomOS is a bare-metal Rust kernel that admits new behavior at runtime — control loops, sensor pipelines, syscall policies — only after a verifier discharges proofs of termination, bounded memory, and safety. No reflash. No reboot. No surprises.
At the very bottom of every robot, drone, or factory machine sits a kernel — the core program that controls the motors, reads the sensors, and keeps everything in time.
Today, changing that kernel means rebuilding it, reinstalling it on the device, and praying nothing breaks. Teams are so afraid of bricking machines in the field that they freeze the kernel and never improve it. Bugs pile up. Motors stutter. Nobody can see why.
axiomOS changes that. It lets you send a small, new piece of behavior to a running machine — a better control loop, a safety rule, a debugging probe — without reinstalling anything or turning it off.
And before that new behavior is allowed to run, the kernel mathematically checks that it is safe: it can't crash the machine, can't loop forever, can't touch memory it shouldn't. If the proof fails, it never runs. That's the whole idea.
Linux is a general-purpose kernel built for servers and desktops. axiomOS is purpose-built for machines that must change in the field without the risk of a reflash.
Note — this is not eBPF bolted onto Linux. axiomOS is a kernel designed from day one around safe, verified, runtime-loadable programs.
Each is a verified program attached to a live kernel hook. Each reads plainly to anyone watching the machine; each maps to a real attach point in the kernel today.
A motor stutters in the field and nobody can reproduce it.
Attach a verified probe to the PWM driver on the running machine. Within seconds you see the exact timing anomaly that userspace logging never caught — no rebuild, no reflash.
pwm_event A limit switch must stop the motor even if the main software crashes.
A verified program on the GPIO interrupt enforces the cutoff inside the kernel. Userspace can crash, hang, or be compromised — the motor still stops. The rule cannot be bypassed.
gpio You want to try a smarter scheduling policy without taking the robot offline.
Load a new policy program and attach it to the scheduler's task-switch hook on the live system. The change takes effect immediately. Roll it back just as fast.
sched_switch Most embedded systems offer a choice: a kernel you cannot modify, or a modification you cannot trust. We refuse the choice.
Every program attached to a kernel hook must discharge a proof: termination, bounded stack, validated memory access. The verifier is the contract; the kernel only runs what it has read.
Sensor fusion, control loops, safety policies — these change in the field. A reflash is a risk. We hot-attach verified bytecode to syscalls, timers, GPIO, PWM, and detach without reboot.
Sub-millisecond control loops cannot tolerate Linux's millisecond-class jitter. axiomOS boots directly on hardware via Limine or device tree — no host OS, no firmware runtime, total control of the interrupt path.
Memory safety is structural. The kernel is ~95% Rust, no_std, panic=abort, with unsafe blocks documented and audited. Whole classes of kernel bugs — use-after-free, data races, iterator invalidation — never compile.
Microkernel IPC at the control-loop layer costs hundreds of nanoseconds per message. axiomOS uses Rust trait boundaries to keep subsystems composable without paying the price of address-space crossings.
Open architecture doc →Behavior hardcoded into Linux — drivers, filters, scheduling policy — becomes loadable, verified programs in axiomOS. The kernel core stays minimal, auditable, and rarely changes.
Trusted. Contains the unsafe code and the verification engine. Minimal surface area.
Safe by construction. Cannot corrupt the kernel; can have logic bugs. Loaded and unloaded at runtime.
Untrusted. Isolated by virtual memory. Applications, tools, services.
Before bytecode reaches the dispatcher, the verifier walks every path: building a control-flow graph, refining ranges across branches, tracking per-instruction liveness, and pruning equivalent states. A program that cannot be proven safe will never run.
// crates/kernel_bpf/src/verifier/walk.rs
fn verify_program(bytecode: &[u8]) -> Result<Verified, VerifyError>
let cfg = build_cfg(bytecode)?;
// 01 — termination
for node in cfg.nodes()
if has_backedge(node) && !has_bounded_iter(node)
return Err(VerifyError::UnboundedLoop);
// 02 — tnum + range refinement after branches
let abs = abstract_interpret(&cfg)?;
// 03 — stack and memory invariants
abs.assert_stack_depth(STACK_LIMIT)?;
abs.assert_memory_access(&cfg)?;
Ok(Verified bytecode, abs )
Honest accounting. No "soon" markers. Either something is in `main` and exercised by tests, or it isn't.
The kernel boots, the verifier works, and the benchmarks are real. The one claim left to make undeniable: a verified program loaded into a running machine, changing its behavior live, all the way out to a robotics ROS2 topic — no reboot.
See the full roadmap →Clone the repo, boot it under QEMU, attach a probe to a syscall, and watch the verifier read your code back to you.
git clone https://github.com/pro-utkarshM/axiomOS cd axiomOS && cargo run ./scripts/build-rpi5.sh # for hardware