Research

Research

Hyphae is developed as a research artifact as much as a product: a formally modeled commit protocol, a bare-metal evidence trail, and a manuscript in preparation that treats the repository's receipts as its primary evidence.

How Hyphae publishes claims

Hyphae has no separate research-publication policy document; the same wording rules that govern the product's marketing govern any paper or public statement, set out in docs/product/claims.md:

  • Every latency number carries its environment class and its receipt. Only class 3 — dedicated hardware, byte-identical workloads, pinned baseline versions — supports a comparative statement.
  • Named third-party systems are measurement subjects and prior art, never adversaries. Comparisons use neutral verbs ("measures", "records", "differs by"), never combative ones ("beats", "crushes", "dethrones") in any language, in either direction.
  • A comparison records the other system's stronger results with the same prominence as Hyphae's, and states the baseline's version, configuration, durability posture, and shared workload definition.
  • Prohibited claim shapes: "universal SQL", "drop-in replacement", "protocol compatible", "serializable" in any form, "distributed"/"replicated"/"highly available", and any latency number without its environment class and receipt.
  • A formal model is evidence about the protocol as specified — never presented as a proof of the Rust implementation. Implementation fidelity is carried separately by the physical crash matrices.

Manuscript in preparation

"One commit, three engines: bounded, verifiable multi-engine transactions in a single process."
Status: draft v0.1, 2026-09-04, record state per claim. Author: Hyphae Research Foundation.

The draft labels every claim Reproduced (repeated on another machine under the public protocol — the TLC model check, the strict-durability commit, the 250k ladder, the baselines) or Measured (one run of the 3.0.0 code on dedicated hardware — the 1.02 ms cross-engine transaction, the 1M rung). The ledger maps each number to its receipt file, commit, host class and caveat, and lists the gaps no receipt yet covers.

Thesis

A single process can run relational SQL, a native data-structure engine, and lexical/vector search over one write-ahead log, one MVCC snapshot space, and one commit sequence number — so that a transaction touching all three engines becomes visible at exactly one CSN in all of them, or in none — and this bound can be stated precisely enough to model-check, and cheaply enough to hold at scale, without hiding where a general-purpose engine still loses to a specialized one.

The evidence it rests on

  • The all-engine transaction contract itself: a delta-staged commit across SQL, structure, and search measured at 1.02 ms p50, roughly 45× cheaper than the materialized path it replaced (46.6 ms p50) — see the bare-metal receipt, §4.
  • The delta-transaction scaling sweep, showing per-commit latency flat at 193–202 µs across three orders of magnitude of prior key history — same receipt, §5.
  • The TLA+ model of the cross-engine commit protocol (docs/formal/HyphaeCommit.tla), checked exhaustively to depth 30 over 79,063,806 generated states with no invariant violation — see the 2026-08-30 receipt and its reproduction in the 2026-09-03 re-measurement against matching spec/config/tool digests.
  • The physical crash matrices that carry implementation fidelity for the modeled protocol (tests/all_engine_transaction_g5.rs, examples/process_crash_matrix.rs), and the G8 per-release crash/corruption/resource/power-loss closure that re-runs them — see the gate status document.
  • The bare-metal ablation across durability classes (Strict, Group, Memory) and the honest per-engine comparisons against SQLite, DuckDB, Redis, and Tantivy on the same host and commit — including the results in Hyphae's own favor and the ones in the baseline's, published at equal weight. See the evidence page for the complete tables.

The formal model

docs/formal/HyphaeCommit.tla models the ordered commit boundary walk, serialized writer admission with first-committer-wins, per-transaction durability classes, sequential WAL recovery with broken-tail truncation, and conflict-table reconstruction — the same state machine the physical crash matrix exercises. It is checked against three transactions, two keys, three engines, and up to two crashes, and its crash model deliberately demonstrates rather than hides that a crash may drop an acknowledged Memory commit while never splitting one across engines. Six invariants hold over the complete bounded state space: TypeOk, Atomicity, StrictDurability, FirstCommitterWins, VisiblePrefixComplete, CsnBounded.

java -XX:+UseParallelGC -jar tla2tools.jar \
  -config docs/formal/HyphaeCommit.cfg docs/formal/HyphaeCommit.tla \
  -workers auto -deadlock

Source: docs/formal/README.md.

Evidence index

Every receipt referenced on this site, and every gate closure that produced it, is indexed in one place: docs/gates/evidence/README.md. Nothing is deleted from that index when superseded — an older receipt stays in the repository, marked obsolete in place, next to the one that replaced it.

How to cite

Cite the repository, the exact release tag, and the receipt a claim depends on — not a version number alone:

Hyphae Research Foundation. Hyphae (version 3.0.0).
https://github.com/Hyphae-Research-Foundation/hyphae,
tag release-v3.0.0-crates, commit 24bce1accdff8d14127797afe6f237a57c1cd4f3.

For a specific measurement, add the receipt path — for example docs/gates/evidence/hyphae-3.0-metal-a443c52-2026-09-03.md — so the citation resolves to the exact host, commit, and workload the number came from.