Harness Architecture

1 Introduction

An agent harness is what remains of an agent system when the language model is removed. It holds the prompts, the tool surface, the memory, the wiring between stages, the policy that admits or refuses an action, and the machinery that decides which model or process runs where. Recent surveys treat this layer as a subject in its own right and enumerate its components (9, 19). An industry account states the division of labour in the same terms: the model holds the capability and the harness is the system that makes it useful (16). Enumeration is not composition. A list of six components does not say what happens when two harnesses are installed side by side, which properties of a harness survive translation into a different runtime, or what it would mean to check that they do.

Banu (2) argues that a formal answer already exists. The ArchAgents programme of de los Riscos, Corbacho and Arbib (4) models an architecture as a triple $(G, \mathrm{Know}, \Phi)$. The syntactic wiring $G$ is a graph of modules, ports and directed edges. The knowledge structure $\mathrm{Know}$ holds invariants and certificates. The deployment map $\Phi$ assigns concrete implementations to abstract capability slots. Morphisms are structure-preserving translations, which in practice are compilers. Banu maps Zhou et al.’s four externalization pillars onto this triple: Memory as coalgebraic state, Skills as operad-composed objects, Protocols as the wiring $G$, and Harness as the full triple. He validates the mapping with five compiler functors and a reference implementation of his own.

This Part takes the fourth row of that table seriously and asks whether a harness built independently of that programme instantiates it. The system is AgentHero, a control plane written in Rust with a JavaScript harness runtime, at commit 1c3ad24. It was not built from Banu’s paper: none of the reference implementation’s identifiers occurs anywhere in it (Section 8). If the triple is a real description of harnesses rather than a description of one harness, the structure should be recoverable anyway.

1.1 Scope

What we claim is narrower than the correspondence taken at face value, and we state it in full before anything is proved. We do not claim that the four externalization pillars and the Architecture triple $(G, \mathrm{Know}, \Phi)$ are the same thing. We claim three things, under assumptions stated at the point where each is used. There is a structure-preserving interpretation of the four pillars in $(G, \mathrm{Know}, \Phi)$. Each of the three systems examined in this series realises that interpretation on an identifiable fragment, which for the harness is the fragment delimited law by law in Section 6. The interpretation fails at identifiable points, of which this Part exhibits several in Section 8. Memory, Skills, Protocols and Harness is the order in which the series presents the pillars, not an order of logical dependency, and where a dependency runs against it we say so (Section 1.3).

For the Harness pillar this specializes to three questions. Does the harness runtime carry all three components of the triple, in separable form? On which fragment can an interpretation $\mathbf{Arch}\to \mathbf{Sys}$ be stated and checked to be lax monoidal? And what can “certificate preservation” mean for a harness whose certificates are receipts and fence tokens rather than triples of theorem, parameter map and replayable derivation?

The last of the three is where the counterexample lives, and its short answer governs the whole Part. Banu’s Definition 1 asks a certificate to carry a theorem statement $\tau$, a symbol-to-parameter map $\sigma$, and evidence $\mathit{evds}$ that can be mechanically replayed. The harness studied here carries schema strings, identity keys and retained receipt bodies. There is no theorem. Preservation therefore cannot mean that a theorem survives translation. It can only mean that a decidable check keeps accepting the same transported witnesses. Our name for that is replay stability, defined precisely in Definition 3.30, and it is never called verification here. Every statement about the running system below is an implementation-level claim established by reading the source at the pinned commit, of the form “the implementation at commit 1c3ad24 performs $Y$”. No claim in this paper rests on an observed run, and Definition 3.24 is built so that the interpretation into systems has no way to depend on one.

1.2 Contributions

1. A definition of the category $\mathbf{Arch}$ of Architecture triples (Definitions 3.3, 3.8 and 3.9), in which a certificate carries a scope in the wiring and a decidable replay check. The deployment map is a parameter rather than preserved data, following Banu’s Definition 2. $\mathbf{Arch}$ is shown to be a category (Proposition 3.10) and symmetric monoidal under disjoint union of wirings (Proposition 3.18).

2. A target category $\mathbf{Sys}$ (Definition 3.24) whose objects carry a sequencing relation rather than fence values, so that a functor into it is defined by a schema and never by a trace (Remark 3.23). An interpretation is then a lax monoidal functor (Definition 3.29).

3. A precise statement of the cost of treating the deployment map as a free parameter. On deployment-independent checks, forgetting $\Phi$ is an equivalence of categories (Proposition 3.11), so no functorial guarantee about deployment can be derived in $\mathbf{Arch}$. The deployment-preserving refinement $\mathbf{Arch}^\Phi$ (Definition 3.13) is a genuinely different category, and the deployment-changing counterexample used by the separation theorem is not a morphism in it.

4. A separation theorem for certificate preservation (Theorem 3.32): a certificate whose check factors through $(G, \mathrm{Know})$ is replay-stable under every architecture morphism, while a certificate whose check reads $\Phi$ need not be. Both kinds occur in AgentHero, and we name them.

5. A proof that certificate-wise preservation does not imply preservation of the derived fail-closed admission predicate (Proposition 3.34), which is antitone in $\mathrm{Know}$. This is a gap in the operational reading of certificate preservation, not in the underlying proposition.

6. A laxness result (Theorem 6.3) locating the failure of strength in one concrete artifact. The harness draws every durability fence from a single database sequence, so the comparison map is a bijection that has no inverse in $\mathbf{Sys}$. On the hook delivery fragment, whose fence tokens are per row, the receipt-sequencing abstraction is strong (Proposition 6.7). It does not model which certificate-event pairs are eligible, so it answers the fragment question only for fence allocation.

7. An admissibility result for the monoidal product (Proposition 3.21): the registry’s refusal to install two applications claiming the same stage name is exactly the side condition that makes $\otimes$ well-defined on globally named architectures.

8. Seven laws for harness realizations (Section 4) and their status against the source at the pinned commit (Section 6), with five satisfied, one partial and one violated, together with a code evidence table (Appendix A).

1.3 Series context

This Part is the last of four and has the heaviest import list. It cites the sibling Parts rather than restating them.

From Part I (10) it imports the memory coalgebra $(S, \alpha \colon S \to F S)$ and the narrowing that ContextFS’s lineage is single-axis rather than bitemporal. Part I’s result is used here only to keep $\mathrm{Know}$ and $S$ apart: a schema registry or a validated manifest is a certificate, a stored memory record is not.

From Part II (11) it imports the coloured skills operad $\mathcal{O}$, the reading of a validated DAG manifest as a formal composite, and the statement that AgentHero’s ports are string-keyed rather than drawn from a closed colour set. This Part does not re-derive the operad reading of a manifest; it uses the manifest as the wiring of one installed application and adds only the registry-level composition across applications.

From Part III (12) it imports the port-type alphabet, the wiring operad $\mathcal{W}$, the sub-operad of tree wirings, and the statement that $\mathcal{W}$ and $\mathcal{O}$ are distinct operads with different concrete colour sets, related in one direction by type erasure. This Part defines no wiring of its own. Where it needs a harness-level wiring it takes a general wiring in Part III’s operad $\mathcal{W}_\mathsf{T}$ whose inner boxes are the stages of an installed application manifest. Such wirings are not tree wirings, for the reason given in Remark 3.2.

Two dependencies run backwards relative to presentation order and are stated as such. Part II cites this Part for the notion of a certificate, because AgentHero attaches a policy envelope to individual operations and that envelope is $\mathrm{Know}$-level. The stage-indexed presentation of $\mathrm{Know}$ in Remark 3.5 exists so that Part II can cite it. Part III cites this Part for the same reason, when arguing that CatDB’s policy decisions and field provenance records are certificate-shaped without being separately addressable. Nothing in Parts I to III depends on any theorem proved here.

The results this Part supplies to the synthesis are Theorems 3.32, 6.3 and 6.5, together with the observation that the harness’s certificates are receipt-shaped. The synthesis needs the laxness result to weigh whether treating an agent as a lax monoidal functor adds anything to a purely economic account of why externalization happens.

2 Background

2.1 The harness pillar

