Lost in Translation: A Formal Semantics of Cross-Protocol Interoperability for Autonomous Agents

The agent ecosystem has converged not on one interoperability protocol but on several—Google’s Agent-to-Agent (A2A) protocol, the Model Context Protocol (MCP), the Agent Communication Protocol (ACP), and the Agent Network Protocol (ANP)—each with a different message model, task lifecycle, authority model, and fault vocabulary. Production systems already chain these protocols through gateways, and a two-layer reference architecture plus a stated cross-vendor joint-specification effort make cross-protocol bridging a near-term reality. Yet there is no formal account of what it means for such a bridge to preserve meaning. A task delegated over A2A, bridged to an ANP agent, fulfilled, and reported back can silently lose capability semantics, have its authority scope distorted, alias distinct task states, or mask typed faults, with no artifact making the loss detectable. The existing literature is either descriptive (protocol surveys) or formal but intra-protocol (commitment-based conformance and interoperability for a single formalism). This paper provides the missing cross-formalism account. We (i) give a protocol-agnostic Abstract Interaction Model (AIM) that assigns each protocol a labelled-transition semantics over a common domain of capabilities, task-lifecycle posets, authority lattices, and fault domains; (ii) define a semantic bridge and a faithfulness criterion adapting the process-calculus encoding criteria of Gorla (compositionality, operational correspondence, divergence reflection, success sensitiveness) and adding two domain-specific criteria—authority preservation and state faithfulness; (iii) prove that faithful bridges compose (so A2A→ACP→ANP chains are well-behaved under stated conditions), that sound bridges cannot amplify delegated authority, and a separation theorem showing that when one protocol exposes an observable distinction another cannot express, no faithful bridge between them exists—formalizing why naive gateways collapse to syntactic interoperability and silently drop features; and (iv) show constructively that an explicit bridge contract cannot defeat that impossibility but can convert silent loss into detectable, attributable loss. We relate the results to the convergence roadmap and to multi-agent miscoordination risk.

1. Introduction

The first wave of agent interoperability standardization did not produce a single protocol. It produced a family. Google’s Agent-to-Agent (A2A) protocol provides capability discovery via Agent Cards, a task/state model, and streaming over HTTP and Server-Sent Events [14, 15]. Anthropic’s Model Context Protocol (MCP) standardizes the orthogonal agent-to-tool channel with its own lifecycle and threat surface [13]. The Agent Communication Protocol (ACP) is a REST-native alternative with different session and authentication assumptions, and the Agent Network Protocol (ANP) targets fully decentralized, peer-to-peer discovery; comparative surveys document the divergence in interaction modes, discovery, and security frameworks across all four, and a 2026 threat model extends the comparison to further variants [15, 14, 18]. These protocols are widely described as complementary, and production stacks already place them in series: an agent on one protocol delegating, via a gateway, to an agent on another.

Complementarity at the level of architecture diagrams is not the same as semantic interoperability. When a task crosses a protocol boundary, the boundary is a translation, and translation can lose meaning. Consider a conditional commitment expressed in a protocol whose task model supports antecedents being bridged to a protocol whose task model is unconditional; a streaming, partially-observable task state projected onto a protocol that only exposes terminal states; a typed, recoverable fault flattened into a generic error; or a delegation scope that, re-expressed in the target protocol’s authority model, is widened because the target lacks the qualifier that constrained it. In each case the gateway can return “success” while the obligation that the originating principal believed it had delegated was never faithfully represented on the other side. We call these cross-protocol semantic failures, and they are presently invisible: nothing in the current stack records what a bridge preserved or dropped.

The relevant theory exists but on the wrong side of the gap. The classical multi-agent systems literature formalized interoperability rigorously, but within a single formalism: Chopra and Singh define interoperability via the alignment of commitments and the orthogonal notions of conformance and coverage for agents enacting one protocol [7, 8, 9]. Conceptual-interoperability frameworks such as the Levels of Conceptual Interoperability Model (LCIM) classify interoperability into technical, syntactic, semantic, pragmatic, and higher levels, observing that implementation-level standards do not by themselves yield semantic interoperability [2, 1]. Concurrency theory provides a mature account of when one formalism can faithfully encode another—Gorla’s unified encoding criteria (operational correspondence, divergence reflection, success sensitiveness, compositionality) and the associated separation results [5, 6, 3, 4]. None of this has been brought to bear on the concrete, deployed problem of bridging A2A, MCP, ACP, and ANP. The protocol surveys, conversely, are descriptive: they tabulate differences but do not say when a bridge across those differences preserves meaning, nor when it provably cannot.

