Testing Overview

Relevant source files

axiomOS testing is layered by what can be trusted at each level. Host tests cover everything extractable into no_std crates; QEMU smoke tests cover boot and in-guest probes; fuzzing and Miri cover adversarial and unsafe surfaces; Lean proofs cover a small slice of the verifier’s abstract domain; and Raspberry Pi 5 behavior is validated manually.

There is no hardware-in-the-loop CI; Pi 5 testing is manual (README, issue 76). docs/operations/release-verification.md says a local pass must not be taken as physical HIL, independent review, a ForgeFPGA bitstream, or robot-level evidence.

Strategy

Layer	What it checks	Where
Static policy	Formatting, clippy, unsafe-code ledger, inventory, boundaries, generated docs, ABI surface, error policy	`cargo xtask check ...`, `scripts/verify/*.py`
Host unit and integration tests	Kernel subsystems extracted as crates (`kernel_bpf`, `kernel_vfs`, `kernel_elfloader`, and others)	`cargo test -p ...`
Concurrency models	Loom models for the run queue and BPF epoch snapshot	`kernel_run_queue`, `kernel_bpf`
Miri	Undefined behavior in unsafe code	`cargo miri test` per crate
QEMU smoke	Boot reaches `QEMU_BOOT_OK`, `init` probes pass	audit gate, `scripts/test/smoke-bpf.sh`
Fuzzing	Verifier, signed container, ring buffer, ELF loader, syscall arguments, bridge protocol	`cargo fuzz`
Formal proofs	Tnum operator soundness in Lean	`formal/`
Hardware validation	GPIO, e-stop, PWM, timing on real boards	`scripts/hil/`, manual runbook

The kernel binary cannot run standard Rust unit tests because it uses a custom linker script. CONTRIBUTING.md therefore asks that new functionality be extracted into separate host-testable crates where possible.

Gate flow

Commands

From docs/operations/testing.md:


cargo xtask check inventory
cargo xtask check boundary
cargo xtask check docs
cargo xtask check all --profile quick --no-qemu
cargo xtask check all --profile full

Substantial runs retain the command, environment, commit, results, summary and logs under ignored artifacts/runs/ directories.

Pages

Page	Covers
Tests	Host tests, kernel tests, script tests, smoke, fuzzing
CI and gates	Manifests, profiles, xtask checks, GitHub workflows
Formal verification	Lean tnum proofs
Hardware-in-the-loop	HIL scripts and manual Pi 5 validation