Zhou et al. (19) organize the externalization of agent capability into four pillars: memory, skills, protocols, and harness engineering. The first three name things that are moved out of the model’s weights and into addressable structure. The fourth names the structure that holds the other three. Meng et al. (9) give an enumerative account of the same layer, decomposing a harness into environment, tools, context, security, learning and evaluation components. Pan et al. (18) study harnesses whose interfaces are natural language rather than typed calls and observe that harnesses behave as portable objects that can be moved between models.

Enumerations of this kind answer the question of what is in a harness. They do not answer the question of what a harness is, in the sense that would let one say when two harnesses are the same. Nor do they say what happens when two are composed, or which of their properties survive being recompiled onto a different runtime. Banu’s contribution (2) is to propose that these questions have standard answers once a harness is presented as an Architecture triple.

2.2 The Architecture triple

Banu’s presentation of the ArchAgents triple, which he takes by citation from de los Riscos, Corbacho and Arbib (4), runs as follows. An architecture is $\mathcal{A} = (G_\mathcal{A}, \mathrm{Know}_\mathcal{A}, \Phi_\mathcal{A})$. Here $G_\mathcal{A}$ is syntactic wiring given as a graph of modules, ports and directed edges, and $\mathrm{Know}_\mathcal{A}$ is a knowledge structure holding structural properties, invariants and certificates. The third component $\Phi_\mathcal{A}$ is a deployment map from abstract capability slots to concrete model or tool implementations. A morphism $f \colon \mathcal{A} \to \mathcal{B}$ is a structure-preserving translation, which Banu reads operationally as a compiler.

Two of Banu’s definitions are used here directly.

Definition 1 (Structural Guarantee as Certificate). A certificate is a triple $(\tau, \sigma, \mathit{evds})$ where $\tau$ is a theorem statement, $\sigma$ maps theorem symbols to architecture parameters, and $\mathit{evds}$ is a derivation that can be mechanically replayed to verify $\tau$ holds.

Definition 2 (Deployment Map). $\Phi \colon \mathit{Stages} \to \mathit{Models}$ assigns each stage a model tier. This map is a parameter of the architecture, not a fixed constant; different deployments can use different $\Phi$ while preserving the same $(G, \mathrm{Know})$.

The second definition has a consequence that shapes everything below. If $\Phi$ is a parameter, a morphism of architectures cannot be required to preserve it. Banu’s own compiler checks reflect this: of his three checks, graph preservation and certificate replay are equalities, while deployment-map preservation asks only that source stage names appear in the target, with mode mapping allowed to differ. We build that asymmetry into Definition 3.9 and then show in Theorem 3.32 that it has a cost, because some checks a real harness performs read $\Phi$.

On certificate preservation Banu is explicit that he is using an imported result rather than proving one:

ArchAgents state certificate preservation as Proposition 5.1. In this paper we use the result operationally, not as a new proof: a compiler that claims preservation must carry each source certificate’s theorem, parameters, and replayable evidence into the target $\mathrm{Know}$ structure. Functor laws alone are not sufficient for that claim, so our compiler checks certificate identity and verifier replay explicitly.

The same discipline is followed here, with one further step. The harness studied below has no theorem field, so $\mathit{evds}$ is replaced by an explicit pair of a witness and a decidable checker, and preservation is defined as stability of the checker under transport. This is weaker than Banu’s reading and strictly weaker than verification. It is also checkable by reading source, which the stronger readings are not.

2.3 Monoidal structure

The definitions are standard (8). A monoidal category is a category $\mathcal{C}$ with a functor $\otimes \colon \mathcal{C} \times \mathcal{C} \to \mathcal{C}$, a unit object $I$, and natural isomorphisms $a_{X,Y,Z} \colon (X \otimes Y) \otimes Z \to X \otimes (Y \otimes Z)$, $\lambda_X \colon I \otimes X \to X$ and $\rho_X \colon X \otimes I \to X$ satisfying the pentagon and triangle coherence conditions. It is symmetric when it further carries $s_{X,Y} \colon X \otimes Y \to Y \otimes X$ with $s_{Y,X} s_{X,Y} = \mathrm{id}$, compatible with $a$ and $\lambda$.

A lax monoidal functor $(A, \mu, \eta) \colon (\mathcal{C}, \otimes, I) \to (\mathcal{D}, \boxtimes, J)$ is a functor $A$ together with a natural transformation $\mu_{X,Y} \colon A X \boxtimes A Y \to A(X \otimes Y)$ and a morphism $\eta \colon J \to A I$. The associativity and unit diagrams commute: $$\begin{array}{ccc} (AX \boxtimes AY) \boxtimes AZ & \xrightarrow{\scriptstyle a^{\mathcal{D}}} & AX \boxtimes (AY \boxtimes AZ) \\[6pt] \big\downarrow{\scriptstyle \mu \boxtimes \mathrm{id}} & & {\scriptstyle \mathrm{id}\boxtimes \mu}\big\downarrow \\[6pt] A(X \otimes Y) \boxtimes AZ & & AX \boxtimes A(Y \otimes Z) \\[6pt] \big\downarrow{\scriptstyle \mu} & & {\scriptstyle \mu}\big\downarrow \\[6pt] A((X \otimes Y) \otimes Z) & \xrightarrow[\scriptstyle A a^{\mathcal{C}}]{} & A(X \otimes (Y \otimes Z)) \end{array}$$ The functor is strong when every $\mu_{X,Y}$ and $\eta$ is an isomorphism, and strict when they are identities. The distinction is the entire content of Theorem 6.3: laxness is not a technicality here but a statement that two applications installed in one harness cannot be separated again.

For the operadic and coalgebraic vocabulary the series uses elsewhere we cite the standard sources rather than restating them. The sources for Part III are Spivak’s operad of wiring diagrams (15) with its directed (13) and open-dynamical-system refinements (17). Fong and Spivak (5) give the general compositional vocabulary, and Rutten (14) and Jacobs (6) Part I’s coalgebras.

3 The formal model

Throughout, $\mathsf{T}$ is a fixed port-type alphabet in the sense of Part III. The set $R$ is a fixed nonempty set of deployment records. A record identifies the concrete realizer of a stage—a model endpoint, adapter process, or plugin binary—and any authorized workspace or artifact-store roots available to that stage.

3.1 Harness wirings

Part III owns the definition of typed ports, boxes and the wiring operad $\mathcal{W}_\mathsf{T}$, together with its sub-operad of tree wirings. This Part does not redefine any of them. It needs only a name for the particular wirings that occur at the harness level.

Two further things are deliberately not claimed. Definition 3.1 does not claim that Part III’s alphabet $\mathsf{T}$ and AgentHero’s string-keyed port names are the same alphabet. Part III’s type-erasure result gives the obstruction, and we return to it in Section 7. It does not claim that $G$ determines an operadic composite. Part II shows that one operadic operation requires an additional rooted output and unique supplier map, and that a multi-output invocation is split into coordinate generators. A PROP preserves the invocation as one operation. Where the results below need $G$ they need only its stage set and its edges, never the composite, so this narrowing does not propagate into them.

3.2 Certificates

Definition 3.3 is Banu’s Definition 1 with two changes, both forced by what implementations carry. The evidence component $\mathit{evds}$ is split into a witness, which is data an implementation retains, and a checker, which is code an implementation runs. Banu’s phrase “a derivation that can be mechanically replayed” is exactly that pair. A scope is also added. Banu’s certificates are architecture-wide. Real harnesses attach policy to individual stages as well as to the whole system, and the scope records which.

A receipt-shaped certificate says that a named party produced a well-formed record with the expected identity, and nothing else. It carries no theorem. The following makes “and nothing else” precise rather than leaving it as an admission.

Proposition 3.7 is the exact sense in which the harness’s knowledge layer is knowledge-free. It detects identity and shape and is blind to content by construction, so any claim of the form “this certificate rules out behaviour $B$” is unavailable unless $B$ is a statement about identity or shape. Section 8 records that every certificate found in the harness is receipt-shaped, and this proposition says what that costs.

3.3 Architectures and their morphisms

3.4 The monoidal product

A real harness does not tag its stage names. It installs applications into one namespace and refuses collisions. That gives a partial version of $\otimes$ which is what the implementation realizes.