Contributions.

• An Abstract Interaction Model (AIM): a protocol-agnostic labelled-transition semantics assigning each protocol a behavior over a common domain of capability descriptors, task-lifecycle posets, authority lattices, and fault domains, so that heterogeneous protocols become formally comparable (Section 4).
• A definition of a semantic bridge and a faithfulness criterion, adapting Gorla’s encoding criteria to the agent setting and adding two domain-specific criteria absent from the concurrency literature—authority preservation and state faithfulness (Section 5).
• A threat model isolating five cross-protocol failure modes (capability loss, authority distortion, state aliasing, fault masking, asynchrony mismatch) and theorems: faithful bridges compose under a stated side condition (so multi-hop A2A→ACP→ANP chains are well-behaved); sound bridges cannot amplify delegated authority; and a separation theorem: if a protocol exposes a success-distinguishing observable another cannot express, no bridge between them is simultaneously operationally corresponding and success sensitive (Sections 3, 6).
• A constructive result that an explicit bridge contract cannot defeat the separation impossibility but provably converts silent semantic loss into detectable, attributable loss, and a corollary placing naive gateways at the LCIM syntactic level for any unspported feature (Section 6).
• A discussion relating the results to the convergence roadmap and to multi-agent miscoordination risk (Sections 7–8).

This is a formal and architectural contribution; we make no empirical claims. Full proofs are in Appendix 10.

2. Background and Related Work

2.1 Interoperability: levels and limits

Wegner’s early synthesis framed interoperability as the ability of systems to exchange and meaningfully use services despite heterogeneity [1]. The Levels of Conceptual Interoperability Model distinguishes a hierarchy from technical and syntactic exchange up through semantic, pragmatic, dynamic, and conceptual interoperability, and argues that implementation-level standards deliver only the lower levels [2]. We use LCIM as a yardstick: our separation theorem says precisely that a feature unsupported by a target protocol cannot exceed the syntactic level across that bridge, regardless of engineering effort.

2.2 Encoding criteria from concurrency theory

Comparing the expressive power of formalisms via translations is a mature subject. Felleisen formalized relative expressiveness for programming languages [4]; Milner’s bisimulation gives the behavioral equivalences over which faithfulness is judged [3]; Gorla consolidated a small set of criteria—compositionality, operational correspondence, divergence reflection, success sensitiveness—now standard for judging whether an encoding is a valid means of language comparison, with companion separation (impossibility) results, later contextualized against full abstraction [5, 6]. We transpose these criteria from process calculi to agent interoperability protocols, which is sound because an agent protocol, abstractly, is a labelled transition system with observables; the transposition is, to our knowledge, new, and it is not free: agent protocols carry authority and task-state structure that the concurrency criteria do not address, which is why we add two further criteria.

2.3 Commitment-based, intra-protocol interoperability

Chopra and Singh define interoperability for open multi-agent systems via the alignment of social commitments, and separate it from conformance (an agent respecting a protocol) and coverage [7]; “constitutive interoperability” grounds interoperation in agents entering and maintaining well-aligned commitments [8], and subsequent work relates choice, interoperability, and conformance for interaction protocols and choreographies [9]. This line is the closest formal prior art and a conceptual input to ours, but it is intra-formalism: it concerns agents enacting a common protocol/choreography. The present paper addresses the orthogonal, now-pressing problem of heterogeneous protocol families with different message models and lifecycles, where the question is whether the bridge between formalisms preserves meaning. Commitment semantics [10, 11, 12] supplies one instance of the task/obligation structure our AIM abstracts over.

2.4 The protocol landscape and convergence

Surveys characterize MCP, A2A, ACP, and ANP and a convergence narrative toward a layered MCP-plus-A2A reference architecture with stated cross-vendor joint-specification intent [15, 14]; security analyses catalog transport- and tooling-layer threats and propose hardening [16, 17, 13, 18]; authenticated delegation and decentralized-identity work define how authority and identity cross service boundaries [19, 20]. These works are complementary: they neither define semantic-bridge faithfulness nor prove when it is unattainable, which is our subject. The Cooperative AI risk taxonomy identifies miscoordination among advanced agents as a core failure mode [21]; cross-protocol semantic loss is a concrete, infrastructural source of exactly such miscoordination.

