# Neologo: A Deterministic Actor/Event Runtime for Executable Coordination

Neologo can be designed as a deterministic actor/event runtime whose core coordination primitive is a failable conditional transaction; on a threshold Stag Hunt game, it converts unsafe simultaneous coordination into an auditable dominant-strategy commitment protocol under explicit assumptions.

# 1. Design target

Neologo is a language/runtime for this class of systems:

* Many autonomous agents.
* Agents live in different administrative domains.
* Coordination terms are symbolic, not just numeric state.
* Every state transition is event-sourced.
* Every command may fail transactionally.
* Failure is recorded, but failed commands produce no partial side effects.
* Cross-agent coordination is expressed as conditional commitments.
* Federation is handled through signed event certificates and deterministic replay.

# 2. Core language model

## 2.1 Semantic objects

* `Symbol`: globally named coordination object.
* `Actor`: deterministic state machine owning one or more event streams.
* `Command`: requested transition against an actor.
* `Event`: immutable fact appended to an actor stream.
* `State`: projection obtained by folding events.
* `Txn`: atomic bundle of events and outbound messages.
* `Fail`: typed abort with no partial state mutation.
* `Capability`: authority token permitting a command.
* `Certificate`: quorum-signed proof that an event block exists.
* `Intent`: conditional symbolic commitment by an agent.
* `Invariant`: executable safety condition checked before append.

## 2.2 Minimal syntax

```neologo
symbol HuntRound(id: Sym)

type AgentId
type FedId
type Money
type Time

enum Action {
  Hare
  Stag
}

enum Status {
  Pending
  Finalized
  Aborted
}

fail AlreadyClosed
fail DeadlinePassed
fail DuplicateJoin
fail BadSignature
fail BadThreshold
fail Unauthorized
```

# 3. Actor definition

```neologo
actor ThresholdHunt(
  game: HuntRound,
  participants: Set<AgentId>,
  threshold: Nat,
  deadline: Time,
  harePayoff: Money,
  stagPayoff: Money,
  commitCredit: Money
) owns game {

  state {
    status: Status = Pending
    joins: Map<AgentId, Signature> = {}
    outcome: Option<Action> = None
  }

  event Created(
    game: HuntRound,
    participants: Set<AgentId>,
    threshold: Nat,
    deadline: Time
  )

  event Joined(
    game: HuntRound,
    agent: AgentId,
    signature: Signature
  )

  event Finalized(
    game: HuntRound,
    agents: Set<AgentId>,
    action: Action
  )

  event Aborted(
    game: HuntRound,
    reason: Text
  )

  event CommandFailed(
    game: HuntRound,
    commandId: CmdId,
    reason: Fail
  )

  fold Created(e) {
    participants = e.participants
    threshold = e.threshold
    deadline = e.deadline
    status = Pending
  }

  fold Joined(e) {
    joins[e.agent] = e.signature
  }

  fold Finalized(e) {
    status = Finalized
    outcome = Some(e.action)
  }

  fold Aborted(e) {
    status = Aborted
    outcome = Some(Hare)
  }

  command join(agent: AgentId, sig: Signature) txn {
    require agent in participants else fail Unauthorized
    require status == Pending else fail AlreadyClosed
    require now() <= deadline else fail DeadlinePassed
    require not joins.contains(agent) else fail DuplicateJoin
    require verify(agent, hash(game, "JOIN_STAG"), sig) else fail BadSignature

    emit Joined(game, agent, sig)
  }

  command close() txn {
    require status == Pending else fail AlreadyClosed

    if joins.size >= threshold {
      emit Finalized(game, joins.keys, Stag)

      for a in participants {
        send Agent(a).settle(
          game = game,
          action = if a in joins.keys then Stag else Hare,
          basePayoff = if a in joins.keys then stagPayoff else harePayoff,
          commitCredit = if a in joins.keys then commitCredit else 0
        )
      }
    } else {
      emit Aborted(game, "threshold_not_met")

      for a in participants {
        send Agent(a).settle(
          game = game,
          action = Hare,
          basePayoff = harePayoff,
          commitCredit = if a in joins.keys then commitCredit else 0
        )
      }
    }
  }

  invariant no_partial_finalization {
    not (status == Finalized and joins.size < threshold)
  }

  invariant terminal_is_unique {
    count(events where type in {Finalized, Aborted}) <= 1
  }
}
```

