Neologo

A Revised Report on Neologo: A Deterministic Actor/Event Runtime for Executable Coordination

Working draft.

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

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

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

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

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:

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:

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

They are distributed across three federations:

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:

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:

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:

J = submit signed Join
K = keep out

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

Payoff under Neologo:

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:

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

So:

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:

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:

J strictly dominates K.

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

(J, J, J, J, J)

The resulting runtime outcome is:

Finalized(Stag)

Payoffs:

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: 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: same_log(replica_1, replica_2) => same_state(replica_1, replica_2)

Lemma 2: Transactional atomicity

Claim: 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: committed(txn) xor failed(txn)

Lemma 3: Threshold safety

Claim: 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: Finalized(Stag) => count(valid Joined) >= q

Lemma 4: Terminal uniqueness

Claim: 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: not (exists Finalized and exists Aborted)

Lemma 5: Federation safety

Claim: 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: valid_cert(Finalized) => no valid_cert(Aborted)

Lemma 6: Liveness

Claim: 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: eventual_delivery ∧ q_valid_joins ∧ live_home_shard => eventually Finalized(Stag)

Lemma 7: Abort liveness

Claim: 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: deadline_passed ∧ joins.size < q ∧ live_home_shard => eventually Aborted

9. Worked trace

Initial deployment:

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:

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:

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:

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:

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:

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:

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:

• 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:

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

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

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

The runtime guarantees:

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

The mechanism eliminates downside risk:

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

The commit credit eliminates indifference:

Joining strictly dominates staying out.

Therefore:

• 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.