3. Problem Setting and Threat Model

3.1 Actors and assumptions

We consider agents that each speak one protocol from a set {P,Q,R,…} and bridges (gateways) that relay an interaction from one protocol to another. A bridge is software; it may be benign-but-lossy or adversarial.

Assumption 1 (Protocol-as-LTS). Each protocol P is given a labelled transition system semantics (Section 4); its externally meaningful behavior is its set of reachable observables, including a success observable ✓ marking the declared successful terminal state of a delegated task.

Assumption 2 (Common semantic domain). Capability descriptors, task-lifecycle states, authority scopes, and fault labels of every protocol embed into a common domain D (Section 4); without such an embedding the protocols are incomparable and no bridge is meaningful.

Assumption 3 (Authority layer). Delegated authority is expressed as a scope in an authority lattice and is carried with tasks, as in authenticated-delegation models [19, 20]; issuance and revocation are provided by that layer.

3.2 Failure modes

A capability or task feature expressible in the source protocol has no image in the target; the bridge silently projects it away (e.g. a conditional commitment bridged to an unconditional task model).

The source-side delegated scope is re-expressed in the target authority lattice as a strictly larger scope (privilege amplification) or an incomparable one.

Distinct source task-lifecycle states map to a single target state, so an endpoint decision that depends on distinguishing them is made on corrupted information.

A typed, possibly recoverable fault is flattened to a generic error (or to success), hiding information the originating principal needed.

Differing synchrony/streaming assumptions cause the bridge to introduce divergence or to report completion before the delegated obligation is observable.

G1, G3, G4 are expressiveness failures; G2 an authority failure; G5 a behavioral failure. The analysis shows G1/G4/G5 are governed by operational correspondence and success sensitiveness, G2 by an authority-preservation criterion, and G3 by state faithfulness; and that some instances are not engineering bugs but provable impossibilities (Theorem 3).

4. The Abstract Interaction Model (AIM)

4.1 Common domain

The semantic domain is D=⟨Cap,⊑c; (L,⊑,T); (A,≤,⊓,⊔); F⟩ where: Cap is a set of capability descriptors with a refinement preorder ⊑c (x⊑cy: “x is at least as specific/strong as y”); (L,⊑) is a finite task-lifecycle poset with a designated terminal antichain T⊆L (e.g. done, failed, cancelled); (A,≤,⊓,⊔) is an authority lattice of scopes (≤: “no more permissive than”); and F is a finite fault domain with a distinguished ⊥F (no fault). All four are equipped with the discrete information order needed below.

4.2 Protocols as labelled transition systems

A protocol is P=⟨CP,ActP,→P,⟦⋅⟧P⟩: configurations CP, a transition relation →P labelled by internal and observable actions, and a semantic map ⟦⋅⟧P:CP→D-LTS sending a configuration to its meaning: the capability it offers/requests, its current lifecycle state, the authority scope it carries, and any fault. Write ⇒P for the reflexive-transitive closure of internal steps, C⇓{P}^{✓} for “C can reach a configuration whose lifecycle state is the declared successful terminal,” and ≈P for the chosen behavioral equivalence (a weak bisimulation/barbed congruence over D-observables, in the sense of [3, 5]). A protocol instance is a configuration; agents are instances; the parallel composition C1∥C_2 models two interacting endpoints.

5. Semantic Bridges and Faithfulness

Definition 1 (Semantic bridge). A bridge B:P⇀Q is a (partial) translation on configurations and actions of P into those of Q, together with a scope embedding ι:A^P​→A^Q and a lifecycle map h:L^P​→L^Q on the domain components.

Adapting Gorla’s encoding criteria [5] and adding two domain-specific criteria, B is faithful iff:

There is a Q-context N with B(C1∥C2)≈QN(B(C1),B(C2)) for all endpoints C1,C_2 (homomorphic on ∥ in the simplest case).

Completeness: C⇒PC′ implies B(C)⇒QD with D≈QB(C′). Soundness: B(C)⇒QD implies there is C′ with C⇒PC′ and D⇒QD′≈_QB(C′).

If B(C) diverges then C diverges.

C⇓{P}^{✓} iff B(C)⇓{Q}^{✓}.