Section 6 identifies the implementation of this decision procedure and shows that it is exactly the check the registry performs before admitting a pair of installed applications.

3.5 Systems

The target category must be concrete enough that its objects correspond to something a harness declares, and abstract enough that a functor into it can be defined without appeal to observed runs. The second requirement rules out the obvious choice of carrying fence values directly. A fence value may be allocated before the guarded write commits. The actual fence carried by an actual receipt is therefore a fact about a run, and cannot appear in the image of a functor defined on architectures. What a store design does fix, statically and readably from its schema, is which receipts are drawn from a common monotone sequence. That is the invariant $\mathbf{Sys}$ records.

The receipt component of Definition 3.24 is a standard structure under a different name.

3.6 Interpretations

Banu describes an agent as a monoidal functor interpreting an architecture in a concrete system. Definition 3.29 makes the laxness explicit and, by Definition 3.29’s relativization to a subcategory, makes room for one abstraction to be strong on a fragment and another to be lax. Section 6 exhibits both receipt- sequencing cases in AgentHero; it does not construct a single operational interpretation covering both.

3.7 Replay stability

Replay stability strengthens (M4) from an implication to an equivalence. It is the formal content of “certificate preservation” here: the check neither loosens nor tightens under translation. It is not verification. A replay-stable certificate whose check is trivially true is replay-stable and says nothing.

The relation between the two conditions is exact, and it is not a change of subject.

So the object of study is not an ad-hoc predicate attached to a category with the wrong morphisms. It is the wide subcategory $\mathbf{Arch}^{=} \subseteq \mathbf{Arch}$, and the question “which certificates are preserved” is the question “which architectures have the property that every morphism out of them lands in $\mathbf{Arch}^{=}$”. Theorem 3.32 answers it.

We now isolate the property that decides replay stability. Say that a check $\mathrm{chk}_c$ factors through $(G, \mathrm{Know})$ when there is a function $k$ such that $\mathrm{chk}_c(\Phi,w) = k(\tau_c, \sigma_c, \mathrm{scope}(c), w)$ for every $\Phi$, that is, when the check reads only the certificate’s own data and the witness. Say that it reads $\Phi$ when its value depends on $\Phi_\mathcal{A}$ with the other arguments held fixed.

4 Harness laws

The definitions above are satisfied by many things, including useless ones. The following seven laws state what a realization must additionally do for the interpretation to carry weight. They are stated so that each can be settled by reading source at a fixed commit. Section 6 settles them for AgentHero.

Law 6 is the one that Theorem 3.32 shows to be load-bearing: a realization that violates it has certificates that do not survive redeployment. Law 4 and Proposition 3.34 pull in opposite directions, and a realization that satisfies Law 4 is thereby one whose admission predicate is not preserved by $\mathrm{Know}$-extending morphisms. That tension is real. We record it rather than resolving it.

5 The system

Table 1 pairs each model object with an identifier in the source. Every system claim below comes from source inspection at commit 1c3ad24. Two schema facts in Sections 6.8 and 6.9 discharge the hypotheses of Theorem 6.3 and Proposition 6.7.

AgentHero is a control plane for installed applications. Its repository documentation states the product boundary directly: the platform owns the Rust control plane, application discovery, executor contracts, runtime state, worker scheduling and process adapter dispatch. Product behaviour lives behind per-application manifests (CLAUDE.md, “Product Boundary”, commit 1c3ad24). That is a description of a harness in the sense of Section 2.1: it is what is left when the applications and the models are removed.

5.1 Model-to-source mapping

5.2 The knowledge layer

The certificate layer is the hook system. A hook is an installed plugin subscribed to canonical lifecycle events, and it has exactly two phases.

Listing 1. crates/orchestrator/src/hooks.rs lines 36-44, attributes omitted; commit 1c3ad24.

/// Hook execution phase.
pub enum HookPhase {
    /// Deterministic admission policy evaluated before canonical mutation.
    PrePolicy,
    /// Side-effect-capable handler evaluated after a canonical event commits.
    PostCommit,
}

The doc comments name the two roles the model needs. A PrePolicy hook is a certificate whose check gates a mutation; a PostCommit hook is a certificate whose witness is produced after the fact and retained. The repository’s own prose says the same: “Pre-policy hooks are synchronous and fail closed before a mutation. Post-commit hooks are created transactionally from PostgreSQL events and use durable attempts, leases, fencing, idempotency, and retained receipts” (README.md, lines 39 to 43).

A subscription also carries a failure policy, which is the certificate’s declared behaviour when its check does not pass.

Listing 2. crates/orchestrator/src/hooks.rs lines 57-66, attributes omitted; commit 1c3ad24.

pub enum HookFailurePolicy {
    /// Deny the synchronous operation.
    Deny,
    /// Retry post-commit delivery with the persisted attempt policy.
    Retry,
    /// Retain the failed receipt without blocking canonical runtime progress.
    Continue,
}

The witness is a receipt, and it is closed: the type is declared with serde(deny_unknown_fields), so a plugin cannot smuggle additional structure past the boundary.

Listing 3. crates/orchestrator/src/hooks.rs lines 427-445, field comments condensed onto their fields; commit 1c3ad24.

/// Closed receipt returned by a hook plugin.
#[derive(Debug, Clone, Deserialize, Serialize)]
#[serde(deny_unknown_fields)]
pub struct HookReceipt {
    pub schema: String,           // stable receipt schema
    pub status: String,           // allow, deny, or completed
    pub plugin: String,
    pub hook_key: String,
    pub event_id: Option<i64>,    // absent for pre-policy admission
    pub idempotency_key: String,  // replay-safe identity
    pub output: Value,            // plugin-defined, closed to the platform
}

Comparing Listing 3 with Definition 3.3 gives the reading used throughout: $\tau_c$ is schema, and $\sigma_c$ is the tuple (plugin, hook_key, event_id, idempotency_key) carried on the corresponding request. The scope $\mathrm{scope}(c)$ is the subscription’s event pattern together with its optional application and manifest filters, and the witness is the receipt itself. The check is a single function.

Listing 4. crates/orchestrator/src/hooks.rs lines 693-727, abridged; commit 1c3ad24.

fn validate_receipt(request: &HookRequest, receipt: &HookReceipt,
                    expected_status: &str) -> anyhow::Result<()> {
    ensure!(receipt.schema == HOOK_RECEIPT_SCHEMA, "hook receipt schema mismatch");
    ensure!(receipt.status == expected_status,  "hook receipt status must be ...");
    ensure!(receipt.plugin == request.plugin,   "hook receipt plugin mismatch");
    ensure!(receipt.hook_key == request.hook_key, "hook receipt key mismatch");
    ensure!(receipt.event_id == request.event.id, "hook receipt event mismatch");
    ensure!(receipt.idempotency_key == request.idempotency_key, "... mismatch");
    ensure!(receipt.output.is_object(), "hook receipt output must be an object");
    Ok(())
}

Listing 4 is a receipt-shaped check in the sense of Definition 3.6: six equalities between witness fields and request parameters, plus one syntactic test. It is total and decidable. This is the single most important identification in the paper, and also the one that bounds its claims. There is no theorem anywhere in Listing 3 or Listing 4 for a $\tau$ to denote.

The replay identity is a hash of transported data.

Listing 5. crates/orchestrator/src/hooks.rs lines 249-258, commit 1c3ad24.

/// Deterministic replay identity for one subscription and canonical event.
pub fn hook_idempotency_key(hook_key: &str, event_id: i64) -> String {
    let mut digest = Sha256::new();
    digest.update(b"agenthero.hook.v1\0");
    digest.update(hook_key.as_bytes());
    digest.update([0]);
    digest.update(event_id.to_string().as_bytes());
    format!("{:x}", digest.finalize())
}

A parallel function pre_policy_idempotency_key (line 1002) uses a distinct domain tag agenthero.hook.pre-policy.v1 and a request identifier in place of the event identifier, so the two phases hash disjoint prefixes.

5.3 Admission

The admission predicate of Proposition 3.34 is implemented as a loop over matching subscriptions with two failure paths, both of which refuse.

