Formal methods · TLA⁺ · TLAPS · distributed consensus
Vasilis Nasopoulos
I work on Vortex DSE, a deterministic consensus protocol that reaches finality without leader election, voting, or gossip. 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.
Motivation, terminology, and what the protocol does and does not claim. Includes a runnable toy demo.
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.
- ✓ Bounded latency — proved for the core, with two diameter-induction steps left explicitly
OMITTEDrather than silently open.
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.
Testnet
Three nodes in Frankfurt, Tokyo and Los Angeles, running continuously. The figures below are what those nodes measure and report. Two of them are worth explaining, because the numbers mean nothing without the problem they answer.
These nodes time the distance between themselves. Light takes what it takes: 244 ms between Frankfurt and Tokyo cannot be faked downward. Three copies on one machine would answer each other in microseconds, and the system flags any pair that close as sharing a host. None are flagged here.
Beta
The network above has been running unattended. A small number of outside nodes will be invited to join it. Participants are chosen rather than admitted on request, and the list is kept short on purpose.
What you would be doing: running one node, on your own machine, against those three. It registers with the bootstrap, discovers the others, and joins — one token, no files edited by hand.
There is no SLA and no uptime guarantee, and the engine on those nodes is a production candidate rather than a released product. The bootstrap does not speak TLS yet either, which is one of the things we sort out before a node of yours joins.