For every task accepted in Q under B, its carried scope is ≤Qι(source scope); and ι is monotone: a≤Pb⇒ι(a)≤_Qι(b) with ι(⊤)≠ the unrestricted scope unless the source scope was unrestricted.

h is monotone and terminal-preserving (h(T^P)⊆T^Q, mapping successful to successful); B is alias-free if h is injective on the reachable sublattice of L^P.

Definition 2 (Cross-protocol interoperability). Agents a on P and b on Q are interoperable via B iff the B-mediated composition is success sensitive (C4), authority preserving (C5), and divergence-free on the protocols’ intended runs (C3), so that every interaction that would reach ✓ in a homogeneous deployment reaches it across the bridge, without authority escalation.

A bridge contract κ_B=⟨h,ι,Δ⟩ publishes the lifecycle map, scope embedding, and the set Δ of P-observables the bridge does not preserve; it is the artifact that makes residual loss explicit (Theorem 4).

6. Analysis

We state results under Section 3’s assumptions; proof sketches appear here, complete proofs in Appendix 10.

Theorem 1 (Composition of faithful bridges). Let B1:P⇀Q and B2:Q⇀R be faithful (C1–C6). If B2 reflects the target equivalence (maps ≈Q-related configurations to ≈R-related ones) and the maps compose (h2∘h1, ι2∘ι1 monotone), then B2∘B_1:P⇀R is faithful.

Sketch. Operational correspondence composes by transitivity once B2 preserves ≈Q (needed to push B1’s “up-to-≈Q” matches through B_2); success sensitiveness and divergence reflection compose because each is an iff/implication chained across the two; C5 and C6 compose by monotone composition of ι and h and transitivity of ≤, ⊑; compositionality composes by nesting contexts. Full argument and the precise role of equivalence reflection in Appendix 10.2. ◻

Theorem 2 (Authority non-amplification). If B satisfies C2-soundness and C5, then no B-mediated interaction yields, in Q, an accepted task whose scope exceeds ι of the source-authorized scope. Hence cross-protocol delegation cannot escalate privilege except by violating C5 (or by authority-layer mis-issuance, excluded by assumption).

Sketch. Any accepted Q-task is, by C2-soundness, the image of a reachable P-configuration whose scope is the source scope; C5 bounds its Q-scope by ι(source scope) and forbids ι from mapping a restricted scope to the unrestricted one. The contrapositive is the claim. Appendix 10.3. ◻

Theorem 3 (Separation: no faithful bridge for an inexpressible distinction). Suppose there exist P-endpoints C1,C2 that are success-distinguishable in P: some P-context K gives K(C1)⇓{P}^{✓} and K(C2)⇓̸{P}^{✓} (e.g. C1 a conditional commitment whose antecedent the context supplies, C2 one it does not; or C1 exposing a typed recoverable fault the context recovers from, C2 not). Suppose further that Q’s observable algebra cannot separate their images, i.e. every faithful B forces B(C1)≈QB(C_2) because Q has no observable distinguishing them (the feature is absent from Q). Then no bridge B:P⇀Q satisfies C1, C2, and C4 simultaneously.

Sketch. By C1 the P-context K induces a Q-context B(K). By C2+C4, success sensitiveness is preserved under context: K(C1)⇓{P}^{✓} forces B(K)(B(C1))⇓{Q}^{✓}, and K(C2)⇓̸{P}^{✓} forces B(K)(B(C2))⇓̸{Q}^{✓}. Hence B(C1)≉QB(C_2) (a context separates them), contradicting the hypothesis that Q cannot separate them. This is the agent-protocol instance of Gorla-style separation [5, 6] and Felleisen-style expressiveness bounds [4]. Appendix 10.4. ◻

Corollary 1 (LCIM collapse of naive gateways). For a feature present in P but absent in Q, a bridge with no contract for that feature attains at most LCIM syntactic interoperability for it (level 2) and necessarily fails semantic interoperability (level 3): the feature is exchanged in form but not in meaning, exactly the silent projection of G1/G4.

Sketch. Theorem 3 forbids meaning-preservation for the feature; the bytes still transit, which is LCIM level 2 by definition [2]. Appendix 10.4. ◻

Theorem 4 (Detectability via bridge contracts). Let B satisfy C2-soundness and publish a contract κB=⟨h,ι,Δ⟩ enumerating its non-preserved observables Δ. Then there is an endpoint monitor that, observing only Q-side behavior and κB, flags every B-mediated run on which a Δ-feature was exercised. Contracts cannot defeat Theorem 3, but they convert silent loss (G1–G5) into detectable, attributable loss.