# 4. Agent actor

```neologo
actor Agent(id: AgentId) owns id {

  state {
    balance: Money = 0
    settled: Set<HuntRound> = {}
  }

  event Settled(
    game: HuntRound,
    action: Action,
    payoff: Money
  )

  event SettlementRejected(
    game: HuntRound,
    reason: Fail
  )

  command settle(
    game: HuntRound,
    action: Action,
    basePayoff: Money,
    commitCredit: Money
  ) txn {
    require not settled.contains(game) else fail DuplicateJoin

    emit Settled(
      game = game,
      action = action,
      payoff = basePayoff + commitCredit
    )
  }

  fold Settled(e) {
    settled.add(e.game)
    balance += e.payoff
  }
}
```

# 5. Runtime design

## 5.1 Execution pipeline

1. A command enters an actor mailbox.
2. The runtime loads the actor’s current event stream.
3. The actor state is reconstructed by deterministic `fold`.
4. The command handler executes against reconstructed state.
5. The handler returns either `Fail(reason)` or `Txn(events, outbox)`.
6. The runtime checks invariants against the proposed post-state.
7. The runtime appends the event block using optimistic concurrency control.
8. The outbox messages become deliverable only after the event block commits.
9. Failed commands append only `CommandFailed`, or append nothing if the deployment policy treats failure telemetry separately.
10. Replay of the committed log reconstructs the same state everywhere.

## 5.2 Transactional failure rule

```text
eval(command, state) =
  Fail(reason)          => append failure record only; emit no domain events; send no messages
  Txn(events, outbox)   => atomically append events and outbox if invariants hold
```

Critical property:

```text
No externally visible message may leave an actor unless the event block that caused it is committed.
```

This is the outbox rule. It prevents “sent but not committed” divergence.

## 5.3 Federation model

Each federation runs a shard group.

* Every `Symbol` has a home shard: `home(symbol) = hash(symbol) mod federation_map`.
* Every event block is signed by the producing shard group.
* A cross-federation message carries the source event certificate.
* A receiving federation accepts only messages backed by valid certificates.
* Duplicate messages are safe because commands carry deterministic command IDs.
* Reordering is safe because handlers validate current actor state.
* Network partitions delay progress but do not permit conflicting finalization under the quorum assumption.

## 5.4 Required runtime assumptions

* `A1`: Actor handlers are deterministic.
* `A2`: Per-symbol event streams are linearizable.
* `A3`: Quorum certificates cannot be forged.
* `A4`: Honest quorum intersection prevents two conflicting terminal blocks for the same stream.
* `A5`: Messages between non-faulty federations are eventually delivered.
* `A6`: Agents cannot forge another agent’s signature.
* `A7`: Deadlines are interpreted by the home shard clock or by a certified logical clock.

# 6. Non-trivial coordination problem

## Federated threshold Stag Hunt

There are five agents:

```text
N = {A, B, C, D, E}
```

They are distributed across three federations:

```text
Fed α: A, B
Fed β: C
Fed γ: D, E
```

Each agent chooses whether to join a high-value collective action.

Underlying game:

* `Hare`: safe fallback.
* `Stag`: high payoff, but only succeeds if enough agents choose it.
* Threshold: `q = 4`.
* Hare payoff: `H = 2`.
* Stag payoff: `S = 6`.
* Failed Stag payoff without protocol: `0`.
* Commit credit: `r = 0.1`.

Underlying simultaneous Stag Hunt payoff:

```text
u_i(Stag) = 6 if at least 4 agents choose Stag
u_i(Stag) = 0 if fewer than 4 agents choose Stag
u_i(Hare) = 2
```

This has the familiar coordination-risk structure:

* Everyone choosing `Hare` is stable.
* Everyone choosing `Stag` is better but risky.
* A rational agent may avoid `Stag` if unsure about others.

Neologo mechanism:

