Test plan

Run the checks that establish the affected behavior. Keep model, process and service-manager evidence distinct.

Repository checks

Rust 1.89 is pinned. Python 3 runs the self-cleaning native walkthrough and documentation checks. No JavaScript runtime or package manager is required.

python3 scripts/check-docs.py
cargo fmt --all --check
cargo clippy --locked --all-targets --all-features -- -D warnings
cargo test --locked --all-targets --all-features
python3 scripts/verify-native-examples.py
cargo run --locked --bin k-harness -- sim --seeds 256 --start-seed 1 --json
cargo package --locked
elan run leanprover/lean4:v4.34.0 lean formal/Protocol.lean

Coverage map

Suite	Behavior
download, source	Digest/size, gzip, resume, stalled HTTP, proxy behavior and manifest selection.
durable, compatibility	Torn-tail repair, rejection of complete corruption, promotion redo, fixed v1 format samples and real-process lock exclusion/dead-owner recovery.
engine, simulation, invariants	Write-ahead effects, crash recovery, predicate refusal, deterministic seeds and mutation self-checks.
runner, protocol, serve	Policy, ownership, consent, compatibility, receipts/replay, bounded input and malformed requests.
process	Native controller timeouts, killed/hung workers, operation-bound receipts, retained worker verification and bounded recovery.
acceptance	Native controller upgrade/rollback and executable self-replacement, with negative controls.
quarantine	Safe-handoff evidence, canonical paths, shared lock and no overwrite of displaced state.

Suite

Behavior

download, source

Digest/size, gzip, resume, stalled HTTP, proxy behavior and manifest selection.

durable, compatibility

Torn-tail repair, rejection of complete corruption, promotion redo, fixed v1 format samples and real-process lock exclusion/dead-owner recovery.

engine, simulation, invariants

Write-ahead effects, crash recovery, predicate refusal, deterministic seeds and mutation self-checks.

runner, protocol, serve

Policy, ownership, consent, compatibility, receipts/replay, bounded input and malformed requests.

process

Native controller timeouts, killed/hung workers, operation-bound receipts, retained worker verification and bounded recovery.

acceptance

Native controller upgrade/rollback and executable self-replacement, with negative controls.

quarantine

Safe-handoff evidence, canonical paths, shared lock and no overwrite of displaced state.

Transaction completion gate

Test real worker termination before takeover; reject mismatched receipts and corrupt recovery bytes; bound both worker and recovery hangs; require a durable outcome or explicit unresolved result. Journal fault cases establish ordering, while actual process tests establish process lifetime. Keep both positive and negative cases. Same-id replay must not repeat effects; another target with that id must be refused.

Maintaining test quality

Use isolated identities, temporary directories and owned processes. Clean on failure. Preserve the first failure when retrying; never delete assertions, silently skip a platform or report model tests as service acceptance. Fixed v1 samples protect disk compatibility without retaining another implementation. Run only affected checks during iteration and all required gates for a release.

cargo run --locked --release --bin k-harness -- sim --start-seed 1 --seeds 50000

The nightly workflow retains failing-seed corpora for replay. Changes to phases, intent ordering or effects also require reviewing the Lean projection.

Platform and product acceptance

CI requires Linux, macOS and Windows checks, including native examples and packaged-source builds. Lean runs separately. Passing K CI does not certify every service manager or target architecture.

For each product target, verify clean installation, repeated installation, owner refusal, live upgrade, bad-candidate rollback, offline recovery and independence from the resident's service boundary. Verify workload/data preservation, enrollment and cloud reconnection when promised. Tests of a product's launchd/systemd integration provide product-level evidence beyond K's generic controller contract.

Physical power loss and product reboot hooks require separate evidence. POSIX directory synchronization and Windows image semantics are documented in the reference; Windows directory sync does not provide the same durability guarantee.