Paraconsistent federation: an ActivityPub inbox that keeps contradictions instead of last-writer-wins

Paraconsistent federation: an ActivityPub inbox that keeps contradictions instead of last-writer-wins

A conventional ActivityPub server applies each inbound activity as it arrives, so a later Delete erases an earlier Create and two peers that disagree fight until one lands last. The Red Cup ActivityPub provider instead treats every signature-verified inbound activity as a witnessed claim, with polarity "for" or "against" and the activity's id as evidence, and folds claims with the Belnap knowledge join. A thing that one peer created and another deleted is reported as contradicted, with both witnesses, and the result is identical whatever order the activities arrived in. We ran the module to confirm both properties; the output is below.

What is wrong with last-writer-wins in the fediverse?

ActivityPub delivers activities to an inbox asynchronously, from multiple servers, with no global clock. A Delete from a moderator on one server and an Update from the author on another can arrive in either order at a third server. If the third server applies them in arrival order, its state depends on network timing, and two servers that received the same activities in different orders diverge permanently. The usual remedies add timestamps (which are claims by the sender), vector clocks (heavy), or an authority (which is the thing federation avoids).

A different remedy is to stop pretending the inbox is deciding anything. An inbox receives testimony. The testimony may conflict. The honest state of a record that was created by one account and deleted by another is not "deleted" or "exists" but "told both ways, by these two witnesses". That is exactly the fourth value in Belnap's logic, introduced in Reading HTTP in four values, and the same algebra the market sells in Belnap's logic as an API.

How does an activity become a claim?

The ./inbound module of @red-cup-engineering/activitypub-services-section reads an already-verified activity. Signature and proof verification belong to Fedify, before this module sees the activity; the module is described as pure, with no clock and no network. It maps each activity to a subject, a polarity and claims, with the activity's own id as the citation:

An activity that cannot be placed (no subject, an unhandled type) becomes a refused batch with its reason, never a silent drop. At the inbox boundary, receiveInbound returns 400 for a non-ActivityStreams body or an unplaceable activity, and 202 with the observation otherwise, which matches ActivityPub's rule that a successful inbox POST is 202 Accepted with asynchronous processing.

How are claims combined?

settleObservations turns each observation into a cell of subject, predicate and object, with its for and against witness sets, and hands them to the content-addressed cell set of the Group's evidence library, which performs the Belnap knowledge join: duplicate, concurrent and opposite tellings merge by union of witnesses. The module then partitions the cells:

if (witnessed.for.length > 0 && witnessed.against.length > 0) {
  out.contradicted.push({ ...base, affirmedBy: citations(witnessed.for), deniedBy: citations(witnessed.against) });
} else if (witnessed.for.length > 0) {
  out.affirmed.push({ ...base, citation: citations(witnessed.for) });
} else {
  out.denied.push({ ...base, citation: citations(witnessed.against) });
}

(Excerpt from inbound.mjs, abridged.) A claim told only "for" is affirmed; only "against" is denied; both is contradicted with the lists affirmedBy and deniedBy. Nothing is overwritten and nothing is discarded. The module's own comment states the guarantee: the fold "is commutative, associative and idempotent so delivery order cannot matter."

What does a run show?

We ran the module on 2026-10-22 with two activities about one note: a Create by an author at one origin and a Delete by a moderator at another.

const note   = { id: 'https://a.example/notes/1', type: 'Note', content: 'hello' };
const create = { '@context': 'https://www.w3.org/ns/activitystreams', id: 'https://a.example/activities/1',
                 type: 'Create', actor: 'https://a.example/actors/alice', object: note };
const del    = { '@context': 'https://www.w3.org/ns/activitystreams', id: 'https://b.example/activities/9',
                 type: 'Delete', actor: 'https://b.example/actors/mod', object: note };

receiveInbound(create) returned status 202. Settling [create, del] produced two contradicted cells, one for the note's content and one for its type:

{ "affirmed": [], "denied": [],
  "contradicted": [
    { "subject": "https://a.example/notes/1", "predicate": "content", "object": "hello",
      "affirmedBy": ["https://a.example/activities/1"],
      "deniedBy":   ["https://b.example/activities/9"] },
    { "subject": "https://a.example/notes/1", "predicate": "type", "object": "Note",
      "affirmedBy": ["https://a.example/activities/1"],
      "deniedBy":   ["https://b.example/activities/9"] } ] }

We then settled [del, create] in the opposite order and compared the serialized results. They were identical. The output states what each peer told the inbox, preserves both activity ids as evidence, and does not claim to know whether the note "really" exists.

What does the outbox do with a contradiction?

./outbox-projection is the mirror. A subject's settled algebra becomes a Create activity, flagged _contested when any of its cells is contradicted, and the actor's outbox is an OrderedCollection, newest first. A downstream reader sees that the claim is disputed instead of receiving a confident-looking state that depended on a race.

Why would anyone want this?

Three reasons, in increasing order of strangeness.

1. Moderation transparency. If a deletion is a claim with a witness, a server can show "removed by X, contested by Y" rather than hiding the dispute. The decision procedure, whether a human or a policy resolves a contradiction, lives outside the inbox and can be audited against the preserved witnesses.
2. Convergence without coordination. Because the join is commutative, associative and idempotent, two servers that have received the same set of activities hold the same settled state, whatever order or duplication occurred. That is the property conflict-free replicated data types provide, obtained here by reading activities as evidence.
3. A common substrate. The same cell, evidence and join machinery reads HTTP probes, citation checks and federated activities. An agent that knows what contested means in one place knows it in all of them.

What does this not do?

It does not decide anything. A contradicted cell stays contradicted until a policy outside this module acts, and it does not tell you whose claim should win. It does not verify activities, since Fedify does that first. It does not infer truth: the module only reads what was admitted. Its mapping from activity type to polarity is a modeling choice; for example an Update is treated as another affirmative witness, not an overwrite, so a corrected field appears as a second object value for the same predicate and is not merged into one.

How does this relate to the wider transport design?

The provider is the protocol layer of a larger design the Group calls ActivityPub++, a specification draft whose idea is that one actor has one public ActivityPub face, and its activities carry a CloudEvents envelope whose data is an A2A agent message with a single content-addressed CBOR part. The market's own outbox (130 Offer activities whose objects are application/sen+cbor documents named by ni: addresses) is a read-only instance of the same shape (One catalog, five machine faces). That nesting is design-in-progress, not a ratified standard, and we say so.

For how the provider itself is assembled and what is live today, see ActivityPub publication provider.