Verification Workflow

This page maps capOS claims to the commands, QEMU smokes, fuzz targets, proof tools, and review documents that currently support them.

Local Command Set

Use the repo aliases and Makefile targets instead of bare host commands. The workspace default Cargo target is x86_64-unknown-none, so host tests rely on aliases that set the host target explicitly.

Scope	Command	What it checks
Formatting	`make fmt-check`	Rust formatting across kernel, shared crates, standalone userspace crates, and demos.
Config and manifest logic	`cargo test-config`	Cap’n Proto manifest encode/decode, CUE value handling, CapSet layout, and config validation.
Ring concurrency model	`cargo test-ring-loom`	Bounded SQ/CQ producer-consumer invariants and corrupted-SQ recovery behavior.
Shared library logic	`cargo test-lib`	ELF parser, frame bitmap, frame ledger, capability table, and property-test coverage.
Manifest tool	`cargo test-mkmanifest`	Host-side manifest conversion and validation behavior.
Userspace runtime	`make capos-rt-check`	`capos-rt` build path, entry ABI, typed clients, ring helpers, and no_std constraints.
Kernel build	`cargo build --features qemu`	Kernel build with the QEMU exit feature enabled.
Generated bindings	`make generated-code-check`	Cap’n Proto compiler path/version, generated output equality, no_std patch anchors, and checked-in baseline drift.
Dependency policy	`make dependency-policy-check`	cargo-deny and cargo-audit policy across root and standalone lockfiles.
Full image build	`make`	Kernel, userspace demos, runtime smoke binaries, manifest, Limine artifacts, and ISO packaging.
Default QEMU smoke	`make run`	End-to-end boot, userspace process output, capability ring, IPC, transfer, VirtualMemory, TLS, cleanup, and final halt paths included in the default manifest.
Spawn QEMU smoke	`make run-spawn`	Init-owned spawn flow, ProcessSpawner hostile cases, child grants, waits, and cleanup.
Networking smoke	`make run-net`	QEMU virtio-net attachment and kernel PCI/device-discovery path.
Kani proofs	`make kani-lib`	Bounded proofs for selected `capos-lib` invariants when `cargo-kani` is installed.

Do not claim full verification unless the relevant command actually ran in the current change. For doc-only changes, use an appropriately narrower check such as mdbook build.

Review Workflow

Identify the changed trust boundary or state that the change is docs-only.
Read REVIEW.md for the applicable security, unsafe, memory, performance, capability, and emergency-path checklist.
Read REVIEW_FINDINGS.md before judging correctness so known open findings are not treated as solved behavior.
For system-design work, list the concrete design and research files read; reviewers should reject vague grounding such as “docs” or “research”.
Run the smallest command set that exercises the changed behavior, then add QEMU proof for user-visible kernel or runtime behavior.
Record unresolved non-critical findings in REVIEW_FINDINGS.md with concrete remediation context before treating the task as reviewed.

Evidence by Claim

Claim type	Required evidence
Parser or manifest validation	Host tests for valid and malformed input; fuzz target when arbitrary bytes can reach the parser.
Kernel/user pointer safety	QEMU hostile-pointer smoke plus code review of address, length, permissions, and validation-to-use windows.
Ring or IPC transport behavior	Host model/property tests where possible, plus QEMU process output proving success and failure paths.
Capability transfer or release	Rollback tests for copy/move/release failure, cap-slot exhaustion, stale caps, and process-exit cleanup.
Resource accounting	Tests that prove quota rejection, matched release on success and failure, and process-exit cleanup.
Generated code or schema changes	`make generated-code-check` and a checked-in baseline diff generated by the pinned compiler.
Dependency or toolchain changes	Dependency-class review plus `make dependency-policy-check`; update `../trusted-build-inputs.md` when trust assumptions change.
Device or DMA work	`make run-net` or a targeted QEMU smoke; no userspace-driver transition without the gates in `../dma-isolation-design.md`.
Panic-surface hardening	Updated `../panic-surface-inventory.md` when reachability or classification changes.

Fuzzing and Proof Tracks

The current fuzz corpus lives under fuzz/ and covers manifest Cap’n Proto input, exported JSON conversion for mkmanifest, and arbitrary ELF parser input. Run fuzzers when a change alters those parsers, schema shape, or validation rules.

Kani coverage is intentionally narrow and lives in capos-lib, where pure logic can be bounded without hardware state. Add or refresh Kani harnesses for ledger, cap-table, bitmap, and parser invariants when those invariants become part of a security claim.

Loom coverage belongs in shared ring logic. Extend cargo test-ring-loom when SQ/CQ ownership, ordering, corruption recovery, or wake semantics change.

Documentation Sources

REVIEW.md: rules for security, unsafe code, capability invariants, resource accounting, and emergency paths.
REVIEW_FINDINGS.md: open remediation backlog and latest verification records.
../trusted-build-inputs.md: trusted compiler, generated-code, dependency, bootloader, manifest, and host-tool inputs.
../panic-surface-inventory.md: classified panic-like surfaces and commands used to generate the inventory.
../authority-accounting-transfer-design.md: authority graph, quota, transfer, rollback, and ProcessSpawner accounting invariants.