Telemetry histories influence monitoring, diagnosis, and automated system decisions, yet lightweight integrity mechanisms are often deployed as ad hoc checksums with little formal connection between mathematical intent and executable code. We present K-Sentry, an order-sensitive telemetry accumulator that binds each log entry to its position through modular weights while maintaining a compact streaming state. The design detects edits, reorderings, insertions, deletions, and truncations, and also supports compositional reasoning over trace segments.
We implement K-Sentry in Rust and verify refinement in Verus. The development machine-checks weight computation, per-step updates, prefix correctness, whole-stream correctness, shifted composition, collision characterization, and first-mismatch localization for equal-length traces. We further derive a probabilistic collision bound for uniformly chosen bases using a small trusted algebraic lemma.