Most time-series databases treat time as a stream of immutable points. Tau treats time as a sequence of half-open intervals [start, end) that tile without gaps or overlap, forming a monoid under concatenation with no boundary ambiguities and a formal algebraic structure.

Corrections work by appending a new layer over the same range. Every layer has a monotonically increasing ID; the highest ID wins at query time: deterministic, no configuration, no coordination. Compaction normalises any stack of N layers into one canonical layer. Every AT, RANGE, and REDUCE result is identical before and after. This is a provable property, checked by property-based tests on every build.

Derived lenses (DERIVE LENS f AS expr) compile expressions into lazy closures at definition time. Closures capture other lens closures so derivations chain; cycle detection runs at DERIVE time by walking the dependency graph.

Algebraic invariants are verified by Hegel/Hypothesis against hundreds of randomised inputs per property. A deterministic simulation tester drives every transport × auth × WAL combination against a reference oracle, injecting faults across hundreds of millions of simulated operations.

Rust · TauQL · WAL · AES-256-GCM · Argon2id · property-based testing · deterministic simulation