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.

325TLAPS obligations discharged

2×RTTlatency bound, no coordination

13 / 13nodes / countries, one state hash

See it before reading about it

Two writes to the same key at the same instant, and three clocks you can drag. One side changes its mind about which write survives; the other cannot.

Order without a clock →

An interactive demonstration of why last-write-wins discards data silently when clocks disagree — and what the alternative looks like.

Where to start

Three entry points, in increasing depth.

1 · Whitepaper

Motivation, terminology, and what the protocol does and does not claim. Includes a runnable toy demo.

2 · Executable specification

The strict admission model in TLA⁺, with reference scenarios and TLC configurations.

3 · Machine-checked proofs

TLAPS 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 OMITTED rather than silently open.

Testnet

loading…

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.

Anyone can claim to run nodes on three continents. Nobody can prove it.

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.

This build is a production candidate, not the engine the published results were measured on. Those come from bounded runs of the core: the most recent, on these same three machines, converged on chain hash c756379c16c8d977 — byte-identical to the single-machine reference, with no shared clock and 241 ms between the furthest pair.