Sketch. Construct the monitor as the product of the Q-LTS with the predicates “a P-run exercising a δ∈Δ would have been required here.” C2-soundness gives that every Q-run corresponds to some P-run; κ_B enumerates exactly the lost δ; the monitor raises a flag iff the corresponding P-run’s δ is in Δ. Soundness/completeness of detection follow. Appendix 10.5. ◻

Proposition 1 (State aliasing). If h is monotone but not injective on the reachable sublattice of L^P, there are distinct reachable s≠s′ with h(s)=h(s′); if any Q-endpoint decision depends on distinguishing s,s′ the bridge is not state-faithful (G3). Alias-freedom holds iff h restricted to reachable states is an order-embedding.

Sketch. Non-injectivity gives the colliding pair directly; an order-embedding is by definition injective and order-reflecting, which is exactly alias-freedom plus C6. Appendix 10.6. ◻

Remark 1. Theorems 1–2 are the positive results (multi-hop bridges are safe when each hop is faithful and authority cannot be amplified); Theorem 3 and Corollary 1 are the negative result (some interoperability is provably unattainable, not merely unimplemented); Theorem 4 is the constructive mitigation (make the unavoidable loss visible). Together they say: design bridges to declared contracts, never to a lowest common denominator.

6.1 Failure-mode coverage

7. Discussion

The convergence roadmap.

The dominant convergence story is a layered MCP-plus-A2A reference architecture with cross-vendor joint-specification intent [15, 14]. Our results sharpen what that effort must deliver: convergence on transport (LCIM levels 1–2) is the easy part and is largely done; semantic convergence (level 3+) for any feature on which the protocols genuinely differ is, by Theorem 3, impossible to obtain by bridging alone—it requires either a common supertype for the feature or an explicit contract that admits the loss. The actionable recommendation is that the joint specification standardize bridge contracts (κ_B), not merely message mappings, so that Theorem 4 applies and loss is never silent.

Relation to multi-agent risk.

The Cooperative AI taxonomy lists miscoordination among the principal multi-agent failure modes [21]. Cross-protocol semantic loss is a concrete, infrastructural generator of miscoordination: two agents each behaving correctly in their own protocol can still fail jointly because the bridge between them silently dropped a conditional, a fault type, or an authority qualifier. Bridge contracts plus the detectability monitor turn such failures from silent into diagnosable, which is a prerequisite for governance.

Deployment.

AIM is an analysis instrument, not a runtime; the deployable artifacts are the bridge-contract schema and the endpoint monitor of Theorem 4, both layerable onto existing gateways without changing the underlying protocols, and compatible with authenticated-delegation authority carriage [19, 20].

8. Limitations and Future Work

Equivalence choice. Results are stated modulo a chosen behavioral equivalence ≈; a coarser equivalence weakens C2 and the separation theorem, a finer one strengthens both. Selecting the right equivalence per protocol pair is future empirical work. Model fidelity. AIM abstracts each real protocol into an LTS over D; the theorems are only as good as those embeddings, which must be validated against the concrete A2A/MCP/ACP/ANP specifications. Contract expressiveness. κ_B enumerates lost observables; richer, quantitative loss (partial preservation, lossy compression of state) is not yet modeled. Liveness and timing. Real bridges add latency and timeouts; a timed extension is needed for G5 beyond divergence. No empirical evaluation. A reference AIM encoding of two concrete protocols, a contract schema, and a measured monitor are the natural next steps.

9. Conclusion

The agent ecosystem standardized on several protocols, not one, and now bridges them. Bridging is translation, and translation can silently lose meaning. We gave a protocol-agnostic semantics, a faithfulness criterion that extends concurrency-theoretic encoding criteria with authority and task-state structure, and proved the shape of the problem: faithful bridges compose and cannot amplify authority, but when one protocol can express a distinction another cannot, no faithful bridge exists, and naive gateways collapse to syntactic interoperability for that feature. The remedy is not a better bridge but an honest one: standardized bridge contracts that make the unavoidable loss explicit and detectable. As convergence proceeds, the question is not whether agents on different protocols can exchange messages—they can—but whether what crosses the boundary still means what it meant.

10. Complete Proofs

