Case study · space traffic coordination · simulated

Who moves? Twenty AI agents wrote the answer in Soma — and the verifier checked it.

When two satellites are about to collide, one of them has to move — exactly one. Today operators settle it by e-mail and phone, case by case; there is no protocol the whole world shares. Orbite is that protocol, written as a program: twenty coding agents built it in a day, in parallel, each seeing only its own part. Its rules of the road are borrowed from the sea, and Soma's verifier proves the ones that keep the decision single. Replayed on a real near-miss from 2019, it settles who moves three days before the closest approach.

Orbite is a research program: States, operators and objects are fictional and nothing connects to a real system. What is real is the question it answers — can agents build a large, safety-critical system that anyone can trust without reading it all?

September 2019, replayed

On 2 September 2019, ESA's satellite Aeolus burned its thrusters to dodge Starlink 44. The risk had climbed to about 1 in 1,000 — ten times ESA's threshold — and ESA could get no answer from SpaceX: an on-call paging bug, SpaceX said later. No rule said who should move. ESA moved alone, without knowing whether the other satellite would move too.

We replayed that timeline on Orbite's real code, not on a model. The first run was honest and disappointing: Orbite decided later than ESA, because it waited for the silent operator until its own take-over deadline. One rule changed — the operator who has to move said yes, the other only stayed silent, so the decision stands — and the replay now looks like this:

The full replay, minute by minute, with what Orbite still does not do →

Rules of the road, borrowed from the sea

Ships have settled "who moves" since 1972 with the international collision regulations, COLREG: every captain knows, without a word exchanged, whether to give way or to stand on. Orbite transposes them to orbit, where the stakes are the same and the ships cannot see each other:

Two rules stay at sea. "Both alter to starboard" (head-on) would mean two manoeuvres without coordination — exactly what property 1 forbids. "The one with the other on its starboard side" has no meaning in orbit. Each rule has a test that applies it and one that does not, in test_colreg.cell.

One decision, proven

The heart of Orbite is a lock. A conjunction gets one lock; the coordination is decided only while the lock is held; the lock is taken only for an agreed coordination and lifted only while it is being reopened. Written as rules on the edges of two state machines, this fits on a screen — and soma verify proves it for every body that will ever be written inside these frames and honour the conditions on their edges, before a single body exists:

// One decision per conjunction. The lock is taken only for an agreed coordination and
// lifted only while that coordination is being released; the coordination is decided
// only while the lock is held, and reopened only once it is lifted.
skeleton Lock {
    memory { holder: Map<String, String> [persistent] }   // conjunction -> object that manoeuvres
    state lock {
        initial: free
        free -> held
        held -> lifted
        lifted -> held
        free -> closed
        held -> closed
        lifted -> closed
    }
    face {
        // Designates `object` for conjunction `c`: only for an agreed coordination.
        signal take(c: String, object: String) -> String
            writes holder
            moves free -> held when Coordination.agreed, lifted -> held when Coordination.agreed
        // Lifts the designation: only while its coordination is being released.
        signal release(c: String) -> String
            writes holder
            moves held -> lifted when Coordination.releasing
        // The conjunction is over: the lock is retired with it, the designation cleared.
        signal retire(c: String) -> String
            writes holder
            moves free -> closed, held -> closed, lifted -> closed
    }
}

skeleton Coordination {
    state coordination {
        initial: open
        open -> agreed
        agreed -> decided
        decided -> releasing
        releasing -> reopened
        reopened -> agreed
        releasing -> closed
        open -> closed
        agreed -> closed
        reopened -> closed
        decided -> closed
    }
    face {
        // Both operators accept the proposed manoeuvre.
        signal agree(c: String) -> String
            moves open -> agreed, reopened -> agreed
        // Takes the decision: only while the lock is held, so only one object ever manoeuvres.
        signal decide(c: String) -> String
            moves agreed -> decided when Lock.held
            calls Lock.take
        // The situation changed (propulsion lost, new data): release, lift the lock, reopen.
        signal reopen(c: String) -> String
            moves decided -> releasing, releasing -> reopened when Lock.lifted
            calls Lock.release
        // The conjunction is over (resolved, passed), decided or not.
        signal close(c: String) -> String
            moves open -> closed, agreed -> closed, reopened -> closed, decided -> closed, releasing -> closed
            calls Lock.retire
    }
}

$ soma verify --summary orbit.cell
17 proven (✓), 11 notes (·) — `soma verify` without --summary prints them
○ 7 holes — signals of a skeleton with no body yet: Lock.take, Lock.release, Lock.retire, Coordination.agree, Coordination.decide, Coordination.reopen, … (1 more)  (`soma holes orbit.cell`)
VERIFY OK (skeleton — the holes above are open obligations)

$ soma verify orbit.cell
Verifying orbit.cell...

