Historical repository record migrated on 2026-10-10. Original repository path: docs/experiments/formal/invariant-consolidation.md Original SHA-256: 05c8798da1c485079c6b061cf6877fad869583733caac04f8f9034aede13ace1 Stated outcomes, measured revisions, failures and limits remain historical. Local raw evidence is private and is not uploaded. Relative links and the data-drive prefix were normalized.

Invariant audit and consolidation

Scope: existing product invariants, failure boundaries and the documentation that reports them. Protocol, wire format, sync order, qualification criteria and oracle expectations are unchanged. The matrix remains the claim-level inventory; this record contains this audit's changes.

Corrections

Boundary	Counterexample	Correction
Verification completion	The self-observation service-bus interruption returned outer exit zero without completing the test gate. Two deterministic mocked transport/stop controls reproduced false success and unsafe scratch deletion.	Require an inner command-completion receipt matching unit, command and transport exit; verify termination before cleanup. Preserve incomplete runs and stop errors.
Control size/restart	Accepted, escaped log paths across a valid inventory can serialize beyond the existing 16 MiB reopen limit.	Check complete serialized size before staging the update; preserve the prior bytes and revision on rejection.
Control publication/authorization	Rename succeeds, directory sync fails, caller rolls memory back; disk and live authorization disagree.	Refuse authentication, polling and mutations after uncertain publication until reopen. Keep the existing sync sequence.
Spool exhaustion	Appending sequence u64::MAX could commit before increment overflow, while recovery rejects that record.	Refuse exhausted local sequence space before any write or rotation; reject an exhausted ACK cursor cleanly.

Source and regressions: resource launcher (local checkout reference tools/resource_group.py; not present at origin/main), launcher controls (local checkout reference tools/test_resource_group.py; not present at origin/main), control persistence, inventory regression (local checkout reference crates/fabric-server/tests/control_persistence.rs; not present at origin/main), Spool. The launcher counterexample derives from the preserved self-observation interruption, unit fabric-work-ebacea46880d4b7eb6173f741ed4e6f0. Its historical receipt is not rewritten. Sequence exhaustion is a local preflight refusal: the Spool retains a representable next sequence and does not emit u64::MAX. The server’s wire range is unchanged. The other cases follow boundary analysis of the persistence implementation; their deterministic fixtures assert state preservation and reopening.

Verification

All commands below run through python3 -B tools/resource_group.py -- with 20 GiB maximum, no swap and data-drive scratch/build paths. This audit does not launch remote workloads or a deployment qualification run.

Command after launcher prefix	Outcome
python3 -B tools/test_resource_group.py Containment.test_wrapper_success_without_command_completion_is_incomplete Containment.test_unconfirmed_stop_preserves_scratch_in_place	Exit 1 before repair: both controls failed. Unit fabric-work-7f64027040134f9497ec6a639efda06b.
python3 -B tools/test_resource_group.py	Exit 0, fourteen controls including real child exit 7, malformed/mismatched receipts, populated cgroups and failed stop; unit fabric-work-2d60d17f2057408abcd85b56ae8b9891.
cargo test --locked -p fabric-server --test control_persistence --test self_identity --test control --lib	Exit 0: 79 passed, two registered research probes ignored; unit fabric-work-f318e032cdf343eca120d21c3fa0e87f.
cargo test --locked -p fabric_o11y --lib spindle::spool	Exit 0: thirteen passed; unit fabric-work-6265e040459a4ce3aa88119effd7b759.
cargo xtask checks --profile fast --receipts $FABRIC_DATA/results/invariant-consolidation-fast-01	Exit 0: all seventeen gates passed, including full workspace tests, Clippy, independent oracles, properties, corpus replay and network simulation.
python3 -B tools/bench/labs/cross_system/sweep_documentation.py --out $FABRIC_DATA/results/invariant-consolidation-docs-01	Outcome in the final receipt summary (local evidence omitted from stage); three manual checks, with hooks/CI disabled.

Final receipts, source hashes, resource observations and cleanup are retained under data/invariant-consolidation-01 (local evidence omitted from stage). Cgroup samples in launcher receipts are observed when the command returns, before final service shutdown; they are not guaranteed whole-descendant-lifetime peaks.

Extended Kani/TLC/new coverage-guided fuzz runs were not executed in this audit. Their required cargo-kani, cargo-fuzz and registered TLA+ JAR were unavailable in the inspected environment; finite property/corpus/simulation checks remain in the fast profile. No verification expectation was weakened.

Remaining limits by invariant family

Family	Remaining evidence gap
Fidelity and encoding	Generated/corpus inputs are finite; gRPC/gzip trace intake and general application-metric intake are outside current support.
Custody and recovery	Physical power loss, failure while recording another I/O failure, and arbitrary generation/retry schedules remain unverified.
Control	Authentication occurs before queueing. An already admitted request can commit after revocation; no immediate in-flight cancellation guarantee is established.
Completeness and query	Readable Parquet bit rot is not universally checked by whole-file hashing; arbitrary publication/retention interleavings and direct server-to-query-spec refinement remain open.
Freshness and capacity	Earlier finite measurements do not qualify the current deployment or sustained backlog/latency bounds.
Boundedness and sealing	Full registered shape/scale/mutant/crash acceptance, retention ceiling, tail growth under outage and unchanged long soak are incomplete.
Process lifecycle and installation	Native companion tests do not establish installed-service behavior on the target unified-cgroup host.
Architecture	Crate dependency/purity checks do not prove every adapter's runtime semantics.

The earlier global query-spec OOM mechanism is unresolved; containment prevents an uncapped repeat but does not explain the allocation. Historical failed soak, large-row comparisons, rejected candidates and incomplete pressure receipts stay visible in their original records.

Documentation

Current state now summarizes implemented behavior, decisive results and remaining gates. The experiment index groups records by capability and preserves its original links. Architecture and invariant indexes now identify the implemented bounded sealer and production Walk-tail FOB1 use. Registered protocols, raw results, contract meanings and negative controls remain intact; repetitive per-round process commentary is removed from navigation pages.

The complete fast invocation took 314.5 seconds with approximately 13.4 GiB memory peak and no swap. This is laboratory verification memory, not server RSS. The mounted data drive held build caches and scratch throughout; owned temporary paths and cleanup are enumerated in the final receipt summary.

The first final-receipt collector exited 1 on a field-name mismatch (status instead of the registry’s result). Its failed receipt is preserved; the collector retry checks both result and exit_code and rejects mutated copies. python3 -B tools/resource_group.py -- python3 -B docs/experiments/formal/data/invariant-consolidation-01/closeout.py exited 0, reconciling seventeen fast receipts, three documentation receipts, source hashes and ten cleanup receipts; two altered receipts were rejected. The retry launcher receipt (local evidence omitted from stage) records its own completion and cleanup. Total data-drive use was 45.67 GB, below the 100 GB ceiling; no remote workloads ran.