Listing 6. crates/orchestrator/src/hooks.rs lines 1101-1142, abridged; commit 1c3ad24.

match executor.invoke(&request).await {
    Ok(receipt) => {
        if let Err(error) = validate_receipt(&request, &receipt, "allow") {
            persist_policy_decision(pool, .., "deny",
                                    Some(&receipt), Some(..)).await?;
            bail!("pre-policy hook `{hook_key}` denied admission: {error}");
        }
        persist_policy_decision(pool, .., "allow", Some(&receipt), None).await?;
        receipts.push(receipt);
    }
    Err(error) => {
        persist_policy_decision(pool, .., "error", None, Some(..)).await?;
        bail!("pre-policy hook `{hook_key}` failed closed: {error}");
    }
}

Two properties of Listing 6 matter. A receipt that fails validate_receipt is treated as a denial rather than as an error to be retried, and an executor that fails to produce a receipt at all is likewise a refusal. The decision, whichever way it goes, is persisted before the function returns, under a uniqueness constraint on (request, subscription). The selection query that produces the subscription list (lines 1051 to 1066) also selects plugin_bundle_sha256. Lines 1073 to 1077 raise an error when it is absent, so an unpinned plugin cannot be consulted for admission.

5.4 Fenced delivery

Post-commit certificates are delivered from a durable queue with leases and fences. A claim increments the fence, takes the lease, and is committed before the plugin runs.

Listing 7. crates/orchestrator/src/hooks.rs lines 593-607, abridged; commit 1c3ad24.

let attempt     = row.try_get::<i32, _>("attempts")? + 1;
let fence_token = row.try_get::<i64, _>("fence_token")? + 1;
sqlx::query(
    "update hook_deliveries set state = 'leased', attempts = $2, fence_token = $3,
            lease_owner = $4, leased_until = now() + make_interval(secs => $5),
            updated_at = now()
     where id = $1",
).bind(id).bind(attempt).bind(fence_token).bind(lease_owner).bind(lease_seconds)
 .execute(&mut *tx).await?;
tx.commit().await?;

Completion is conditional on the lease and fence still matching, and a mismatch is detected rather than ignored.

Listing 8. crates/orchestrator/src/hooks.rs lines 642-662, abridged; commit 1c3ad24.

pub async fn complete_hook_delivery(pool: &PgPool, claim: &HookDeliveryClaim,
                                    receipt: &HookReceipt) -> anyhow::Result<()> {
    validate_receipt(&claim.request, receipt, "completed")?;
    let changed = sqlx::query(
        "update hook_deliveries set state = 'completed', receipt = $4, ...
         where id = $1 and state = 'leased'
           and lease_owner = $2 and fence_token = $3",
    ).bind(claim.id).bind(claim.lease_owner).bind(claim.fence_token)
     .bind(serde_json::to_value(receipt)?).execute(pool).await?.rows_affected();
    ensure!(changed == 1, "stale hook completion was fenced");
    Ok(())
}

The parallel function fail_hook_delivery (line 665) applies the same fenced predicate, chooses between the failed and dead_letter states according to HookFailurePolicy and the attempt count, and computes a quadratic backoff capped at sixty seconds.

The other fence in the system is the durability barrier, which sits between a node’s admission and its handler. Its module documentation states the contract and its receipt carries the fence.

Listing 9. crates/orchestrator/src/durability.rs lines 1, 17-22 and 271-285, abridged; commit 1c3ad24.

//! Canonical, lease-fenced commit-before-dispatch storage.

/// Commit one exact validated node-attempt identity before handler dispatch.
/// The signed worker lease is locked and checked in the same transaction as
/// the node projection and event insert. Returning a receipt therefore proves
/// PostgreSQL accepted the fence; an adapter event or in-memory observation is
/// never treated as acknowledgement.

receipt: DurabilityBarrierReceipt {
    schema: DURABILITY_RECEIPT_SCHEMA.to_string(),
    durable_ref: format!("postgres:dag_events/{event_id}"),
    dag_type: request.dag_type.clone(),
    manifest_hash: request.manifest_hash.clone(),
    node_id: request.node_id.clone(), attempt: request.attempt,
    fence: u64::try_from(event_id)?,
}

The last line of Listing 9 is the whole of Theorem 6.3 in one expression. The fence of a durability-barrier receipt is the identifier of the row the barrier inserted into dag_events, and that column is declared id bigserial primary key (supabase/migrations/20260522000002_app_runtime_tables.sql, line 133). At this commit that path is a symbolic link to agenthero/migrations/20260522000002_app_runtime_tables.sql, whose lines are the ones cited. One sequence, one table, every installed application.

5.5 The deployment map

$\Phi$ is realized in two independent halves. For model-backed stages there is a name-keyed factory.

Listing 10. crates/llm-adapter/src/lib.rs lines 430-446, abridged; commit 1c3ad24.

/// Build a provider by short name.
pub fn provider_by_name(name: &str, cfg: &ProviderConfig)
    -> Result<Arc<dyn LLMProvider>, LLMError> {
    match name {
        /* four feature-gated provider names */
        other => Err(LLMError::Provider(format!("unknown provider: {other}"))),
    }
}

For process-backed stages there is a manifest-declared adapter.

Listing 11. crates/orchestrator/src/dag_apps.rs lines 541-575, abridged; commit 1c3ad24.

/// Adapter declaration for an installed DAGOps app.
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum AppAdapter {
    /// Spawn a local process and exchange JSON over stdin/stdout.
    Process { command: String, runtime_commands: Vec<String>,
              host_commands: Vec<String>, environment: Vec<String>,
              args: Vec<String>, /* ... */ },
}

Both halves are keyed by a name rather than by a stage. The assignment of a stage to a name lives in the application manifest and in configuration, so the code realizes the second factor of $$\Phi \colon \mathrm{St}(G) \xrightarrow{\ \text{manifest and configuration}\ } \mathit{Names} \xrightarrow{\ \text{resolution}\ } R .$$ This factorization is what makes $\Phi$ a parameter in Banu’s sense: the resolution half is fixed code, the assignment half is data that a deployment can change without touching $(G, \mathrm{Know})$. It is also why Law 6 is not automatic. A check that reads a root directory chosen by the adapter’s environment reads the left factor.

5.6 Registry composition

Installed applications are discovered from a directory of manifests, and the discovery function performs exactly the compatibility test of Proposition 3.21.

Listing 12. crates/orchestrator/src/dag_apps.rs lines 1410-1427 and 2442-2458, abridged; commit 1c3ad24.

pub fn load_app_manifests_from_root(root: &Path)
    -> anyhow::Result<Vec<AppManifest>> {
    /* one manifest per subdirectory containing app.yaml */
    manifests.sort_by(|a, b| a.slug.cmp(&b.slug));
    validate_unique_dag_types(&manifests)?;
    Ok(manifests)
}

