redoq

This Redis-compatible server is kill -9'd every hour. On purpose.

Every data command it answers is machine-checked in Rocq; its recovery-by-replay is a theorem, and this page demonstrates it live: an hourly harness kills the process mid-write-load, the server replays its append-only file, and an independent checker verifies that every acknowledged write survived. Built with the rocqeteer toolchain.

connecting…
–
kills survived
–
acked writes lost
–
acked writes verified
–
last recovery
–
append-only file

Talk to it

redoq 0.0.1 — live instance, resets daily
redoq>
stock clients work too — no SDK, no fork:
redis-cli -h redoq.bb.org.ai -p 16379

Kill log — the last five, verified

when (UTC)writes ackedlostrecoveryverdict
no kills yet — the first one is scheduled within the hour

The trust model, honestly

Proven (machine-checked in Rocq) The semantics of all 22 data commands, the RESP2/RESP3 codecs, and journal replay — for every store and request history, replay reproduces the live state. Axiom-free; Print Assumptions closed.
Trusted (explicit, fault-injected) The socket shell, the fsync path, and a short list of named extraction realizers — each listed in the runtime manifest and differentially tested. The hourly kill you're watching is that list being exercised in public.
Measured (never “proven”) Performance: 95k SET/s AOF-off on our bench box — 93% of Valkey measured same-machine, same-day. Numbers are published measurements, not claims.