Distributed systems · coordination · leaderless consensus
Vasilis Nasopoulos
I work on Vortex DSE, a leaderless protocol that runs consensus only where it is provably unavoidable — on silence — and exactly as much as needed. Order and winner are computed by every node from the content, with no vote. The specifications and safety proofs below are public and machine-checked; the engine itself is not.
See it before reading about it
Two things you can check for yourself, before deciding whether any of the rest is worth your time.
Three bookings for one airline seat, and three clocks you can drag. One side changes its mind about who gets it; the other cannot.
Pick the order →An open challenge: choose the arrival order for 3,000 transactions — any permutation you like. The ledger hash comes out the same. Send a number and test it.
Where to start
Three entry points, in increasing depth.
Where coordination is unavoidable, and how little of it is enough: agreement on silence, exactly τ. TLAPS proofs and TLC models.
2 · Executable specificationThe strict admission model in TLA⁺, with reference scenarios and TLC configurations.
3 · Machine-checked proofsTLAPS deductive proofs of admission safety. CI fails the build if any obligation is left unproved.
What is actually proved
Bounded model checking and deductive proof are different guarantees, so the distinction is kept explicit rather than collapsed into one number.
- ✓ Exactly-once admission — 131 obligations, TLAPS, unbounded.
- ✓ Type safety & no-future admission — 194 obligations, TLAPS, unbounded.
- ✓ Per-slot agreement — TLC and Apalache, two independent checkers, bounded; plus a Lean 4 inductive proof.
- ✓ Where coordination goes (the Silence Theorem) — the only coordination a decision needs is agreement on silence, exactly τ of it; TLAPS, public in where-coordination-goes.
- · Bounded latency — stated for the core in flooding rounds, not seconds; the proof body is
OMITTED, so it is not a machine-checked result.
One claim that does not rest on me
Everything above is my own work, checked with my own tools. This is the exception. On 25 August I published a small property under CC BY 4.0. Within three days, three independent engineers had taken it further than I had.
- ✓ Made executable — turned into a crash benchmark against LangGraph, where it found failures.
- ✓ Reproduced — by a second person, on different hardware and a different checkpoint backend.
- ✓ Extended — by a third, to LangGraph, Temporal and DBOS, reading the side-effect count from a hash-chained ledger in a separate process, so the runtime under test cannot report its own score.
The property states its own limit: at-most-once needs the receiver to honour the identity, because the effect and its durable record live in two different systems. That declared limit is why the third harness measures the receiver instead of assuming it. The three benchmarks above are their authors' own work, not mine; all of it is public in langgraph#8039.