10.1 Preliminaries

Fix protocols as LTSs over D (Section 4). For a configuration C, Obs(C) is the set of D-observables reachable from C via ⇒; C⇓^✓ abbreviates ✓∈Obs(C) where ✓ is the declared successful terminal observable. ≈ is a weak barbed congruence: an equivalence, closed under the protocol’s contexts, that equates configurations with the same observables up to internal steps [3, 5]. A context K(⋅) is a configuration with a hole; congruence means C≈C′⇒K(C)≈K(C′). An encoding/bridge B is compositional (C1) if it commutes with composition up to a fixed context, and operationally corresponding (C2) as defined in Section 5. We use the standard fact that, for ≈ a congruence, success is context-monotone: if some context separates two configurations by ✓ they are not ≈-related.

10.2 Proof of Theorem 1 (Composition)

Proof. Write B=B2∘B1, h=h2∘h1, ι=ι2∘ι1. We verify C1–C6.

C2 (operational correspondence). Completeness: let C⇒PC′. By B1 completeness, B1(C)⇒QD1≈QB1(C′). By B2 completeness applied to B1(C)⇒QD1, B2(B1(C))⇒RE≈RB2(D1). Now D1≈QB1(C′) and, by hypothesis, B2 reflects the source equivalence, i.e. X≈QY⇒B2(X)≈RB2(Y); hence B2(D1)≈RB2(B1(C′))=B(C′). Transitivity of ≈R gives E≈RB(C′), the required match. The equivalence-reflection hypothesis is necessary: without it, B2 might not carry B1’s up-to-≈Q match to an up-to-≈R match, and completeness would not chain. Soundness is the symmetric argument: a ⇒R run of B(C) is, by B2 soundness, matched by a ⇒Q run of B1(C) up to ≈R​∘B2, which by B1 soundness is matched by a ⇒P run of C; composing the two matchings and using that ≈ is transitive yields a C′ with C⇒_PC′ and the image of C′ equivalent to the endpoint.

C4 (success). C⇓{P}^{✓}⇔B1(C)⇓{Q}^{✓} (C4 of B1) ⇔B2(B1(C))⇓{R}^{✓} (C4 of B2); compose the iffs.

C3 (divergence reflection). If B(C)=B2(B1(C)) diverges in R then by C3 of B2, B1(C) diverges in Q, then by C3 of B_1, C diverges in P.

C5 (authority). For an accepted R-task, C5 of B2 bounds its scope by ι2(its Q-scope); that Q-scope is, by C5 of B1, ≤Qι1(source scope). Monotonicity of ι2 gives ι2(⋅)≤Rι2(ι1(source scope))=ι(source scope). Transitivity of ≤R closes it; ι maps a restricted scope to the unrestricted one only if some ιi did, contradicting C5 of that B_i.

C6 (state). h=h2∘h1 is monotone (composition of monotone maps) and terminal-preserving (h1(T^P)⊆T^Q, h2(T^Q)⊆T^R, success to success by each). If each hi is injective on the relevant reachable sublattice and B1 maps reachable states into the sublattice on which h_2 is injective, then h is injective there (composition of injections), giving alias-freedom; otherwise C6’s monotone, terminal-preserving part still holds.

C1 (compositionality). Let Ni witness C1 for Bi. Then B(C1∥C2)=B2(B1(C1∥C2))≈RB2(N1(B1(C1),B1(C2))); applying C1 of B2 to the binary context N1 (treating its holes as composed sub-terms) yields a R-context N=N2⟨N1⟩ with B(C1∥C2)≈RN(B(C1),B(C2)), using equivalence reflection of B2 to transport the ≈Q step. Hence all of C1–C6 hold and B is faithful. ◻

10.3 Proof of Theorem 2 (Authority non-amplification)

Proof. Let tQ be any task accepted in a B-mediated run, with carried scope aQ. By C2-soundness, the accepting Q-configuration D satisfies: there is a reachable P-configuration C′ with C⇒PC′ and D⇒QD′≈QB(C′). The scope carried by C′ is the source-authorized scope aP (authority is a domain component preserved by ⟦⋅⟧, Assumption 3). By C5, aQ≤Qι(aP). Suppose, for contradiction, aQ exceeds ι(aP), i.e. aQ≰Qι(aP). This directly negates the C5 inequality just derived—contradiction. The only escapes are: (a) C5 fails for B (excluded by hypothesis), or (b) the authority layer mis-issued or failed to revoke aP at the source, excluded by Assumption 3. Moreover C5 forbids ι from sending a strictly restricted aP to the unrestricted scope, so amplification cannot enter through ι itself. Hence no B-mediated interaction yields a Q-task whose scope exceeds ι of the source scope. ◻