```text
Agents do not directly choose Stag.
Agents issue signed conditional Join events.
The runtime finalizes Stag only if at least 4 valid joins exist by deadline.
Otherwise it aborts and assigns Hare.
Joiners receive a small symbolic/audit credit r for making a verifiable cooperative commitment.
```

# 7. Game-theoretic proof

## 7.1 Mechanism action space

Each agent chooses:

```text
J = submit signed Join
K = keep out
```

Let `k_-i` be the number of other agents who choose `J`.

Payoff under Neologo:

```text
u_i(J) = S + r if k_-i >= q - 1
u_i(J) = H + r if k_-i < q - 1

u_i(K) = H
```

With values:

```text
S = 6
H = 2
r = 0.1
q = 4
```

So:

```text
u_i(J) = 6.1 if at least 3 other agents join
u_i(J) = 2.1 otherwise

u_i(K) = 2
```

## 7.2 Dominance result

For every agent `i`:

```text
if k_-i >= 3:
  u_i(J) = 6.1 > 2 = u_i(K)

if k_-i < 3:
  u_i(J) = 2.1 > 2 = u_i(K)
```

Therefore:

```text
J strictly dominates K.
```

Since this holds for every agent, the unique dominant-strategy equilibrium is:

```text
(J, J, J, J, J)
```

The resulting runtime outcome is:

```text
Finalized(Stag)
```

Payoffs:

```text
A = 6.1
B = 6.1
C = 6.1
D = 6.1
E = 6.1
```

[INFERENCE] The `commitCredit` can represent reputation, audit credit, future-priority credit, or a small escrow-funded reward. If `r = 0`, joining weakly dominates abstention, but all-abstain remains a weak Nash equilibrium because failed coordination and abstention both pay `H = 2`.

## 7.3 Mechanism lineage

This construction is not original to Neologo. Refund-if-threshold-fails contracts fully implementing the core are due to Bagnoli and Lipman (1989); the refund *bonus* that upgrades weak to strict dominance — exactly the `commitCredit r` above — is Tabarrok's dominant assurance contract (1998). Kickstarter deployed the r = 0 variant at planetary scale with no cryptography and no federation. Neologo's contribution is not the mechanism; it is making such mechanisms *programmable, auditable, and composable* as first-class runtime objects: schemas anyone can write, event logs anyone can replay, invariants the runtime enforces rather than a platform brand.

* Bagnoli, M., Lipman, B. (1989). "Provision of Public Goods: Fully Implementing the Core through Private Contributions." *Review of Economic Studies* 56(4).
* Tabarrok, A. (1998). "The private provision of public goods via dominant assurance contracts." *Public Choice* 96.

## 7.4 Scope of the payoff assumption

The dominance proof assumes the runtime can credibly deliver `S + r`, `H + r`, and `H`. That assumption holds unconditionally only when payoffs are *runtime-internal* — credits, priority, compute budget, capability grants inside the same system. When payoffs are external (money, legal obligation, physical delivery), settlement requires escrow, oracles, or legal enforcement, and the mechanism inherits their trust assumptions; the runtime then guarantees the *bookkeeping* of the commitment, not the payment itself. This is why the nearest-term domain for Neologo is coordination among software agents, whose incentives are already denominated in runtime-internal quantities. The proof also treats joining as costless; where commitment locks capital or forecloses outside options during the round, `r` must exceed that carrying cost for strict dominance to survive.

# 8. Runtime correctness proof

## Lemma 1: Replay determinism

Claim:

```text
For any actor stream L, every correct replica computes the same state fold(L).
```

Proof:

* Actor state is defined only as the fold of committed events.
* `fold` functions are deterministic.
* Event order inside a stream is linear.
* Therefore equal logs imply equal states.

Result:

```text
same_log(replica_1, replica_2) => same_state(replica_1, replica_2)
```

## Lemma 2: Transactional atomicity

Claim:

```text
A command produces either all declared events and outbox messages, or no domain-visible effects.
```

Proof:

* A handler returns either `Fail` or `Txn`.
* `Fail` emits no domain event and no outbox message.
* `Txn` is appended as one event block.
* Outbox entries are released only after block commit.
* Therefore no partial domain mutation is externally visible.

Result:

```text
committed(txn) xor failed(txn)
```

