I work on formal methods (TLA+, TLAPS) and distributed systems: where coordination is needed, how much of it, and how to build systems that keep working with no central server. The measurements come from Vortex, my own leaderless engine.
where-coordination-goes — in Hellerstein's Complete CALM framework, the least coordination a commitment needs is a transversal of silences: deciding, before they act, that certain participants' future actions will not count — and exactly how many (τ, in the worst case, for specifications where a refused action leaves no trace). Paper proofs plus TLAPS-checked cores; what is not ours (Berge, coteries/quorums, Hamsaz, …) is stated in the repository.
| Repository | What you will find |
|---|---|
| where-coordination-goes | The Silence Theorem: definitions, proofs (TLAPS), counterexamples, prior art |
| vortex-dse-formal | Formal models of the engine: C-slot admission spec, TLAPS proofs (325 obligations), Merkle agreement layer (TLC + Apalache) |
| vortex-tesla-demo | Three cars, one ledger, no server — Tesla fleet-telemetry data across three continents |
| vortex-festival-demo | Festival payments with no payment server: registers fail at peak and the rest keep going |
| vortex-dss-demo | Drone airspace deconfliction (ASTM F3548 DSS rule) with no leader |
| vortex-testnet-status | Live status of the three-node testnet (Frankfurt · Tokyo · Los Angeles) |
| vortex-dse-whitepaper | Early whitepaper (August 2026) — background and vocabulary |
| pick-the-order · recovery-safety-property | An open ordering challenge · a recovery-safety property for durable runtimes |
Scope: the public repositories are separate evidence slices — models, proofs, demos — not a proof of the complete production engine. See CLAIMS_AND_SCOPE.md and SLICES.md.
git clone https://github.com/vasilisnasopoulos/vortex-dse-formal && cd vortex-dse-formal/cslot-proofs/specs
tlapm --toolbox 0 0 Vortex_DSE_CSlot_Proofs.tla
tlapm --toolbox 0 0 Vortex_DSE_CSlot_ExactlyOnce_Proof.tlaFull commands: REPRODUCTION.md.
- CLAIMS_AND_SCOPE.md — canonical claim/evidence/scope matrix for reviewers
- ARCHITECTURE.md — cross-repository system map and CI topology
- PROOF_STRUCTURE.md — proof/model-check dependency flow
- REPRODUCTION.md — canonical local reproduction commands
- SLICES.md — public verification slices and boundaries
- proof-dependencies.json — machine-readable dependency graph
- REPOSITORY_DESCRIPTIONS.md — suggested one-line GitHub descriptions
- RELEASE_NOTES.md — draft
v1.0.0release notes for the public formal baseline - CONTRIBUTING.md — contributor onboarding and review expectations
- README_BLUEPRINTS.md — consistent README section blueprint for all related repos
- These repositories are public formal artifacts; they are not the complete production engine.
- Production C internals, benchmark internals, and some end-to-end composition details remain private.
- Each repository documents assumptions, guarantees, and reproducibility commands for its scope.
formal-methods · tla+ · tlaps · tlc · apalache · distributed-systems · coordination · calm