10.4 Proof of Theorem 3 and Corollary 1 (Separation)

Proof. Assume, for contradiction, a bridge B:P⇀Q satisfying C1, C2, C4, while (i) K is a P-context with K(C1)⇓{P}^{✓} and K(C2)⇓̸{P}^{✓}, and (ii) Q has no observable separating B(C1) from B(C2), so any faithful bridge yields B(C1)≈QB(C_2).

By C1 there is a Q-context B(K) (the image of K under the compositional translation) such that for i∈{1,2}, B(K(Ci))≈QB(K)(B(Ci)). By C4 applied to the whole configuration K(Ci): K(C1)⇓{P}^{✓} implies B(K(C1))⇓{Q}^{✓}, and K(C2)⇓̸{P}^{✓} implies B(K(C2))⇓̸{Q}^{✓} (C4 is an iff, so it transports both success and its negation; C2 ensures the ⇒ behavior underlying ⇓^✓ is matched, so ⇓^✓ is well-defined on images). Since ⇓^✓ is invariant under ≈Q (a barbed congruence preserves barbs), B(K)(B(C1))⇓{Q}^{✓} and B(K)(B(C2))⇓̸_{Q}^{✓}.

Thus the single Q-context B(K) separates B(C1) and B(C2) by the observable ✓. Because ≈Q is a congruence, two ≈Q-related configurations cannot be separated by any context; therefore B(C1)≉QB(C_2). This contradicts (ii). Hence no bridge satisfies C1, C2, and C4 together; equivalently, any bridge preserving operational behavior and compositionality must sacrifice success sensitiveness for the distinguishing feature. This is the agent-protocol specialization of the encoding/separation methodology of [5, 6] and of relative-expressiveness arguments [4].

Corollary 1. Fix a feature present in P, absent in Q, witnessed by C1,C2 as above. By the theorem, no bridge preserves its meaning across P​→​Q, so semantic interoperability (LCIM level 3, “meanings understood” [2]) is unattainable for it. A naive gateway still serializes and transmits the feature’s bytes in some Q field, which satisfies LCIM level 2 (syntactic, structured exchange) by definition. No level strictly above 2 is reached for that feature; hence the gateway sits exactly at the syntactic level for it, and the feature is exchanged in form but not meaning—the silent projection identified as G1/G4. ◻

10.5 Proof of Theorem 4 (Detectability)

Proof. Let κB=⟨h,ι,Δ⟩ with Δ the declared non-preserved P-observables. Define a monitor M as a deterministic automaton running in product with the observed Q-LTS. For each δ∈Δ, κB specifies the Q-side syntactic footprint ϕδ that a P-run exercising δ induces under B (it exists because B is a fixed translation, so the pre-image pattern of any source feature is determined by B and recorded in the contract). M raises flag loss(δ) exactly when it observes ϕδ.

Soundness of detection (no false negatives). Suppose a B-mediated run exercises δ∈Δ at the P side. By C2-completeness the corresponding Q run exhibits the translated behavior, whose footprint is ϕδ by construction of κB; M observes ϕδ and flags loss(δ). Soundness of attribution (no false positives). Suppose M flags loss(δ). Then it observed ϕδ. By C2-soundness every Q run corresponds to a P run; by the contract’s definition ϕδ is produced only by the B-image of a P run that exercised δ (the contract pins ϕδ to δ). Hence a genuine δ-exercising source run occurred. Therefore M flags loss iff a Δ-feature was exercised: loss is detectable and attributable from Q-side observation plus κ_B alone.

Finally, M does not prevent loss: it cannot, by Theorem 3, since no faithful bridge for a Δ-feature exists; M only observes. Thus contracts strictly weaken silentness (G1–G5 become observable) without contradicting the impossibility. ◻

10.6 Proof of Proposition 1 (State aliasing)