State machine 'Lock.lock': 4 states, initial 'free'
  States: [closed, free, held, lifted]

  ✓ 4 states, 6 transitions
  ✓ all states reachable from 'free'
  ✓ terminal states: [closed]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  · think-isolated: judged when the 7 holes of the program have a body
  · termination: 3 holes — judged when they have a body
  · refinement: `take` is a hole — its frame allows {free → held [while ? ∧ if ? ∧ if status_in(?, "Coordination.agreed")], lifted → held [while ? ∧ if ? ∧ if status_in(?, "Coordination.agreed")]}
  · refinement: `release` is a hole — its frame allows {held → lifted [while ? ∧ if ? ∧ if status_in(?, "Coordination.releasing")]}
  · refinement: `retire` is a hole — its frame allows {free → closed, held → closed, lifted → closed}

State machine 'Coordination.coordination': 6 states, initial 'open'
  States: [agreed, closed, decided, open, releasing, reopened]

  ✓ 6 states, 10 transitions
  ✓ all states reachable from 'open'
  ✓ terminal states: [closed]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  · think-isolated: judged when the 7 holes of the program have a body
  · termination: 4 holes — judged when they have a body
  · refinement: `agree` is a hole — its frame allows {open → agreed, reopened → agreed}
  · refinement: `decide` is a hole — its frame allows {agreed → decided [while ? ∧ if ? ∧ if status_in(?, "Lock.held")]}
  · refinement: `reopen` is a hole — its frame allows {decided → releasing, releasing → reopened [while ? ∧ if ? ∧ if status_in(?, "Lock.lifted")]}
  · refinement: `close` is a hole — its frame allows {open → closed, agreed → closed, reopened → closed, decided → closed, releasing → closed}

product:

  ✓ entering Lock.held from free while Coordination.agreed — every run of the handlers, 17 product state(s) explored over Lock.lock (4) × Coordination.coordination (6)
  ✓ entering Lock.held from lifted while Coordination.agreed — every run of the handlers, 17 product state(s) explored over Lock.lock (4) × Coordination.coordination (6)
  ✓ entering Lock.lifted from held while Coordination.releasing — every run of the handlers, 17 product state(s) explored over Lock.lock (4) × Coordination.coordination (6)
  ✓ entering Coordination.decided from agreed while Lock.held — every run of the handlers, 17 product state(s) explored over Lock.lock (4) × Coordination.coordination (6)
  ✓ entering Coordination.reopened from releasing while Lock.lifted — every run of the handlers, 17 product state(s) explored over Lock.lock (4) × Coordination.coordination (6)

15 passed, 0 warnings, 0 failures
note: cross-cell: `Coordination.decide` transitions its own machine and acts on `Lock` — a rule BETWEEN the two cells' machines ("not while the subject is withdrawn") is not verified unless soma.toml states it (`[verify.before."Cell.state"] requires = ["Other.state"]`); enforce it with a `require` reading the other cell
note: cross-cell: `Coordination.reopen` transitions its own machine and acts on `Lock` — a rule BETWEEN the two cells' machines ("not while the subject is withdrawn") is not verified unless soma.toml states it (`[verify.before."Cell.state"] requires = ["Other.state"]`); enforce it with a `require` reading the other cell
note: cross-cell: `Coordination.close` transitions its own machine and acts on `Lock` — a rule BETWEEN the two cells' machines ("not while the subject is withdrawn") is not verified unless soma.toml states it (`[verify.before."Cell.state"] requires = ["Other.state"]`); enforce it with a `require` reading the other cell

  Temporal properties for 'Lock.lock':
  ✓ deadlock_free — no deadlocks in any reachable state

  Temporal properties for 'Coordination.coordination':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 2 passed, 0 failed
note: state machines are verified per cell. A value crosses a cell boundary by a face contract (`requires` / `ensures` on the signal); a rule between two cells' machines is proven when soma.toml states it — `[verify.before."Pay.paid"] requires = ["Approval.signed_off"]` explores the product of the machines.
○ 7 holes — signals of a skeleton with no body yet: Lock.take, Lock.release, Lock.retire, Coordination.agree, Coordination.decide, Coordination.reopen, … (1 more)  (`soma holes orbit.cell`)
VERIFY OK (skeleton — the holes above are open obligations)

The five ✓ entering … lines in the full output are the rules, each proven over every run of the handlers, on the product of both machines. Now add the shortcut someone always wants — an "urgent" decision, force, that takes the edge to decided without the lock:

skeleton Lock {
    state lock {
        initial: free
        free -> held
        held -> free
        held -> closed
    }
    face {
        signal take(c: String) -> String     moves free -> held
        signal release(c: String) -> String  moves held -> free
        signal retire(c: String) -> String   moves held -> closed
    }
}

