Ravel
A distributed database for OpenTelemetry metrics, logs and traces whose only durable storage is an object store, so a strictly acknowledged write survives the crash of any Ravel process with no write-ahead log or replicated ingest layer.
Ravel stores OpenTelemetry data directly on object storage instead of buffering it first in a replicated layer with local disks. An ingest shard builds an immutable columnar segment in memory, writes it and a commit record to the object store, and only then acknowledges the write; the response carries a commit token that lets a following query read that exact write back.
Acknowledgement is strict by default, meaning every batch a point contributed to is durably stored before the caller is told the write succeeded. A buffered mode is available per request, trading that guarantee for lower latency: it acknowledges after the point is queued, and a crash before the flush completes loses that buffered window.
The commit, catalog, lifecycle, resharding and maintenance protocols are modeled in TLA+ and checked with TLC across finite models, with each checked property traced to a Rust symbol and, for most, a named test.