Proof. Let Lr⊆L^P be the reachable sublattice and h:L^P→L^Q monotone. If h​↾​Lr is not injective, by definition there exist s≠s′∈Lr with h(s)=h(s′); these are reachable, so some B-mediated run presents the Q-state h(s) ambiguously for {s,s′}. If a Q-endpoint decision function d satisfies d(s)≠d(s′) in the intended semantics but receives only h(s)=h(s′), then d cannot recover the distinction: state faithfulness (C6’s alias-free clause) fails—this is G3. Conversely, h​↾​Lr is an order-embedding iff it is injective and both order-preserving and order-reflecting; injectivity is exactly alias-freedom, and order-preservation/-reflection is exactly C6’s monotone, terminal-respecting requirement restricted to reachable states. Hence alias-freedom holds iff h​↾​L_r is an order-embedding. ◻

References

[1] P. Wegner. Interoperability. ACM Computing Surveys, 28(1):285–287, 1996.

[2] A. Tolk and J. A. Muguira. The Levels of Conceptual Interoperability Model. In Proceedings of the 2003 Fall Simulation Interoperability Workshop, paper 03F-SIW-007, Orlando, FL, 2003.

[3] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[4] M. Felleisen. On the expressive power of programming languages. Science of Computer Programming, 17(1–3):35–75, 1991.

[5] D. Gorla. Towards a unified approach to encodability and separation results for process calculi. Information and Computation, 208(9):1031–1053, 2010. https://doi.org/10.1016/j.ic.2010.05.002.

[6] D. Gorla and U. Nestmann. Full abstraction for expressiveness: History, myths and facts. Mathematical Structures in Computer Science, 26(4):639–654, 2016. https://doi.org/10.1017/S0960129514000279.

[7] A. K. Chopra and M. P. Singh. Producing compliant interactions: Conformance, coverage, and interoperability. In Declarative Agent Languages and Technologies IV (DALT 2006), LNAI 4327, pages 1–15. Springer, 2006. https://doi.org/10.1007/11961536_1.

[8] A. K. Chopra and M. P. Singh. Constitutive interoperability. In Proceedings of the 7th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 797–804, 2008.

[9] M. Baldoni, C. Baroglio, A. K. Chopra, N. Desai, V. Patti, and M. P. Singh. Choice, interoperability, and conformance in interaction protocols and service choreographies. In Proceedings of the 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 843–850, 2009.

[10] M. P. Singh. A social semantics for agent communication languages. In Issues in Agent Communication, LNAI 1916, pages 31–45. Springer, 2000. https://doi.org/10.1007/10722777_3.

[11] P. Yolum and M. P. Singh. Flexible protocol specification and execution: Applying event calculus planning using commitments. In Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 527–534, 2002.

[12] Foundation for Intelligent Physical Agents. FIPA ACL Message Structure Specification, document SC00061G, 2002.

[13] X. Hou, Y. Zhao, S. Wang, and H. Wang. Model Context Protocol (MCP): Landscape, security threats, and future research directions. arXiv:2503.23278, 2025. https://doi.org/10.48550/arXiv.2503.23278.

[14] Y. Yang et al. A survey of AI agent protocols. arXiv:2504.16736, 2025.

[15] A. Ehtesham, A. Singh, G. K. Gupta, and S. Kumar. A survey of agent interoperability protocols: MCP, ACP, A2A, and ANP. arXiv:2505.02279, 2025.

[16] I. Habler, K. Huang, V. S. Narajala, and P. Kulkarni. Building a secure agentic AI application leveraging A2A protocol. arXiv:2504.16902, 2025.

[17] V. S. Narajala and I. Habler. Improving Google’s A2A protocol: Protecting sensitive data and mitigating unintended harms in multi-agent systems. arXiv:2505.12490, 2025.

[18] Security threat modeling for emerging AI-agent protocols: A comparative analysis of MCP, A2A, Agora, and ANP. arXiv:2602.11327, 2026.

[19] T. South, S. Marro, T. Hardjono, R. Mahari, C. D. Whitney, D. Greenwood, A. Chan, and A. Pentland. Authenticated delegation and authorized AI agents. arXiv:2501.09674, 2025.

[20] S. Rodriguez Garzon et al. AI agents with decentralized identifiers and verifiable credentials. arXiv:2511.02841, 2025.

[21] L. Hammond, A. Chan, J. Clifton, et al. Multi-agent risks from advanced AI. Cooperative AI Foundation, Technical Report #1; arXiv:2502.14143, 2025. https://doi.org/10.48550/arXiv.2502.14143.