How we test

A database is trusted for what it survives. Every part of UltraFabric is checked against a simpler model of itself, with failures injected, before it is made fast.

Simulated crashes

A simulated disk injects the failures real disks produce: torn writes, reordered writes, fsync calls that report success without persisting, full disks and flipped bits. A campaign of a million randomized crash points against the write-ahead log, and smaller campaigns against the full engine, check that every acknowledged write is recovered and nothing else appears. Every run is reproducible from its seed.

Differential testing

The same random workloads run against UltraFabric, RocksDB and a deliberately simple in-memory model, and every read is compared. In the query layer, a reference interpreter plays the same role: it defines the right answer that the fast executor and every optimizer rewrite must match.

Tenant isolation testing

For each generated query we build a second database that differs only in what the requester may not see: other tenants' rows, fields masked for them, and rows every access rule hides. Both databases must give the same answer, in the reference interpreter and in the executor. Deliberately broken plans are caught by the same test.

Ten million queries

A nightly runner checks generated queries at scale: executor against reference, every optimizer rewrite in both, encoding round trips, and an isolation check on every tenth query. The first run of ten million found no wrong answer and no isolation failure. It did stop three times on resource limits, and each stop became a permanent test.

Proofs

Eight rewrite laws the optimizer uses (moving filters through projections, joins, unions, grouping and sorting) and the isolation guarantee for the core operators are proved in Lean 4, with no unproved steps. The proofs cover queries without runtime errors; the error rules are tested instead.

Model checking

The write-ahead log and group commit protocol are modelled in TLA+ and checked with TLC: recovery always yields a prefix of acknowledged writes, and nothing is acknowledged before it is durable.

Mutation testing

We change the code on purpose (drop a check, flip a comparison) and confirm the tests fail. Survivors become new tests. In the query plan layer, 19 of 20 mutations were caught; the twentieth disabled a backup check that the other checks already cover. In the test harnesses themselves, three planted defects first went unnoticed; the harnesses gained self-checks and now catch all seven.

Independent references

• The BLAKE3 hash matches the 35 official test vectors.
• Plan and value encodings match the reference protobuf compiler byte for byte, in both directions.

Benchmarks

Measured 19 October 2026 in the same run for both engines, with fsync on every write and no compression. RocksDB still has lower tail latency on point reads, and both engines are limited by the disk on write-heavy workloads. Memory and disk use are at or below RocksDB's on these runs.