## Lemma 3: Threshold safety

Claim:

```text
Finalized(Stag) cannot occur unless at least q valid joins were committed first.
```

Proof:

* The only command that emits `Finalized(Stag)` is `close`.
* `close` emits `Finalized(Stag)` only if `joins.size >= threshold`.
* `joins` is derived only from committed `Joined` events.
* `Joined` requires participant membership, non-duplication, deadline validity, and signature validity.
* The invariant `no_partial_finalization` rejects any proposed post-state violating the threshold.
* Therefore a committed `Finalized(Stag)` implies at least `q` valid committed joins.

Result:

```text
Finalized(Stag) => count(valid Joined) >= q
```

## Lemma 4: Terminal uniqueness

Claim:

```text
A hunt round cannot both finalize and abort.
```

Proof:

* Both `Finalized` and `Aborted` set `status` to terminal.
* `close` requires `status == Pending`.
* The event stream is linearizable.
* The invariant `terminal_is_unique` rejects a second terminal event.
* Therefore only one terminal event can commit.

Result:

```text
not (exists Finalized and exists Aborted)
```

## Lemma 5: Federation safety

Claim:

```text
Two federations cannot validly observe conflicting terminal outcomes for the same hunt round.
```

Proof:

* The hunt round is owned by one symbolic stream: `home(game)`.
* Terminal events are appended only to that stream.
* The stream is linearizable under assumption `A2`.
* Terminal blocks require quorum certificates.
* Conflicting certified terminal blocks would require quorum conflict or signature forgery.
* Assumptions `A3` and `A4` exclude that.
* Therefore all valid observers eventually accept the same terminal event.

Result:

```text
valid_cert(Finalized) => no valid_cert(Aborted)
```

## Lemma 6: Liveness

Claim:

```text
If at least q valid joins arrive before deadline and the home shard remains live, the round eventually finalizes.
```

Proof:

* Eventual delivery ensures valid joins reach the home shard.
* Each valid join appends a `Joined` event.
* Once `joins.size >= q`, `close` satisfies the finalization guard.
* A live home shard eventually processes `close`.
* Therefore `Finalized(Stag)` eventually commits.

Result:

```text
eventual_delivery ∧ q_valid_joins ∧ live_home_shard => eventually Finalized(Stag)
```

## Lemma 7: Abort liveness

Claim:

```text
If fewer than q valid joins exist after deadline, the round eventually aborts.
```

Proof:

* After deadline, no further valid `join` can commit.
* `close` observes `joins.size < q`.
* The only enabled terminal transition is `Aborted`.
* A live home shard eventually processes `close`.
* Therefore `Aborted(threshold_not_met)` commits.

Result:

```text
deadline_passed ∧ joins.size < q ∧ live_home_shard => eventually Aborted
```

# 9. Worked trace

Initial deployment:

```neologo
spawn ThresholdHunt(
  game = HuntRound("hunt-17"),
  participants = {A, B, C, D, E},
  threshold = 4,
  deadline = T,
  harePayoff = 2,
  stagPayoff = 6,
  commitCredit = 0.1
)
```

Observed federated command sequence:

```text
1. A@Fedα submits Join.
2. B@Fedα submits Join.
3. B retries the same Join because of a network timeout.
4. C@Fedβ submits Join.
5. D@Fedγ submits Join after a temporary partition heals.
6. E@Fedγ submits no Join.
7. The close command executes before terminal state exists.
```

Committed event stream:

```text
0 Created(hunt-17, {A,B,C,D,E}, q=4, deadline=T)
1 Joined(hunt-17, A, sigA)
2 Joined(hunt-17, B, sigB)
3 CommandFailed(hunt-17, retryB, DuplicateJoin)
4 Joined(hunt-17, C, sigC)
5 Joined(hunt-17, D, sigD)
6 Finalized(hunt-17, {A,B,C,D}, Stag)
```

Settlement events:

```text
A Settled(hunt-17, Stag, 6.1)
B Settled(hunt-17, Stag, 6.1)
C Settled(hunt-17, Stag, 6.1)
D Settled(hunt-17, Stag, 6.1)
E Settled(hunt-17, Hare, 2.0)
```

