A MultiPlanetary Exchange System

Inspiration

A message from Earth to Neptune can take hours, and nobody on either end can tell whether a lost reply means "no" or "not yet". Every ordinary exchange assumes a fast, shared clock. We asked what an exchange looks like when that assumption is gone and the brief's nine settlements are light-minutes to light-hours apart.

What it does

We designed an exchange with nine Branches, one per settlement. There is no hub and no central bank.

Home ledger. Each Branch keeps the only ledger for the assets held at its settlement. Every NeoDollar and share sits on exactly one home ledger at all times.
Lock, then commit. Nothing is owed across light-lag unless it is locked first. A cross-planet trade locks the buyer's money at home, and the seller's Branch decides once and commits. The buyer's Branch then releases the funds.
Only the lock holder resends. No timer ends a lock. A lost, late, duplicated or contradictory message therefore delays a deal but cannot lose or double-spend money.
Capped price contracts. A Ceres Iron future locks each side's full maximum loss at home. The Branch where the price is published acts as referee and settles on one signed "settling print".
Time has a price, and we measure it. The 288-hour future keeps 30% of all cash locked. A 72-hour isolation of the referee at maturity makes the remote winner wait longer, and we report the extra dollar-hours. Our worst stacked incident is traced too.

How we built it

Simulator and evidence (Python). We wrote our own event simulator and orbit and latency models, because the data bundle shipped without the reference propagator. The scripts cover the E1–E5 evidence items and the S1–S3 scenarios.
Invariant checks. The three invariants (G1–G3) rest on the rules alone. We check them after every ledger step of 4,500 fault-injected fuzz runs, with 0 violations.
Orbit scan. A 200-year scan certified to 1 ms shows that two Branches can always eventually exchange a packet. That is the only liveness assumption the design needs.
Papers and deck. The design paper and the evidence appendix are written in LaTeX, 12 pages each, with every number generated from the code. The slides are built in Slidev.

Challenges we ran into

None of us comes from a finance background. We had to learn margin, settlement, price runs and so much more
An external evaluation scored the first draft 76/100. We responded with a hardening round, adding resubmit-on-contact, an echo/audit rule, void and griefing-cap rules, and stacked incident scenarios. Each was backed by new tests rather than prose.
Keeping every balance consistent across the paper, the traces and the appendix, inside a hard page limit.

What we learned

Delay is a cost you can price, but lost money cannot be priced. Putting the safety guarantee in the rules, not in timing assumptions, let us prove it by machine check instead of arguing for it. We also learned to separate what is implemented from what is only an extension. For example, detecting a Branch that breaks its own rules is implemented and tested, but enforcing against it is not claimed.