billnas

Quick context for anyone digging into the C-slot spec: it's the admission layer of a multi-layer deterministic settlement system. Other layers (clock coordination, recovery, finality) are at various stages of formalization. Vortexdse architecture @billnas25

@RSoulatIOHK @mkindahl If you do get a Lean translation running, I'd be very interested in the k-induction results — happy for you to publish them.

@billnas25 @mkindahl Looks fun! Is the model available? I’d love to translate it to Lean to benchmark our State machine and k induction capabilities

Per-node clocks. Bounded skew. Byzantine attacker spoofs timestamp + sender ID. TLC: 96,481 states / 10,099 distinct / 6 invariants / 0 errors. Plus: executable spec — 10/10 scenarios pass. C-slot holds. @mkindahl @RSoulatIOHK

@RSoulatIOHK @mkindahl Here's the repo: github.com/vasilisnasopou… Two TLA+ modules (base safety/liveness + Skew adversarial), configs, TLC logs, and a JS reference impl. Apache-2.0.

@RSoulatIOHK @mkindahl Yes, gladly. Three TLA+ modules — safety / liveness / adversarial (per-node clocks + Byzantine origin spoofing) — plus configs, logs, and a JS reference impl. Pushing the repo , will share the link.

Vortex DSE — C-slot admission verified. Safety (TLC, exhaustive): 608,477 distinct, depth 23, 0 errors. Safety (Apalache, symbolic): 6 invariants, length=8, 0 ctex. Liveness (TLC): 2 properties, 0 errors — tick progresses, crashed nodes rejoin. No leader. No quorum. No agreement.

Vortex DSE — deterministic exactly-once admission, formally verified. Not a TTL window. Async reorder. Unbounded delay. Crash/rejoin. Adversarial replay. Holds. TLC: 608,477 distinct states, depth 23, 0 errors (exhaustive). Apalache: 6 invariants, length=8, 0 ctex. No leader. No quorum. No agreement.@k0nn0v @MarcJBrooker @audithare @KingBootoshi

@Franc0Fernand0 whats your opinion?

Vortex DSE — two safety invariants checked with Apalache symbolic SMT (Informal Systems). TemporalBound · length=10 · EXITCODE: OK ReplayBounded · length=10 · EXITCODE: OK 0 counterexamples. Independent of prior TLC explicit-state run (21,959 states, 11 invariants, 0 errors).@k0nn0v @muratdemirbas

@Franc0Fernand0 Amazing!!!👍👍👍

Fresh air, hikes, nature, and gorgeous landscapes. It was a beautiful long weekend in the Austrian Alps.

Just testing the Kerberos TTL gate (1988) against classic Lamport replay (1978) in TLA+. Classic spec: NoStaleDelivery violated in 7 steps.
Same spec + clock[p] ≤ m.ts + TTL on Receive: holds across 27K states. Two old ideas, one TLC run.

Lamport clocks (1978): ordering, no replay protection. Added one conjunct to Receive:
clock[p] ≤ m.ts + TTL Classic spec: stale delivery in 7 steps.
With the gate: 27,097 states, no violation. Same spec. One line. @muratdemirbas @k0nn0v @MarcJBrooker

Two-Phase Commit (1978) has a textbook failure mode: coordinator dies, replicas stuck in "prepared" forever. Modeled it in TLA+. Scaled 3 → 7 nodes. •Classic: violates EventualResolution at every size. •Same protocol + deterministic TTL gate: holds at every size. @k0nn0v @muratdemirbas

That's a textbook problem in distributed systems since 1978. I used TLA+ to encode a referee-less version with my Vortex work. The model checker explored 2043 scenarios — none froze.

Encoded classic 2PC in TLA+ with explicit coordinator-crash. EventualResolution violated in 5 steps — textbook blocking (Gray '78). Replaced coordinator with a deterministic TTL-bounded rule from my Vortex work. 2043 states, 0 violations. @k0nn0v @tlaplus @MarcJBrooker

@github @TheHackersNews @ycombinator