Counterfactual for `E`:

```text
If E had joined, E would receive 6.1 instead of 2.0.
```

Therefore `E` skipping is not a best response once three or more others join.

Under the full mechanism with `r > 0`, `Join` is strictly better even when the threshold fails:

```text
Join and fail: 2.1
Skip:          2.0
```

So all agents joining is the unique dominant-strategy equilibrium.

# 10. Failure cases handled

| Failure                  |         Runtime behavior | Safety result               |
| ------------------------ | -----------------------: | --------------------------- |
| Duplicate join           |  `DuplicateJoin` failure | No double-counting          |
| Late join                | `DeadlinePassed` failure | Deadline integrity          |
| Bad signature            |   `BadSignature` failure | No forged participation     |
| Network retry            |    Idempotent command ID | At-most-once effect         |
| Partition                |         Delayed delivery | No conflicting finalization |
| Concurrent close         | Linearized stream append | One terminal outcome        |
| Partial settlement crash |            Outbox replay | Eventually delivered once   |
| Receiver crash           |       Agent event replay | Settlement not lost         |

# 11. Why this is actor-based

* Each participant is an `Agent` actor.
* Each game round is a `ThresholdHunt` actor.
* Each actor owns its own event stream.
* Actors communicate only by certified messages.
* No actor directly mutates another actor’s state.
* Coordination is achieved by symbolic event exchange, not shared memory.

# 12. Why this is event-sourced

* `joins` is not stored as authoritative mutable state.
* `joins` is reconstructed from `Joined` events.
* `status` is reconstructed from `Created`, `Finalized`, and `Aborted`.
* Recovery is replay.
* Audit is replay.
* Federation verification is event-certificate verification.

# 13. Why this is transactionally failable

The following command does not partially mutate the game:

```neologo
command join(agent, sig) txn {
  require status == Pending else fail AlreadyClosed
  require now() <= deadline else fail DeadlinePassed
  require not joins.contains(agent) else fail DuplicateJoin
  emit Joined(game, agent, sig)
}
```

If any guard fails:

```text
No Joined event is emitted.
No outbox message is released.
No threshold count changes.
The failure is typed and auditable.
```

# 14. Why this solves the coordination problem

The original game has coordination risk:

```text
Choosing Stag alone can yield 0.
Choosing Hare always yields 2.
```

Neologo changes the move from direct risky action to conditional symbolic commitment:

```text
“I will play Stag if enough others also commit.”
```

The runtime guarantees:

```text
If enough commitments exist: finalize Stag.
If not enough commitments exist: abort to Hare.
```

The mechanism eliminates downside risk:

```text
A joiner never receives the failed-Stag payoff of 0.
```

The commit credit eliminates indifference:

```text
Joining strictly dominates staying out.
```

Therefore:

```text
The unique dominant-strategy equilibrium is universal Join.
Universal Join causes Finalized(Stag).
Finalized(Stag) gives every participant the high cooperative payoff.
```

# 15. Compact theorem

## Theorem

For the five-agent, three-federation threshold Stag Hunt with `q = 4`, `H = 2`, `S = 6`, and `r > 0`, Neologo’s conditional event-sourced transaction protocol implements `Stag` as the unique dominant-strategy equilibrium outcome, assuming deterministic actors, linearizable per-symbol streams, unforgeable signatures, quorum-intersecting certificates, and eventual delivery.

## Proof

* By Lemma 3, `Stag` finalizes only after at least four valid joins.
* By Lemma 4, the round cannot both finalize and abort.
* By Lemma 5, federations cannot certify conflicting terminal outcomes.
* By Lemma 6, four or more valid joins eventually finalize.
* By Lemma 7, fewer than four valid joins eventually abort to Hare.
* For each agent, `Join` yields either `S + r` or `H + r`.
* `Skip` yields `H`.
* Since `S > H` and `r > 0`, `Join` strictly dominates `Skip`.
* Therefore every rational agent joins.
* With all five joining, the threshold condition is satisfied.
* Therefore the runtime commits `Finalized(Stag)`.
* Therefore the mechanism implements the cooperative equilibrium and removes the unsafe all-Hare equilibrium from the dominant-strategy solution.

QED.