skeleton Coordination {
    state coordination {
        initial: open
        open -> agreed
        agreed -> decided
        decided -> closed
    }
    face {
        signal agree(c: String) -> String
            moves open -> agreed
        signal decide(c: String) -> String
            moves agreed -> decided when Lock.held
            calls Lock.take
        // An "urgent" shortcut that forgets the lock.
        signal force(c: String) -> String
            moves agreed -> decided
        signal close(c: String) -> String
            moves decided -> closed
            calls Lock.retire
    }
}

$ soma verify --strict --summary shortcut.cell
product:
  ⚠ open obligation — entering Coordination.decided from agreed while Lock.held: a run of the program's handlers enters `decided` without it (from Lock=free, Coordination=agreed) — the bodies written so far respect it; a hole's frame allows this run. Run: Coordination.agree → Coordination.force. It is proven when the holes on the run have bodies that rule it out, or when their frames no longer allow it
--strict failures:
  ⚠ open obligation — entering Coordination.decided from agreed while Lock.held: a run of the program's handlers enters `decided` without it (from Lock=free, Coordination=agreed) — the bodies written so far respect it; a hole's frame allows this run. Run: Coordination.agree → Coordination.force. It is proven when the holes on the run have bodies that rule it out, or when their frames no longer allow it
12 proven (✓), 11 notes (·) — `soma verify` without --summary prints them
○ 7 holes — signals of a skeleton with no body yet: Lock.take, Lock.release, Lock.retire, Coordination.agree, Coordination.decide, Coordination.force, … (1 more)  (`soma holes shortcut.cell`)
VERIFY FAILED — --strict: 1 ⚠ line (runtime-checked or unprovable)

The verifier names the run that breaks the rule — Coordination.agree → Coordination.force — before any code is written. It is an open obligation while force has no body (a body could still refuse the edge); --strict, the mode for CI, fails at once. In Orbite the same rules tie the real lock to the real coordination, in a program of 156 machines. A reviewer found a way to designate twice in an earlier version; the fix is the lifted state above, and their attempt is now a regression test.

How do you trust 69,000 lines no one reviewed?

No model holds 69,000 lines in context, and no human read them all. Soma's answer is to write the structure first, prove it, and then check each body against the part of the structure it belongs to.

That last point is the one agents need: soma skeleton prod.cell CoordVerrou.poser prints everything one body is allowed to touch, and nothing else. An agent writes that body without ever seeing the other 69,000 lines — and cannot quietly reach outside it.

What the verifier — and the replays — caught

The point of a verifier is what it finds before anyone relies on the system. These are real, from the build of Orbite:

Building Orbite also improved Soma itself: the verifier now searches each rule over its own cone of machines, follows the success of a try, accepts a link key a signal makes once, and no longer mistakes two cells' handlers of the same name for a recursion. All of it shipped in Soma 3.2.4.

Six properties, and how each is held

The approval chain behind property 4 is the real frame of ManPlan.approuver (Orbite is written in French):

signal approuver(h: Horodatage, plan: String, par: String) -> ManEtatPlan
    moves crible    -> recoupe   when ConjCriblagePlan.sur,                       // screening still holds
          recoupe   -> coordonne when CoordDossier.arretee  via verrou_de,        // coordination decided
          recoupe   -> habilite  when OpMembres.actif       via proprietaire_de,  // (not an avoidance)
          coordonne -> habilite  when OpMembres.actif       via proprietaire_de,  // operator active
          habilite  -> localise  when EphSuivi.a_jour       via objet_de,         // ephemeris fresh
          localise  -> capable   when RefObjet.en_service   via objet_de,         // object in service
          capable   -> approuve  when ManEvitement.engage   via verrou_de         // the lock is ours

What is not proven — yet

• The 97 rules are proven on the skeleton: they hold for every body that stays in its frame (soma check proves each one does) and takes an edge only under its condition — which soma verify judges on the bodies. Running it on all 1,787 bodies together does not yet finish in reasonable time; that is the next work on the verifier.

• 151 rules through a link (via) stay open obligations until then: each needs the verifier to see, in the body that writes the link, that it is written once.

• Notified is not informed: in the replay, the silent operator receives the decision but never acknowledges it. Orbite reduces the 2019 risk — the other satellite moving too — but cannot remove it.

• Simulated: orbital mechanics are simplified, every actor is fictional. Orbite is a demonstration of method, not a service.

We have not built the same system in another language with the same agents to compare; that experiment is the honest next step, and we will publish its result either way.

Check it yourself in eight minutes

Everything above can be checked with the public release. The whole program is published — 492 files, for people and for agents:

$ curl -fsSL https://soma-lang.dev/install.sh | sh          # soma 3.2.4
$ curl -fsSL https://soma-lang.dev/cases/orbite/orbite.tar.gz | tar xz && cd orbite
$ soma check prod.cell                                       # 0 errors, 1,787 signals, all filled
$ soma verify app.cell                                       # about 8 minutes: VERIFY OK, 97 rules proven
$ soma test test_aeolus.cell                                 # the 2019 replay: 101 assertions