fn validate_unique_dag_types(manifests: &[AppManifest]) -> anyhow::Result<()> {
    let mut owners = BTreeMap::<&str, &str>::new();
    for manifest in manifests { for action in &manifest.actions {
        if let Some(owner) = owners.insert(action.dag_type.as_str(),
                                           manifest.slug.as_str()) {
            if owner != manifest.slug {
                bail!("dag_type `{}` is declared by both app
                       `{owner}` and app `{}`", ..);
            } } } }
    Ok(())
}

The set $N$ of global names of Definition 3.20 is the set of manifest type identifiers, $\nu$ is the assignment of a type identifier to each declared action, and the compatibility test is the injectivity check in Listing 12. The check is performed over all installed applications at once, before any of them is admitted, which is the implementation of a partial monoidal product refusing an inadmissible pair.

5.7 The harness runtime boundary

Two functions in the JavaScript harness runtime carry structure the model needs. The first normalizes raw provider output before it reaches anything else. sanitizeProviderSessionEvents (packages/harness-runtime/src/provider-session.mjs, line 8) is documented as converting provider JSONL into “bounded, content-safe operator session events”, against explicit budgets declared at lines 1 to 3 (MAX_VISIBLE_TEXT_CHARACTERS, MAX_VISIBLE_RECORD_CHARACTERS, STREAM_FLUSH_BYTES). It is wrapped by ProviderSessionCapture (line 114), which suppresses repeated tool call identifiers. This sits between the model and the rest of the architecture and belongs to neither $G$ nor $\mathrm{Know}$: it is part of the realization.

The second is a check, and it is the counterexample of Theorem 3.32(2) in the field.

Listing 13. packages/harness-runtime/src/workspace.mjs lines 22-30 and 51-65, abridged; commit 1c3ad24.

export function resolveManagedArtifactPath(artifact, workspaceRoot) {
  const expected = artifact.metadata?.content_sha256 ?? artifact.metadata?.sha256;
  const artifactStore = process.env.AGENTHERO_ARTIFACT_STORE_DIR;
  const allowedRoots = [workspaceRoot, artifactStore]
        .filter(Boolean).map(r => resolve(r));
  /* ... URI parsing ... */
  if (!allowedRoots.some((root) => isStrictDescendant(root, path)))
    throw new Error(`artifact path is outside an authorized root: ${path}`);
  if (!existsSync(path) || !lstatSync(path).isFile()
      || lstatSync(path).isSymbolicLink())
    throw new Error(`artifact path is missing, non-regular, or symbolic: ${path}`);
  if (expectedHash) {
    const actual = createHash("sha256").update(readFileSync(path)).digest("hex");
    if (actual !== expectedHash)
      throw new Error(`artifact content hash mismatch ...`);
  }
  return path;
}

Listing 13 performs three tests. The content hash comparison factors through $(G, \mathrm{Know})$: the expected hash is carried in the artifact reference, which is transported data. The containment and symbolic link tests do not: allowedRoots is built from the workspace root and from an environment variable naming the artifact store, both of which are deployment data.

The corresponding certificate $c_{\mathrm{art}}\in\mathrm{Know}$ has claim identifier managed-artifact, parameters for the artifact URI and expected digest, and scope equal to the consuming stage. Its witness records the resolved path, actual digest, file kind, and symlink status. The checker requires a regular non-symlink file, digest equality when a digest is supplied, and strict containment under a root in the consuming stage’s deployment record $\Phi(n)$. The first two clauses are deployment-independent; containment reads $\Phi$.

6 Law checking

The seven laws are tested against the source identifiers in Table 1. Each result is an implementation claim from source inspection at commit 1c3ad24, not an observation of a running system. The durability and hook subsections then supply the schema hypotheses required by Theorem 6.3 and Proposition 6.7.

6.1 Law 1: separability

Hook certificates are rows in a hook_subscriptions table, selected at admission time by a query on phase, enabled and the event pattern (crates/orchestrator/src/hooks.rs, lines 1051 to 1066). They are installed by a separate manifest schema agenthero.hook.v1 (line 30), whose receipt counterpart HOOK_RECEIPT_SCHEMA is declared at line 34. Nothing about installing, listing or removing a hook requires editing a wiring: the certificate layer is addressable on its own. Compared with the situation Part III reports for CatDB, where policy is evaluated inline with planning and provenance is attached to individual field values inside an executed plan, this is a genuine separation.

DagToolPolicy (crates/dag-runtime/src/lib.rs:566) carries budget, approval, network, filesystem, subprocess, and credential policy inside the manifest. Stage scope alone does not make that record a certificate under Definition 3.3: no claim identifier, witness, or replay checker is specified here. We therefore exclude it from $\mathrm{Know}$ rather than using it as a counterexample to separability. Law 1 holds for the identified hook-certificate layer; whether tool policy admits a complete certificate interpretation remains open.

6.2 Law 2: receipt identity replay

validate_receipt (Listing 4) is total, decidable, and compares six identity fields plus one structural test. It is called on both paths: at admission with expected status allow (line 1103) and at completion with expected status completed (line 647). The receipt type is closed under deny_unknown_fields, so the check cannot be evaded by adding fields. A mismatch produces a refusal, not a warning.

6.3 Law 3: deterministic replay identity

hook_idempotency_key (Listing 5) is a SHA-256 digest over a domain tag, the subscription key and the canonical event identifier, with explicit zero-byte separators between fields, so distinct field tuples cannot produce the same input string. pre_policy_idempotency_key uses a different domain tag. The store enforces the same identity independently: hook_deliveries carries unique (subscription_id, event_id) (supabase/migrations/20260824000002_plugin_hooks.sql, line 57), so a second delivery row for the same pair cannot be created.

One qualification is required by Definition 3.30. The identity is a function of the subscription key and an event identifier assigned by the store at insert time. Under an architecture morphism the subscription key is transported, but the event identifier is not architecture data. The certificate is therefore replay-stable relative to a fixed event stream, and not across two runs of the same architecture. This is a real narrowing: Law 3 is only partially satisfied.

6.4 Law 4: fail-closed admission

Listing 6 refuses on three distinct conditions: an executor error, a receipt that fails validation, and, before either, a subscription without a pinned plugin bundle hash. Each refusal propagates out of evaluate_pre_policy_hooks and therefore out of the mutation that called it, and there is no branch on which a failed check yields admission. The three differ in what they leave behind. The executor-error and invalid-receipt paths call persist_policy_decision before raising, so a decision row survives. The missing-bundle path raises at lines 1073 to 1077, before the request is built, so nothing is persisted for it.

By Proposition 3.34 this has a consequence the implementation cannot avoid. Installing an additional enabled pre_policy subscription whose pattern matches an event is a morphism that preserves every existing certificate and can turn an admitted mutation into a refused one. The selection query at line 1053 returns the new row, and the loop conjoins its decision. A harness that satisfies Law 4 is one whose admission predicate is antitone in $\mathrm{Know}$, and no amount of certificate preservation repairs that.

6.5 Law 5: fence exclusion

For writes to the canonical store the law holds. complete_hook_delivery (Listing 8) and fail_hook_delivery both predicate their update on id, state = ’leased’, lease_owner and fence_token. Both assert rows_affected() == 1, with the messages “stale hook completion was fenced” and “stale hook failure was fenced”. A superseded writer’s update matches no row and the mismatch is raised. The claim path (Listing 7) takes the row with for update ... skip locked inside a transaction and increments the fence before committing, so two dispatchers cannot hold the same fence.

The law concerns whether a stale writer can update the canonical record, and that property holds. External effects form a separate limitation. A plugin invoked under a claim runs as a child process. InstalledPluginHookExecutor is declared at line 749 of the same file, and its invoke method at line 1149 spawns the resolved process with env_clear() at line 1163 and an explicit environment whitelist. That is environment isolation and not filesystem or network isolation, neither of which appears at this boundary. The plugin may perform an external effect before its completion is fenced out. The platform offers a deduplication key for this case, the idempotency_key field on AppAdapterRequest (crates/agent-runtime/src/app_protocol.rs:233). Its own documentation places the obligation on the adapter: it is a “stable key adapters use to deduplicate retried external side effects”. The field is data the platform supplies, not a check the platform performs, so whether a retried effect is suppressed is decided outside the harness. Fencing protects the canonical record, not the world.

6.6 Law 6: $\Phi$-independence

Listing 13 constructs its authorized root set from workspaceRoot and from process.env.AGENTHERO_ARTIFACT_STORE_DIR, and refuses any path that is not a strict descendant of one of them. Both are deployment data in the sense of Section 5.5: they are determined by where the harness placed the application and which store the environment names, not by the wiring or the certificate set. The check therefore reads $\Phi$. This particular certificate is not replay-stable: redeploying the same $(G, \mathrm{Know})$ against a different artifact root changes whether a path lying under one root but not the other passes. Theorem 3.32(2) gives the same shape of counterexample but is not needed as a universal inference.

The same function contains a check on the other side of the line. The content hash comparison against artifact.metadata.content_sha256 depends only on transported data, and by Theorem 3.32(1) it is replay-stable. One function, two certificates, one preserved and one not. This is the sharpest available statement of what Law 6 costs and why a realization should separate the two tests rather than conjoining them.

6.7 Law 7: name disjointness

validate_unique_dag_types (Listing 12) is called by load_app_manifests_from_root at line 1425, before the manifest list is returned, and raises when two distinct application slugs declare the same type identifier. The enumeration entry points reach it: load_app_manifests (line 1405) delegates to it directly, and registered_dag_apps (line 2461) calls load_app_manifests. This is Proposition 3.21’s decision procedure, realized.

One qualification belongs here. The check is a property of enumeration, not of loading. load_app_manifest_by_slug_from_root (line 1443) reads a single manifest and never sees the others, so it cannot detect a collision and does not try to. The implementation decides admissibility of the composite whenever it forms the composite, which is what Proposition 3.21 requires. It says nothing when one factor is loaded alone, which the proposition does not require.

6.8 Laxness on the durability fragment

The fragment result follows. Everything in it is determined by the stage sets and by one schema fact, and no part of it refers to a run. The schema fact enters only as a named hypothesis of Theorem 6.3, that the composite’s sequencing relation is total, and it is discharged for AgentHero in the paragraph following the proof. The theorem does not depend on how, or whether, it is discharged. Proposition 6.7 is built the same way around the opposite hypothesis, that delivery fences are per row.

The receipt identity set is the set of shapes a barrier receipt may take, determined by $G_\mathcal{A}$ alone. It is countably infinite, and it is not a set of receipts that were produced. The relation $\nabla_\mathcal{A}$ is total because the barrier’s fence is drawn from one database sequence, which is a fact about the schema, recorded after Theorem 6.3. Component labels are not constrained by $\mathbf{Sys}$ morphisms, mirroring Proposition 3.11: an interpretation records $\Phi$ as a labelling that a translation may change.

The hypothesis that the composite’s sequencing relation is total is the implementation-level claim, and it is a claim about a schema. It holds for AgentHero at commit 1c3ad24 because the barrier’s fence is u64::try_from(event_id)? (Listing 9), the event identifier is the primary key of dag_events, and that column is declared id bigserial primary key with no application scoping in its key (supabase/migrations/20260522000002_app_runtime_tables.sql, line 133). A bigserial column draws from one database sequence, so every row of the table, whichever application produced it, is co-sequenced with every other. A later migration states the intent in prose: “dag_events.id is allocated by PostgreSQL’s non-transactional sequence before this trigger runs. Reusing that value for an omitted run_seq preserves a strict order within every app run (gaps are allowed)” (supabase/migrations/20260827000003_lock_free_dag_event_sequence.sql, lines 3–5). The gaps within one application’s fences are the values other applications took, which is the same fact seen from the other side. Because PostgreSQL allocates sequence values before commit, the field establishes numeric allocation order. It does not by itself establish commit order or the order in which a replay consumer processes rows.

The two results just proved are instances of one criterion, which is where the categorical content sits. Say that an interpretation $A$ has local sequencing on a pair $\mathcal{A}, \mathcal{B}$ when the composite’s sequencing relation is exactly the transport, along $\mu_{\mathcal A,\mathcal B}$, of the disjoint-sum relation on $A(\mathcal A)\boxtimes A(\mathcal B)$. Composition then adds neither cross-summand pairs nor new pairs within a summand.

Theorem 6.3 and Proposition 6.7 are the two sides of Theorem 6.5, and the criterion is what makes them more than a pair of observations about integer counters. Strength of an interpretation is not a property of the architectures being composed. It is a property of the sequencing resource the realization gives them, and it holds precisely when that resource is partitioned along the same boundary the architectures are. A design that wants strength must therefore make its ordering resource local to a component; a design that wants a single cross-application allocation order must give strength up. Treating that order as replay order additionally requires consumers to sort by it and accept gaps and commit-order inversions. No third option exists for the modeled relation, because the criterion is an equivalence.

6.9 Strength of the hook-fence abstraction

The same harness is strong elsewhere, and the contrast is instructive.

The certificate coordinate $c$ retains its scope, but $A_{\mathrm{hk}}$ does not use that scope to restrict the event coordinate $e$. The proposition therefore concerns only the partition of possible receipt identities by fence resource. It does not prove that scope-based event eligibility is preserved by composition, nor does it model the set of deliveries that actually occur. A stronger operational target would need an architecture-indexed event set and an explicit eligibility relation between certificate scopes and event targets.

The implementation-level claim behind Proposition 6.7 is that hook_deliveries.fence_token is a per-row counter rather than a shared sequence: the column is declared bigint not null default 0 (supabase/migrations/20260824000002_plugin_hooks.sql, line 48), the same file constrains a row to one subscription and one event with unique (subscription_id, event_id) (line 57), and Listing 7 sets the token to that row’s previous value plus one. Two delivery rows are therefore never co-sequenced, which is the schema fact the proposition needs.

7 Layer composition

7.1 Layer contribution

Parts I to III each describe a component of an architecture. None of them describes the act of installing that component somewhere, deciding whether an operation on it is admitted, or recording that the operation happened. Those three are what the harness adds, and they correspond exactly to $\Phi$, to the admission predicate, and to the witness set.

The addition is not free. Each of the three brings a failure mode that the component layers do not have. $\Phi$ brings Theorem 3.32(2): once deployment is a parameter, checks that read it stop being stable. Admission brings Proposition 3.34: once refusal is conjunctive and fail-closed, adding a certificate changes behaviour even though every old certificate is preserved. Recording brings Theorem 6.3: once the record is ordered by a shared resource, composition creates information that neither factor had.

7.2 Part I dependency

Part I models a memory store by two coalgebras on the same carrier (10): a store coalgebra for a deterministic input-output functor whose alphabet is the memory interface extended by an allocation oracle, and a lineage coalgebra whose final semantics is the ancestry of a record. This Part uses neither construction. It uses only the boundary the two of them fix. A certificate is something checked; a memory record is something remembered. As stated in Part I, the schema registry and structured-data validation belong on the $\mathrm{Know}$ side and the stored lineage belongs on the $S$ side, and Part I’s separation theorem shows that ContextFS’s recorded state is single-axis, so a retroactive correction and a belated recording are indistinguishable in it. Five of Part I’s eight law clauses fail against its own system. That result sets the standard: a pillar paper in this series reports the failures rather than restricting attention to the fragment that works.

The dependency is architectural rather than realized. At commit 1c3ad24 the AgentHero workspace manifest (Cargo.toml, lines 1–72) lists eight member crates and its third-party dependency set, and neither names ContextFS; the harness runtime package (packages/harness-runtime/package.json, lines 1–21) declares no dependency block at all. A case-insensitive search over the Rust, TOML and JavaScript sources likewise returns no occurrence of the name. The harness does carry a store-side projection of session content, agent_session_memory_chunks (supabase/migrations/20260824000001_agent_session_memory.sql, line 4), keyed by source_event_id, but that is store state and not a coalgebra in Part I’s sense; it has no evolve, merge, split or supersede operations and no lineage edges. The composition of the memory pillar with this harness is therefore a statement about the series’ model, not about a shipped integration, and we say so rather than implying otherwise.

7.3 Part II dependency

Part II’s operad is realized in the same repository as this Part’s harness, which makes the boundary between them a matter of discipline rather than of packaging. The division we adopt is the one recorded in both contracts: Part II owns NodeHandler and the reading of a validated manifest as an operadic composite; this Part owns AppAdapterRequest, AppAdapterResponse and provider_by_name, which are the deployment boundary rather than the composition law.

Three results from Part II are used here (11). Validation establishes a finite acyclic dependency graph but not the rooted output and unique supplier map needed to determine one operadic operation. A plain operad splits a multi-output invocation into coordinate generators, while a PROP preserves it as one operation. Actual sibling-output disjointness is sufficient for order-independent merging, while a collision carrying distinct values is a counterexample; declared disjointness is insufficient unless returned value keys are confined. That statement is the operad-level analogue of Proposition 3.21: in both cases a composition law is total on the model and partial on the implementation, and in both cases the side condition concerns disjointness of names. The two conditions are not the same condition, since one is about actual outputs within a manifest and the other about type identifiers across applications, but both expose collisions in a shared namespace.

7.4 Part III dependency

The prospectus asks whether the series has one wiring object or two. The answer this Part adopts, following Part III (12), is two: $\mathcal{W}$ and $\mathcal{O}$ are distinct operads sharing a colour vocabulary, and there is no checkable identification of CatDB’s port-type alphabet with AgentHero’s string-keyed JSON ports at the pinned commits. Part III’s type-erasure result is in two halves, and both are needed here. In one direction, any assignment sending a CatDB port type to the manifest key at which a tool response is stored is constant on all port types stored at that key, so it is not injective as soon as two distinct field sets share a key. In the other direction, nothing checks an assignment at all, because the manifest edge type records a source and a target node identifier and no port datum.

This Part therefore does not fix one $G$ for the series. $G$ is a component slot in Definition 3.8, and different architectures fill it with different wiring objects of the same shape. Definition 3.1 names the harness-level filler and defines it as a general wiring in Part III’s operad $\mathcal{W}_\mathsf{T}$, not as a tree wiring; nothing in Proposition 3.10, Proposition 3.18, Theorem 3.32 and Theorem 6.3 depends on which filler is chosen, because all four are proved from the stage set, the certificate set and the deployment map alone. That is a deliberate feature of the presentation: the results transfer to any Part’s wiring, which is what makes them series-level results rather than AgentHero-level ones.

Remark 3.2 adds a second, independent difference between the two layers. The protocol system’s wirings are tree wirings and the harness’s are not, so the two Parts are studying different fragments of the same operad, and a result proved by induction over a tree in Part III has no automatic counterpart here. The series therefore does not describe one wiring object seen from four angles.

On the $\mathrm{Know}$ side the two Parts divide the evidence. Part III reports that CatDB’s policy decisions and field provenance records are certificate-shaped, in a sense this Part would make precise as Definition 3.6, but are not separately addressable, so the $G$ and $\mathrm{Know}$ components are not distinguishable at the crate level. This Part reports (Section 6.1) that AgentHero separates its modeled hook certificates. Per-operation tool policy is not classified as a certificate here because a complete witness and checker mapping was not established.

7.5 Dependency graph

This Part imports Part I’s coalgebra as a component realized inside a harness, Part II’s operad as the composition law for stages within one application, and Part III’s wiring operad $\mathcal{W}_\mathsf{T}$ as the shape of $G$, on the non-tree fragment described in Remark 3.2. It exports Definition 3.3, Remark 3.5, Definition 3.8 and the reading of certificate preservation as replay stability to Parts II and III, both of which cite them without restating them. Nothing proved in this Part is used in the proof of any result in Parts I to III, so the import graph restricted to formal dependencies is acyclic, with this Part as its unique sink. The cycles the prospectus asks each Part to state are operational rather than formal: a Part II operation may call a Part I memory operation at runtime, and a Part III wiring may carry a Part II skill as a node, without either Part importing the other’s definitions.

8 Limits and counterexamples

8.1 Receipt-shaped certificates

Banu’s Definition 1 requires $\tau$, a theorem statement. Listing 3 has schema, a version string. Listing 4 compares identities. The output field is documented as “plugin-defined closed-to-the-platform output”, which means the platform does not interpret it, so no logical content can be recovered from it either.

The consequence bounds the enterprise as applied here. Preservation of a certificate means, by Definition 3.30, that a decidable identity check keeps accepting the same transported records; it does not mean that a property of the system is preserved, because no property is stated. The harness has $\mathrm{Know}$-shaped machinery with $\mathrm{Know}$-content that Proposition 3.7 shows to be blind to everything except identity and record shape. What remains true is narrower and still worth stating: the machinery is the right shape, the checks are total and decidable, the identities are deterministic, and the results of Section 3 apply. Section 10 states what filling $\tau$ would require.

8.2 Sorting hypothesis

Theorem 3.32(1) needs the value set to be sorted, so that a stage identifier can never be confused with a payload string. The hook certificates satisfy it, because HookRequest and HookReceipt give names and payloads distinct typed record positions (Remark 3.4). The manifest port vocabulary does not, and the failure is not hypothetical.

As stated in Part II, AgentHero’s manifest ports are keyed by arbitrary strings with JSON payloads, so a certificate written against manifest ports rather than against hook records has no protection from Example 8.1. This bounds the theorem’s reach inside the very system it is about, and the boundary runs along the same line as Part II’s: wherever the port vocabulary is untyped, the structural results weaken. The reach can be stated exactly. Every certificate identified in Sections 5.2 and 5.4 has a witness that is a closed record with typed positions, a hook receipt or a durability receipt, so the sorting hypothesis holds for all of them and Theorem 3.32(1) applies to all of them; the harness at this commit carries no certificate whose witness is a manifest port map. A certificate of that kind would have to establish the hypothesis first, by typing its name-valued fields, and the theorem says nothing about it until it does.

8.3 Redeployment counterexample

Section 6.6 exhibits resolveManagedArtifactPath as a check that reads the deployment map, and Theorem 3.32(2) shows such checks are not replay-stable. The model predicts this rather than being embarrassed by it. The containment test is security-relevant, so the certificates most likely to read $\Phi$ are the ones a deployment cares most about. Moving the deployment-relative part of such a test into the wiring, by making the authorized root a declared port type rather than an ambient environment variable, is what Part III reports CatDB does for authorized field sets, and is the available remedy.

8.4 Lax composition

By Theorem 6.5 the interpretation cannot be made strong on the durability fragment without changing the store design. A harness that draws its fences from one sequence violates the strong-functor requirement. The single shared order supplied by that design is also what obstructs strength.

8.5 Reference vocabulary

Banu’s four-pillar table names concrete components of his own reference implementation: BiTemporalMemory and RunContext for Memory, SkillStage and PatternTemplate for Skills, WiringDiagram for Protocols, and SkillOrganism for Harness. A recursive search for these six identifiers across the Rust, JavaScript and TypeScript sources of AgentHero at commit 1c3ad24 returns no match, and Parts I to III report the same for their own systems. The search is stated exactly in Appendix A, because an absence is not exhibited by any line. Nothing in this series implements that vocabulary. The claim is only that a system built without knowledge of it independently exhibits a structure the vocabulary names, which is a weaker and more interesting claim than implementation would be, and a reader should hold it to the weaker standard.

8.6 Fence scope

Section 6.5 records that a plugin can perform an external effect and then be fenced out of recording it. The model as stated has no vocabulary for this: $\mathbf{Sys}$ objects carry components and receipts, and an unrecorded effect is neither. Extending $\mathbf{Sys}$ with an effect monad and asking which of Law 5’s guarantees survive is the most concrete gap between this model and the systems it is about.

8.7 Missing system composition

The four-pillar reading describes a harness as the layer that composes memory, skills and protocols. At commit 1c3ad24 AgentHero composes one of the three. Its workspace manifest declares eight member crates and a third-party dependency set naming neither ContextFS nor CatDB (Cargo.toml, lines 1–72), and the case-insensitive searches recorded in Appendix A find no occurrence of either name in the sources. The DAG runtime that Part II studies is in the same repository, so that composition is present in the artifact. The other two are compositions the model supports and the code has not yet made. The formal results are unaffected, since none of them mentions a particular component system, but a reader entitled to expect a harness that composes three named systems should know that it composes one.

9 Related work

The immediate antecedent is Banu (2), whose correspondence this Part tests on an independent system. The differences are worth naming. Banu validates with five compiler functors and one reference implementation, and reports certificate preservation rates across those targets; this Part validates with one implementation and reports which certificate kinds can be preserved in principle, with a separation theorem distinguishing them. Banu’s certificates carry theorem statements by construction because he wrote them; the certificates here do not, which is what forces Definition 3.6. Banu’s own limitations section names the static framework, the single reference implementation, the restriction of certificate scope to structural invariants, a two-model escalation experiment and an 8B-parameter format-discipline ceiling on SWE-bench-lite. This Part adds a second, independently developed system and one negative structural result; it does not address the experimental limitations at all.

The ArchAgents framework (4) supplies the triple. This Part uses its shape and gives its own definitions of the category and the monoidal structure, because the operational questions asked here, in particular the status of $\Phi$ under morphisms and the fence order on receipts, are finer than the comparative framework needs.

Cao (3) argues that agentic systems are a restructuring of software engineering rather than an improvement of it, on a complexity-scaling argument: interaction paths among $n$ components grow as $\Theta(2^n)$ against roughly constant human capacity to reason about them. Theorem 6.3 is a small piece of counter-pressure on the optimistic reading of that argument. If composing two agent applications creates ordering information that belongs to neither, then the composite is not understandable by understanding the parts, which is the same difficulty in categorical dress.

Zhou et al. (19) give the four pillars, Meng et al. (9) the enumerative harness taxonomy, and Pan et al. (18) the natural language harness study that Banu reads as evidence that harnesses are portable objects with algebraic structure. Banu’s reference list attributes that study to a different first author; the attribution used here follows the arXiv record. Trivedy (16) states the industry framing that the model holds the intelligence and the harness is what makes it useful.

For the compositional apparatus, Spivak’s operad of wiring diagrams (15) and its directed (13) and dynamical (17) refinements are Part III’s source and are cited here only for the shape of $G$. Fong and Spivak (5) is the general reference. Mac Lane (8) supplies the monoidal category definitions. Rutten (14) and Jacobs (6) are Part I’s sources. Ma et al. (7) supply the atomic-skills result Banu reads as operadic. That preprint has since been withdrawn by its authors over errors in its data, which is worth recording because it is one of the two empirical supports Banu offers for the operadic reading of the Skills pillar. Nothing proved here depends on it; it is cited only through Part II and only for the composition vocabulary.

Prior work by the present author describes a different harness in a different runtime. The agent-os papers at commit 61cb399 present an Elixir umbrella application composing a scheduler, a tool interface, a memory layer and a planner engine through a dependency-ordered supervision tree, and argue that every pairwise combination of subsystems yields capabilities that neither has alone (1). That is the same composition-creates-structure claim made informally, and Theorem 6.3 is one precise instance of it. A naming collision must be flagged: the agent-os series has its own Part IV, the Planner Engine, which is unrelated to this series’ Part IV. Where this paper writes Part IV it always means the present one.

10 Conclusion

At commit 1c3ad24, application manifests, hook records, and name-keyed resolution make the three components of an Architecture triple identifiable. Five laws hold, deterministic replay identity is partial, and deployment-independent checking fails for managed artifact containment. The evidence therefore supports a structural correspondence, not a transfer of system guarantees: the modeled certificates attest identity and record form rather than substantive theorems.

11 Open problems

The harness needs a theorem field. Definition 3.6 is a degenerate case of Definition 3.3, and the gap between them is a specific piece of engineering: a claim language in which a hook can state what its receipt attests, and a checker that evaluates the claim against the receipt rather than against the request’s identity fields. Until that exists, Theorem 3.32(1) preserves identity and nothing else.

The choice between one fence sequence and many remains open. Theorem 6.3 and Proposition 6.7 exhibit both designs in one system. The question is whether the global allocation order the durability barrier provides is worth the loss of strength. That order is not itself a commit or replay order; a replay claim requires evidence that consumers sort by the field and tolerate gaps and commit-order inversions.

$\mathbf{Sys}$ also needs to record effects that were performed but not recorded. Section 8.6 shows that Law 5 is about the store and not about the world, and that the model has no way to say so. An object of $\mathbf{Sys}$ carrying a set of external effect identifiers, with morphisms required to preserve them, would let the gap between a fenced record and an unfenced side effect be stated as a failure of a square to commute rather than as a remark.

The two disjointness conditions in Section 7.3 may be instances of one theorem. Part II’s equivariance condition on sibling output keys and this Part’s compatibility condition on global type identifiers are both partiality conditions on a composition law, arising from name collision in a shared namespace. If there is a single statement subsuming them, it would apply at every level of this series, and if there is not, the reason would explain why the levels are genuinely different.

12 Code evidence

Every code-backed claim in the paper has a row. All AgentHero rows are at commit 1c3ad24; the agent-os row is at commit 61cb399. Pinning to an immutable commit hash is what makes the citations stable rather than fragile: a later refactor produces a different commit and leaves the cited one unchanged, so a reader can reconstruct exactly the artifact the claims were checked against. The formal results of Section 3 are independent of the code and remain whatever the repository does next; what a refactor can invalidate is the status of a law in Table 2, which is the intended, checkable content of Section 6. Statements in the last column are implementation-level claims established by source inspection at the stated commit, not reports of observed runs.

Two claims in Section 8 are absence claims and cannot be pinned to a line, since no line exhibits the absence of a name. They are stated here as the exact searches that establish them, each reproducible at the pinned commit. A case-insensitive recursive search of the AgentHero tree over files matching *.rs, *.toml and *.mjs for the strings contextfs and catdb returns no match. A separate recursive search over *.rs, *.mjs and *.ts for RunContext, SkillOrganism, PatternTemplate, WiringDiagram, BiTemporalMemory and SkillStage, the six component names in Banu’s four-pillar table, returns no match. The table below gives the positive, line-pinned evidence that neither system is declared as a dependency.

References

[1] M. Long. The AI Operating System, Part V: Modular Synthesis. agent-os repository, papers/latex/synthesis.tex, commit 61cb399, 2025.

[2] B. Banu. Harness Engineering as Categorical Architecture: Structural Guarantees Are Harness-Level Properties. arXiv:2605.12239, 2026.

[3] Z. Cao. Agentic Software: How AI Agents Are Restructuring the Software Paradigm. arXiv:2606.05608, 2026. The version consulted here is titled “The End of Software Engineering: How AI Agents Are Fundamentally Restructuring the Software Paradigm”.

[4] P. de los Riscos, F. J. Corbacho, and M. A. Arbib. Towards a category-theoretic comparative framework for artificial general intelligence. arXiv:2603.28906, 2026.

[5] B. Fong and D. I. Spivak. Seven Sketches in Compositionality: An Invitation to Applied Category Theory. arXiv:1803.05316, 2018.

[6] B. Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science 59, Cambridge University Press, 2016.

[7] Y. Ma, Y. Liu, X. Yang, et al. Scaling coding agents via atomic skills. arXiv:2604.05013, 2026. Withdrawn by the authors; the submission history records errors in the data affecting the validity of the results.

[8] S. Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, Springer, 2nd edition, 1998.

[9] Q. Meng, Y. Wang, L. Chen, Q. Wang, C. Lu, W. Wu, Y. Gao, Y. Wu, and Y. Hu. Agent harness for large language model agents: A survey. Preprints, DOI 10.20944/preprints202604.0428.v2, 2026.

[10] M. Long. Coalgebraic Memory. Part I of the Agentic Engineering series, The YonedaAI Collaboration, YonedaAI Research Collective, 2026. GrokRxiv:2026.09.memory-coalgebra.

[11] M. Long. Operadic Skill Composition. Part II of the Agentic Engineering series, The YonedaAI Collaboration, YonedaAI Research Collective, 2026. GrokRxiv:2026.09.skills-operad.

[12] M. Long. Typed Protocol Wiring. Part III of the Agentic Engineering series, The YonedaAI Collaboration, YonedaAI Research Collective, 2026. GrokRxiv:2026.09.protocols-wiring.

[13] D. Rupel and D. I. Spivak. The operad of temporal wiring diagrams: Formalizing a graphical language for discrete-time processes. arXiv:1307.6894, 2013.

[14] J. J. M. M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. DOI 10.1016/S0304-3975(00)00056-6.

[15] D. I. Spivak. The operad of wiring diagrams: Formalizing a graphical language for databases, recursion, and plug-and-play circuits. arXiv:1305.0297, 2013.

[16] V. Trivedy. The anatomy of an agent harness. LangChain Blog, March 2026. https://www.langchain.com/blog/the-anatomy-of-an-agent-harness.

[17] D. Vagner, D. I. Spivak, and E. Lerman. Algebras of open dynamical systems on the operad of wiring diagrams. Theory and Applications of Categories, 30:1793–1822, 2015. arXiv:1408.1598.

[18] L. Pan, L. Zou, S. Guo, J. Ni, and H.-T. Zheng. Natural-language agent harnesses. arXiv:2603.25723, 2026. Banu’s reference list attributes this work to “Erik Willstrom et al.”; the arXiv record lists the authors given here.

[19] C. Zhou, H. Chai, W. Chen, et al. Externalization in LLM agents: A unified review of memory, skills, protocols and harness engineering. arXiv:2604.08224, 2026.