CBCL: Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication Hugo O’Connor

arXiv:2604.14512v1 [cs.CR] 16 Apr 2026

Anuna Research [email protected]

cases, ad-hoc validation cannot reliably prevent the emergence of “weird machines” [2], unintended computational artifacts that attackers exploit to achieve behavior beyond a system’s intended functionality. Contemporary agent communication presents a particularly acute instance of this problem. Early ACLs such as KQML [3] and FIPA-ACL [6] defined core vocabularies of communicative acts (“performatives”). These languages are parseable and well-defined; KQML explicitly allowed communities to define new performatives by agreement, but without formal constraints on such extensions. In practice, extensibility was largely pushed into content languages and ontologies. Surveys of ACLs identify persistent interoperability failures. Heterogeneous agents remain confined to rigid contexts, and ad-hoc extensions proliferate incompatible dialects that are difficult to generalize without the original developers [4], [5]. In the terminology of Zambonelli et al. [20], traditional ACLs support only selfadaptation (parameter tuning within a fixed structure), not self-expression (structural evolution of the system itself). The modern alternative, using natural language or unrestricted JSON schemas as the communication substrate (as in MCP [7] and LLM-based agent frameworks), provides unlimited extensibility but creates an input language whose computational complexity is effectively unbounded. Determining whether an arbitrary natural language message will cause harmful behavior requires solving undecidable I. Introduction problems. Autonomous software agents increasingly coordinate This paper presents CBCL, a language designed to be through message-passing protocols to perform complex expressive, extensible, and tractable. CBCL provides a tasks: managing supply chains, orchestrating IoT device minimal core vocabulary (8 performatives) and a formal swarms, and mediating human–AI collaboration. The mechanism for agents to define, exchange, and adopt correctness and security of these systems depend critically new domain-specific vocabularies (“dialects”) at runtime, on how agents parse and interpret the messages they without centralized coordination and without escaping the exchange. DCFL complexity class. CBCL achieves this through hoLanguage-theoretic security (LangSec), as articulated moiconic self-extension. Dialect definitions are themselves by Sassaman, Patterson, Bratus, and Locasto in Security valid CBCL messages expressed in S-expression syntax, so applications of formal language theory [1], shows that they can be transmitted, verified, and installed using the the computational complexity class of an input language same parsing machinery used for ordinary communication. determines the difficulty of validation and the attack surface Three safety constraints, verified both in a Lean 4 formalthat parser implementations exhibit. Languages above the ization and enforced in a Rust reference implementation, deterministic context-free class introduce ambiguity that ensure that this self-extension is provably safe: makes parser equivalence undecidable [1], while Turing• R1 (No Recursion): Dialect templates are purely complete inputs make validation itself undecidable; in both declarative pattern-template substitutions. Direct and mutual recursion are forbidden (no cyclic dependencies Accepted at the LangSec Workshop, 2026 IEEE Security and Privacy Workshops (SPW). between performative templates). No iteration or

Abstract—Agent communication languages (ACLs) enable heterogeneous agents to share knowledge and coordinate across diverse domains. This diversity demands extensibility, but expressive extension mechanisms can push the input language beyond the complexity classes where full validation is tractable. We present CBCL (Common Business Communication Language), an agent communication language that constrains all messages, including runtime language extensions, to the deterministic context-free language (DCFL) class. CBCL allows agents to define, transmit, and adopt domain-specific “dialect” extensions as first-class messages; three safety invariants (R1–R3), machine-checked in Lean 4 and enforced in a Rust reference implementation, prevent unbounded expansion, applying declared resource limits, and preserving core vocabulary. We formalize the language and its safety properties in Lean 4, implement a reference parser and dialect engine in Rust with property-based and differential tests, and extract a verified parser binary. Our results demonstrate that homoiconic protocol design, where extension definitions share the same representation as ordinary messages, can be made provably safe. As autonomous agents increasingly extend their own communication capabilities, formally bounding what they can express to each other is a precondition for oversight. Index Terms—language-theoretic security, agent communication, multiagent systems, deterministic contextfree languages, formal verification, protocol security

© 2026 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

reflection is permitted. R2 (Resource Bounds): Every dialect declares static resource limits (nesting depth ≤ 64, expansion size ≤ 8192 characters, verification time ≤ 1000 ms) enforced at both installation and runtime. • R3 (Core Preservation): The eight core performatives cannot be redefined by any dialect, preserving protocol bootstrap invariants. Together, these constraints support DCFL preservation, meaning that the language recognized by a CBCL parser remains in DCFL regardless of how many dialects are installed. We give a formal argument in Section IV-G; the full closure proof is mechanized in Lean 4 (theorem dcfl_preserved). CBCL is named after McCarthy’s 1982 proposal for a “Common Business Communication Language” [9] that would be “open ended so that as programs improve, programs that can at first only order by stock numbers can later be programmed to inquire about specifications and prices. . . ” Our work aspires to this vision while providing formal security guarantees. Contributions. (1) A protocol design methodology that achieves runtime self-extension while preserving DCFL membership, applicable to message-passing systems where DCFL expressiveness is acceptable. (2) A Lean 4 formalization covering parser correctness (soundness and completeness), safety constraint verification (R1–R3), pipeline totality for parse/validate/verify, and DCFL preservation under dialect installation. (3) A Rust reference implementation (cbcl-rs) with dialect verification, gossip propagation, C FFI/WASM bindings, and fuzz targets; a verified parser binary extracted from the Lean proofs. (4) A draft IETF Internet-Draft specifying application/cbcl [10], with a proof-of-concept Nostr [30] transport binding (cbcl-nostr) for agent communication and Lightning Network micropayments over decentralized relays. •

TABLE I Agent communication protocols classified by input language complexity.

Protocol KQML [3] FIPA-ACL [6] MCP [7] LLM Agents CBCL

Complexity CFL CFL RE RE DCFL

Ext.

Verif.

Partial Partial Partial Partial Yes No Yes No Yes Yes

Weird M. Stack Stack Turing Turing None†

“Complexity” refers to the effective computational power of the end-to-end message interpretation pipeline, not the surface syntax alone. KQML and FIPA-ACL use S-expression envelope syntax (DCFL), but neither specification constrains the content language, so the end-to-end complexity is at least CFL. MCP and LLM agent frameworks can induce Turing-complete behavior when tool invocation permits arbitrary code execution. CFL = context-free language (Type 2); DCFL = deterministic CFL; RE = recursively enumerable (Type 0). Ext. = runtime self-extension of the protocol’s vocabulary; “Partial” indicates informal extensibility without safety guarantees (KQML’s open performative set, FIPA-ACL’s X- parameters). Weird M. = weird machine class [2]. † At the parser and template-expander layer; tool backends and agent action semantics are outside CBCL’s scope.

B. Why DCFL Is the Right Complexity Class The choice of DCFL (rather than regular, general CFG, or context-sensitive) is deliberate: Regular languages cannot express the nested structure of agent messages (envelopes wrapping messages, dialects scoping inner messages). • General CFL risks parser differentials: ambiguous grammars admit multiple parse trees, and attackers can exploit divergent interpretations [1], [16]. Every DCFL has an unambiguous grammar, making unambiguity a class-level property rather than a per-grammar proof obligation [13]. Parser equivalence is therefore preserved automatically under language evolution. • DCFL is the minimal class supporting nested structure with parser equivalence. Residual divergence from serialization or encoding is mitigated through canonical serialization (Section V-E). • Context-sensitive and beyond. Context-sensitive membership is PSPACE-complete [13]; Type 0 is undecidable. Both exceed the recognizer complexity that LangSec considers tractable for full input validation [1].

•

II. Background and Threat Model A. The Unbounded Attack Surface Problem Modern agent communication protocols have moved up the Chomsky hierarchy [29], from the well-defined grammars of KQML and FIPA-ACL to unbounded complexity, without acknowledging the security consequences implied by formal language theory [1], [2] (Table I). The threat model for CBCL assumes agents operating S-expression syntax is a natural fit: the grammar is in open Byzantine environments where: (1) untrusted LR(1)-parseable (indeed LL(1)) and nested parenthesized peers may send maliciously crafted messages designed to lists directly mirror the pushdown automaton’s stack exploit parser differentials, trigger resource exhaustion, operations. or inject unintended computation; (2) dialect definitions arrive from potentially adversarial sources and constitute III. CBCL Language Design executable extensions to the receiver’s behavior; and (3) no We use the following terminology throughout. A percentral authority controls participant conduct or vocabulary formative is a named message type (e.g., tell, ask). A evolution. The security goal is to ensure that no message, including dialect is a named, versioned collection of performative dialect definitions, can cause a conformant parser to enter definitions that extends CBCL’s core vocabulary. Each an unanticipated state or perform unexpected computation. dialect performative has a template: the pattern-template

substitution rule that maps dialect invocations to core CBCL messages. A. Core Grammar CBCL messages are S-expressions conforming to an ABNF grammar (fully specified in the IETF draft [10]). The top-level rules are: cbcl-message = simple-message / meta-message / lang-message / wrapped-message simple-message = "(" performative SP recipient [SP content] *(SP parameter) ")" SP = " " ; single ASCII space (0x20) performative = "tell" / "ask" / "reply" / "hello" / "bye" / "ok" / "error" / "cancel" lang-message = "(" "lang" SP dialect-name SP cbcl-message ")" s-expr = "(" *( s-expr / atom ) ")" atom = identifier / string / number / boolean / symbol

The four message categories are: Simple messages use one of eight core performatives: (tell @bob "The meeting is at 3pm") (ask @alice "Status of task-42?" :thread conv-17) (reply @alice "75% complete" :in-reply-to msg-9874) (ok @bob) (error @sender "parse failure") (hello @bob) (bye @bob)

A query meta message asks a peer whether it supports a dialect; a teach meta message transmits a previously defined dialect to another agent: (meta (query logistics @bob)) (meta (teach logistics @alice <dialect-definition>))

The teach payload is the same S-expression used in define; the receiving agent parses, verifies (R1–R3), and installs it using its existing CBCL infrastructure. Language-scoped messages invoke dialect performatives. Dialect invocations must appear inside a lang wrapper that names the dialect; bare dialect performatives at top level are syntactically invalid. This scoping rule is what makes the DCFL preservation argument (Section IV-G) straightforward: the lang tag serves as a deterministic dispatch token. (lang logistics (track-shipment "PKG-123" :route "A->B"))

This expands via pattern-template substitution to: (tell @tracking-svc (shipment-request :package "PKG-123" :route "A->B" :priority "normal") :domain logistics)

Colon-prefixed identifiers such as :thread and :in-reply-to are keyword parameters: named optional Wrapped messages provide metadata (envelopes), inarguments in the style of Common Lisp keyword symbols. tegrity (signatures), and resource governance: They are syntactically atoms (the symbol production in (with-limits :timeout 100 :max-depth 10 the grammar) and carry no special semantics beyond (ask @reasoner "Compute optimal path")) serving as self-quoting parameter labels. Meta messages operate on dialects—defining, querying, B. Homoiconic Self-Extension and teaching: CBCL’s dialect definitions are themselves valid CBCL (meta (define logistics (cbcl) @consortium messages, eliminating the need for a separate meta(:resource-requirements language parser (a second attack surface) or out-of-band ((max-depth 16) registry. Inspired by Racket’s #lang mechanism [11], a sin(max-expansion-size 4096) (verification-time 1000))) gle DCFL recognizer handles both ordinary communication (extend track-shipment (pkg-id &key route priority) and language extension; the DCFL preservation argument (tell @tracking-svc (Section IV-G) explains why installing a dialect does not (shipment-request :package pkg-id :route route increase the recognizer’s computational power. :priority (or priority "normal")) :domain logistics)) (:examples (track-shipment "PKG-42" :route "A->B") (tell @tracking-svc (shipment-request :package "PKG-42" :route "A->B" :priority "normal") :domain logistics))))

C. Template Expansion Semantics

Dialect performatives expand through a deliberately restricted template language supporting four forms: (1) literal templates with parameter placeholders, (2) substitution of parameter references with argument values, (3) bounded conditionals (cond ((= param value) template) ...) The optional :examples clause carries semantic meaning: with no recursion, and (4) sequences of template expreseach input/output pair illustrates what the dialect author sions. intends a performative to do in a concrete scenario. Because This template language is not Turing-complete. It CBCL cannot formally constrain meaning (Section VII-D), supports only flat pattern matching, finite conditional examples serve as the primary mechanism for communicat- branching, and one-shot substitution. Critically, expansion ing intended semantics between agents. A receiving agent is single-pass: the expanded result is not fed back through can additionally evaluate the examples against its own the expander. This ensures that template evaluation termiexpander to verify mechanical agreement before claiming nates in time linear in the template size plus substituted dialect support. argument size, and is bounded by declared expansion limits.

D. Message Processing Lifecycle Figure 1 shows the processing pipeline that every incoming message traverses. Steps 1–2 (parse, validate + classify) apply to all messages. The dialect-definition path (steps 3–4) applies only to meta define messages; the expansion path (step 5) applies only to lang invocations. The pipeline is total: every input produces either a well-typed result or a well-typed error (Theorem 12). IV. Safety Invariants and Formal Verification A. Lean 4 Formalization Overview We formalize CBCL in Lean 4 as a library (LeanCbcl) comprising modules for S-expressions, messages, parsing, serialization, pattern matching, dialect parsing, template expansion, deterministic-union reasoning, dialect constraints (R1–R3), and an end-to-end pipeline. The formalization comprises approximately 5,400 lines of Lean across 16 modules and yields 176 machine-checked theorems, with zero sorry gaps and no custom axioms. A verified parser binary (cbcl-parse) is extracted from the proofs. B. Parser Correctness

(envelope/signed/with-limits) messages. Because the grammar is DCFL, each valid input admits exactly one parse tree, so the Message returned by the parser is unique. Theorem 2 (Soundness). If parseMessage(e) = some m, then ValidMsgGrammar(e, m). Theorem 3 (Completeness). If ValidMsgGrammar(e, m) holds, then parseMessage(e) = some m. Soundness and completeness together establish that the parser recognizes exactly the message grammar encoded in Lean (via ValidMessageGrammar), no more, no less. This eliminates the possibility of parser differential attacks between the formal specification and the implementation, a core LangSec concern. We additionally verify 10 concrete round-trip properties (parse(serialize(e)) = Ok(e)) covering the seven atom types (symbol, integer, negative integer, boolean true/false, string, keyword), empty lists, flat lists, and nested lists. A SafeSymbol predicate formally characterizes which symbol names survive round-tripping (non-empty, no delimiters, not a boolean or integer literal); the general theorem roundtrip_safeSymbol proves round-tripping for all safe symbols via char-level parser reasoning.

C. R1: No Recursion Constraint R1 ensures that dialect performative templates contain no direct or mutual recursion, preventing unbounded expansion. The Lean 4 formalization covers both: Theorems 4–5 establish soundness and completeness for self-reference detection (a performative name cannot appear in its own template), while Theorem 7 proves soundness of mutual recursion prevention via a transitive-closure dependency predicate (DependsClosure) that detects cycles of any length in the performative dependency graph. Theorem 4 (R1 Soundness). If containsSelfRef (name, t) = false, then name does not occur anywhere in t. Theorem 5 (R1 Completeness). If name occurs in t, then containsSelfRef (name, t) = true. Theorem 6. The base dialect (8 core performatives) is R1-valid. Theorem 1 (Termination). For all inputs s, parseSExpr(s) terminates and produces either a valid SExpr or a parse Theorem 7 (Mutual Recursion Soundness). If verifyR1NoMutualRecursion(δ) = true, then no perforerror. mative in δ participates in a dependency cycle. A universal well-formedness theorem (allSExpr_wellThe mutual recursion verifier uses a computable Formed) additionally proves by structural induction that DFS-based cycle detector (checkNoCycles) with full every SExpr value satisfies the inductive WellFormedSExpr soundness and completeness proofs against a semantic predicate, ensuring the parser can only produce structurally mutualRecursion specification: no false negatives and no valid output. false positives. The Rust reference implementation mirrors In these theorems, e is an SExpr (the S-expression the computable version. parse tree/AST) and m is a Message (the semantic classification into simple, meta, dialect, or wrapped). The D. R2: Resource Bounds predicate ValidMsgGrammar(e, m) is an inductive relation Constraint R2 enforces static resource limits encoding which S-expressions constitute valid CBCL mes- (maxDepth ≤ 64, maxExpansionSize ≤ 8192 characters, sages: it has four constructors corresponding to simple verificationTime ≤ 1000 ms). The Lean 4 model uses a messages (with one of the eight core performatives), meta fuel parameter: boundedEvalFull decrements a naturalmessages, lang-scoped dialect invocations, and wrapped number counter at each expansion step, returning none

The S-expression parser uses recursive descent with a fuel parameter for termination. The fuel is set to |s| × 4 + 1, where |s| is the input length in characters. The multiplier 4 reflects the worst-case fuel consumption per input character: a single character can trigger up to four recursive steps (entering a list, attempting to parse an element, consuming the closing delimiter, and returning the result). The +1 ensures termination on empty input. This bound is sufficient for all inputs; the Lean proof of Theorem 1 confirms that parseSExpr never exhausts fuel. The fuel parameter is retained in the extracted cbcl-parse binary. The fuel value is computed at runtime from the input length, so the executable faithfully mirrors the verified model with no gap between proof and implementation. The top-level parser also rejects trailing input and unterminated strings.

Error fail 3. Verify R1–R3 + signature

4. Install dialect

meta

1. Parse S-expression

2. Validate + classify

fail Error

simple / wrapped

6. Deliver to application layer

fail Error

lang 5. Expand template under resource ctx fail Error

Fig. 1. Message processing lifecycle. Steps 1–2 apply to all messages; the upper branch handles dialect definitions (meta), the lower branch handles dialect invocations (lang), and simple or wrapped messages proceed directly to delivery. Any step may reject with a well-typed error (Theorem 12).

when fuel reaches zero. The Rust implementation mirrors this for depth and size, adding a wall-clock timeout as defense-in-depth.

G. DCFL Preservation Argument

The central security property is that installing dialects does not push the recognized language beyond DCFL. We Theorem 8 (Bounded Evaluation). boundedEvalFull(fuel, e, rs) establish this through three steps: always terminates, producing either a result or none (re1) Base case. The core CBCL grammar is LR(1)source exhaustion). A depth-bounded invariant additionally parseable (indeed LL(1)), hence DCFL. rules out depth creep across nested expansions. 2) Extension step. A dialect adds finitely many Theorem 9. If verifyR2 (δ) = true, then δ’s declared extend clauses that introduce new performative bounds are within system limits. heads. All dialect invocations must appear inside a (lang name ...) wrapper. DCFLs are not closed E. R3: Core Preservation under union in general [33]; CBCL avoids this because the lang keyword followed by a unique dialect Constraint R3 prevents dialects from redefining the eight name forms a prefix-free partition: a deterministic core performatives. pushdown automaton (DPDA) [13] dispatches to Theorem 10 (Core Preservation). If verifyR3 (δ) = true, the appropriate subgrammar by consuming the lang then for all core performative names n, δ does not define n. tag and dialect name, with no additional lookahead beyond LR(1) required. R1 and R2 ensure template Theorem 11 (Installation Safety). Installing an R3-verified expansion terminates and is resource-bounded, but dialect into a well-formed agent preserves well-formedness. do not increase parsing power. 3) Inductive closure. Since each installation preserves F. Pipeline Totality DCFL membership, and the base grammar is DCFL, The Lean pipeline from parse → validate → verify the language remains DCFL after any finite sequence constraints (for define/define-dialect meta messages) of dialect installations. is formalized as runPipeline : String → PipelineResult. This argument is fully mechanized in Lean 4. Theorems 2– Theorem 12 (Pipeline Totality). For all inputs s, 3 establish parser correctness, 4–7 verify R1, 8–9 verify R2, runPipeline(s) returns a PipelineResult and never diverges. and 10–11 verify R3. The deterministic-union construction Theorem 13 (Pipeline Soundness). If runPipeline(s) = is proven by agentDetParser_agrees, which shows that success(m), then s parsed successfully, m satisfies the combined DPDA agrees with the boolean decider for ValidMsgGrammar, and m passes validation. If m is a agents with unique dialect names (namesUnique). The final define/define-dialect meta message, its dialect defi- theorem dcfl_preserved composes these results: installing nition passes R1–R3. a fresh R3-verified dialect preserves DCFL membership.

TABLE II Reference implementation crates (Rust). Crate

LOC Responsibility

cbcl-core 7,800 cbcl-parser 1,900 cbcl-cli 430 cbcl-ffi 430 cbcl-wasm 490

Agent, evaluator, R1–R3, gossip, canonical Recursive-descent S-expr & message parser Parse, verify, agent REPL, gossip simulation C FFI bindings via cbindgen WebAssembly bindings (optional JS interop)

V. Reference Implementation A. Architecture

TABLE III Lean 4 verification coverage. Component S-Expression types Parser Serializer Message parser R1 (no recursion) R2 (resource bounds) R3 (core preservation) Pipeline DCFL preservation Agent & dialect model Total

Thm. 2 26 51 9 13 6 4 6 50 9 176

Approach Structural induction Fuel-based, well-formedness Round-trip, SafeSymbol Soundness + completeness DFS sound. + complete. Depth-bounded evaluation Redefinition check Totality + composition Det. union + det. parser Installation + matching All machine-checked, zero sorry

The reference implementation is written in Rust (∼11,000 lines of library code) as a Cargo workspace of five crates (Table II). The core library (cbcl-core) forbids unsafe a 100-agent network achieves full coverage in ∼3 rounds. code and uses only alloc, making it suitable for no_std Receiving agents independently verify dialect constraints environments. An earlier GNU Guile Scheme prototype (R1–R3) and cryptographic signatures before installation. informed the design but is superseded by the Rust impleE. Canonical Serialization mentation. For cryptographic operations (signing, hashing), CBCL B. Dialect Verification Engine uses the canonical form of S-expressions specified in Upon receiving a dialect definition, the implementation RFC 9804 [14]. This encoding eliminates whitespace variexecutes: (1) R1 check: walk each template AST for ation and uses length-prefixed verbatim strings, ensuring self-references and reject if found; additionally reject that structurally identical messages produce identical byte mutual recursion by detecting cycles in the performative representations, a prerequisite for deterministic signature dependency graph; (2) R2 check: verify declared bounds verification. are within system limits; (3) R3 check: reject if any extend VI. Evaluation clause redefines a core performative; (4) Integrity check (optional): if a cryptographic signer is registered (via a A. Verification Coverage The Lean 4 formalization covers parsing, validation, Signer trait), verify the signature and content hash. The dialect parsing/verification for meta definitions, and a fuelprotocol is algorithm-agnostic; the signature algorithm is bounded evaluation model. Table III reports counts for the identified by the dialect’s metadata, allowing deployments core safety modules. to use Ed25519, ECDSA, or post-quantum schemes without The verified parser binary cbcl-parse is extracted from protocol changes. Only after all checks pass is the dialect 2 the Lean proofs and runs 17 built-in test cases covering all installed. Verification runs in O(|δ| ) time in the size of message types, including negative cases for trailing input the dialect definition. and unterminated strings. C. Runtime Resource Enforcement The Rust implementation includes property-based tests A ResourceContext struct tracks depth, cumulative (using proptest), differential tests that cross-check the expansion size, and elapsed wall-clock time during message Rust parser against the Lean-extracted binary, and five evaluation. Three checks enforce bounds: enter_depth cargo-fuzz targets covering the S-expression parser, mesincrements the depth counter and returns a resource-limit sage parser, dialect parser, constraint verification, and error if max_depth is exceeded; check_expansion_limit template expansion. Five example dialects (37 performaaccumulates expansion size; and check_time_limit com- tives total) have been verified against the implementation pares elapsed time against the timeout. These checks are (R1–R3 pass): precision agriculture (11 performatives), invoked at each step of template expansion, ensuring that AI planning (7), cross-chain asset transfer (7), artifact even adversarially crafted templates cannot exceed their management (7), and email use (5). declared resource bounds. B. Security Testing D. Epidemic Dialect Propagation We validate CBCL’s security properties against concrete attack scenarios: Dialects propagate between agents via an epidemic (gossip) protocol. In a fully-connected topology, classic Recursive expansion attack. A malicious dialect conepidemic dissemination analysis [27] yields convergence to taining (extend bomb (x) (bomb (bomb x))) is rejected full coverage in O(log n) rounds; CBCL builds on this result. at R1 verification; the self-reference is detected before instalWith transmission probability p = 0.8, empirical testing lation. Mutual recursion (e.g., ping expands to pong, pong with networks of 10–500 agents matches the O(log n) bound; expands to ping) is also rejected by the implementation.

parser differential vulnerabilities that arise when different implementations interpret the same message differently, a problem endemic to protocols with ambiguous gramOperation Median time mars or natural language content. Canonical serialization Parse simple tell message 78 ns (Section V-E) further reduces—but cannot fully eliminate— Parse meta define 125 ns implementation-level divergence in areas such as Unicode Parse lang dialect invocation 130 ns handling. Pipeline: simple tell (end-to-end) 386 ns Pipeline: meta define (end-to-end) 1.03 µs Explicit computational complexity. Every dialect Template expansion (conditional) 215 ns declares its resource requirements, and evaluation is guaranR1 verify full dialect 1.83 µs R2 bounded eval (nested) 185 ns teed to terminate within those bounds. An implementation R3 verify dialect 21 ns can decide before evaluation whether a dialect’s demands Gossip: 100-agent convergence 2.6 ms are acceptable, yielding explicit worst-case resource budgets. This transforms resource governance from a runtime Depth bomb. A deeply nested message (lang d1 (lang emergency into a design-time contract. d2 (lang d3 ...))) exceeding max-depth triggers re- No parser- or expander-induced weird machines. source exhaustion at the enforced limit, returning an error The restriction to declarative pattern-template expansion with bounded resources means that the CBCL parser and rather than consuming unbounded stack. Core redefinition. A dialect attempting (extend tell template expander introduce no unintended computational (x) (drop-table x)) is rejected at R3 verification; tell artifacts. The template language is not Turing-complete; its semantics are fully determined by a finite substitution table. is a core performative and cannot be redefined. Weird machines could still arise in layers outside CBCL’s Expansion bomb. A template producing output larger scope (e.g., tool backends or agent action semantics); than max-expansion-size is halted mid-expansion when CBCL’s guarantee is that the message recognition and the cumulative size check fires. expansion pipeline itself is free of them. In all cases, the parser returns a well-typed error value B. Comparison with Contemporary Agent Protocols rather than entering an undefined state. This is the The Model Context Protocol (MCP) [7] and similar practical consequence of DCFL preservation: the parser is deterministic and total, always terminating with a definite LLM agent frameworks use JSON-RPC with unrestricted schemas. While practical, this design creates an input accept or reject. language whose computational complexity depends on C. Performance the tools agents invoke, potentially reaching TuringTable IV reports Criterion benchmark results for the completeness when they can execute arbitrary code in Rust implementation on an Apple M4 (macOS 15). The end- response to messages. CBCL demonstrates that meaningful to-end pipeline (parse → validate → verify) processes a sim- extensibility does not require unbounded input complexity. KQML [3] and FIPA-ACL [6] have parseable grammars ple tell message in under 400 ns and a meta define (including R1–R3 verification) in ∼1 µs. Template expansion and limited extensibility (KQML’s performative set was completes in 120–350 ns depending on template complexity. explicitly open; FIPA-ACL supported user-defined message Constraint verification is dominated by R1 (dependency- parameters), but extensions were unconstrained by formal graph cycle detection, ∼1.8 µs for a full dialect); R2 and R3 safety guarantees and required out-of-band agreement. checks complete in under 25 ns each. Gossip simulation of CBCL inherits their grammar tractability while adding a 100-agent fully-connected network converges in ∼2.6 ms. formally safe runtime evolution. These numbers indicate that CBCL’s safety checks impose C. Implementation Strategy negligible overhead relative to typical network round-trip The Lean 4 formalization and the Rust implementation times. serve complementary roles. Lean provides machine-checked proofs of the safety properties (Theorems 1–13) and yields VII. Discussion an extracted parser binary (cbcl-parse) that is correct by A. Relation to LangSec Principles construction. However, extracted code optimizes for proof Verifiable parsers. The Lean 4 formalization produces a structure, not for runtime performance or integration. The parser with machine-checked soundness and completeness Rust implementation (cbcl-rs) provides a productiontheorems. The extracted binary constitutes a verified quality library with O(n) hand-rolled parsing, C FFI and recognizer for the CBCL language. WebAssembly bindings, property-based and differential Parser equivalence. Because CBCL specifies a single testing, and fuzz targets—capabilities that are essential unambiguous grammar that is LR(1)-parseable (and indeed for adoption but outside the scope of formal verification. LL(1)), all conformant parsers produce identical parse The two implementations are cross-validated: the Rust trees for every input. This eliminates the grammar-level parser’s test suite includes differential tests against the TABLE IV Benchmark results (Rust, Apple M4).

Lean-extracted binary, ensuring that both accept and reject the same inputs. D. Toward Semantic Guidance CBCL guarantees syntactic safety but not semantic agreement. Several mechanisms could narrow this gap, with different complexity implications. Examples (supported via :examples in dialect definitions) and typed parameter declarations add no formal complexity and remain within DCFL. Interaction protocol state machines (e.g., after ask, expect reply) are regular, well below DCFL. Pre/postconditions and ontological commitment [12] risk crossing the complexity boundary CBCL is designed to enforce, and would need to be scoped carefully or relegated to an application layer above the protocol. The :examples clause offers a machinecheckable anchor: a receiving agent should expand each example input through its own expander and compare the result against the expected output before claiming dialect support. This catches the most common interoperability failures (template misconfiguration, parameter-type disagreement) before they manifest at runtime, though it cannot detect deeper semantic divergence. Following Singh [19], CBCL treats dialect installation as a public commitment to the dialect’s declared semantics; semantic divergence is thus a breach of commitment, observable and accountable, rather than a hidden failure of shared mental state. We are investigating structural contracts that extend CBCL’s syntactic safety toward protocol correctness while remaining within DCFL and requiring no coordination. Protocol constraints are expressed as causal dependency graphs over performative types; each message carries an explicit causal reference (a content hash of its predecessor’s canonical serialisation), forming a Merkle DAG that is cryptographically tamper-evident and independently verifiable. Verification is a monotonic predicate on the append-only message store, coordinationfree by the CALM theorem [34]. Message shape constraints are expressed as visibly pushdown languages [32] over expanded S-expressions, exploiting the decidable inclusion checking that VPLs provide. The full design is implemented in cbcl-rs and will be described in a forthcoming report. E. Limitations Expressiveness ceiling. DCFL restriction means some patterns cannot be expressed in dialect templates. Concrete examples of inexpressible patterns include: (1) recursive data transformations such as flattening a nested list of arbitrary depth; (2) cross-field references where one parameter’s value depends on another parameter’s content (e.g., a checksum computed over other fields); (3) iteration or aggregation over variable-length collections (e.g., summing line items in an invoice); and (4) context-sensitive validation such as ensuring a reply’s thread ID matches an earlier message. In Standish’s extensibility taxonomy [31], CBCL restricts itself to paraphrastic extension (defining new constructs in terms of existing ones), deliberately

excluding orthophrase (adding orthogonal features) and metaphrase (altering interpretation rules). This ceiling is a deliberate trade-off: it exists precisely to bound the attack surface. Agents requiring these patterns must implement them in application logic outside the CBCL layer. Trust infrastructure. CBCL specifies algorithmagnostic dialect signing (via an abstract Signer interface) but does not define key distribution, certificate authorities, or revocation. These are left to deployment infrastructure. Dialect identity and naming. The DCFL preservation proof (dcfl_preserved) requires unique dialect names per agent (namesUnique), since the lang tag dispatches by name. The true identity of a dialect is the content hash of its canonical encoding (RFC 9804); two dialects with the same name but different hashes are rejected at installation, mitigating name collisions and downgrade attempts. Dialect churn is bounded by R2 resource limits but requires deployment-level rate limiting for full mitigation. Dialect quality and bloat. CBCL constrains dialect safety but not dialect quality. Nothing prevents propagation of redundant or poorly designed dialects. Agents can uninstall unhelpful dialects, but the protocol does not define curation mechanisms, leaving lifecycle management to agent policy. Performance. The fuel-based termination model in the Lean formalization is sound but conservative. The reference implementation’s runtime resource enforcement adds overhead proportional to the number of expansion steps. VIII. Related Work A. Language-Theoretic Security Sassaman et al. [1] established the foundation for language-theoretic security, observing that mismatch between an input language’s complexity and the parser’s recognizer class raises the likelihood of exploitable errors, and that unanticipated computational artifacts (“weird machines”) arise when input handling violates designer assumptions. Kaminsky, Patterson, and Sassaman [16] demonstrated this concretely with parser differential attacks against the X.509 PKI infrastructure. Sassaman et al. [17] extended the analysis to network stacks, framing protocol insecurity as instances of the halting problem. Momot et al. [15] developed a taxonomy of LangSec errors and proposed actionable CWE refactorings to address them. CBCL is, to our knowledge, the first protocol designed from the ground up on these principles for agent communication, and the first to demonstrate that LangSec constraints are compatible with runtime language self-extension. Von Hippel and Miyazono [28] argue that AI security is fundamentally a LangSec problem, identifying structured output parsing and tool-use capabilities in LLM-based systems as key attack surfaces. Their analysis reinforces the premise underlying CBCL: that securing agent communication requires constraining the computational complexity

of the input language, not merely adding ad-hoc validation layers. Fazeldehkordi et al. [18] demonstrated that unconstrained communication patterns between distributed financial agents can enable DDoS through call-based flooding cycles, using static analysis to detect these patterns at design time. CBCL addresses a related concern at the protocol layer: R2 resource bounds ensure that processing any message, including dialect expansion, terminates within declared limits. B. Agent Communication Languages

verification, addresses this root cause by making provenance syntactically explicit. Zhou et al. [24] show that projecting high-dimensional LLM states to natural-language tokens is many-to-one and non-invertible, compounding information loss across conversational turns. A decidable formal language avoids this lossy bottleneck by making coordination semantics explicit in the message structure. Borazjanizadeh and Piantadosi [25] provide complementary evidence. Pairing LLMs with a formal symbolic engine (Prolog) outperforms pure natural-language chain-of-thought on deductive tasks, suggesting that structured representations improve multi-step reasoning.

KQML [3] introduced speech-act performatives for agent communication; FIPA-ACL [6] later codified 22 perfor- C. Language Extensibility and Formal Methods matives with mental-state semantics. Both supported McCarthy’s 1982 proposal [9] envisioned open-ended extensibility: KQML through an explicitly open perfor- business communication. Flatt [11] showed how language mative set (communities could define new performatives by extensibility can be systematized through first-class lanagreement), FIPA-ACL through X- prefixed user-defined guage definitions in Racket. CBCL adapts this principle for message parameters. Gruber’s Ontolingua [12] addressed adversarial distributed environments and makes the safety the content layer separately. Building on McCarthy and constraints explicit. Hayes’s [8] principle that what is represented can be speciDemers et al. [27] established the O(log n) convergence fied independently of how it is computed, Gruber showed bound for epidemic information dissemination, which that interoperability between heterogeneous agents requires underlies CBCL’s dialect propagation protocol. Jelasity et formal ontological commitment: each agent must commit al. [26] developed theoretical foundations for gossip-based to the declarative specification of shared concepts (classes, aggregation, proving that the per-round convergence factor relations, and the axioms constraining their use), with no is independent of network size; their gossip framework commitment to the form or content of knowledge internal informs CBCL’s peer-selection strategy. RFC 9804 [14] to the agent. CBCL’s dialect mechanism inherits this comspecifies a canonical form for S-expressions used in CBCL mitment architecture; a dialect definition is a declarative for deterministic signature verification. specification to which the installing agent publicly binds itself, independent of its internal representation. Gruber IX. Conclusion left the process of reaching consensus on shared ontologies CBCL demonstrates that the LangSec principle of matchas an open problem, and treated ontology specification as separable from the communication protocol, so that ing input language complexity to recognizer capability can extending shared meaning required out-of-band agreement be applied even to self-extending protocols. By constraining invisible to protocol-level safety analysis. CBCL addresses dialect definitions to declarative pattern-template substituthe consensus problem directly: agents propose, query, and tions within S-expression syntax, we show that meaningful adopt dialect definitions as ordinary protocol messages. runtime extensibility and provable parsing safety are not in Singh [19] identified a complementary flaw: reliance on conflict. Because safety constraints are machine-checked at unverifiable mental states rather than observable social installation, agents can create and adopt dialects ad hoc, commitments. CBCL makes dialect installation a protocol- without external coordination. level action subject to machine-checked safety constraints. As autonomous agent systems proliferate, the choice Yang et al. [21] survey AI agent protocols across seven of communication substrate becomes a security decision. evaluation dimensions. Deng et al. [22] survey security Natural language and unrestricted schemas offer maximal threats to AI agents, organising them around prompt injec- flexibility but cannot guarantee that two agents interpret tion, tool-use risks, and adversarial multi-agent interactions. the same message identically, a source of coordination CBCL’s DCFL constraint directly addresses the parser- failure even among cooperative agents and a fundamentally level attack surface underlying prompt injection: because unsecurable attack surface in adversarial settings. CBCL dialect extensions are structurally distinct from message offers an alternative: a formally specified, machine-verified content, an agent’s parser never conflates instructions with protocol where every message, including those that extend data. Zhang et al. [23] demonstrate this concretely: their the language itself, is parsed in bounded time by a ClawWorm worm achieves a 64.5% attack success rate deterministic pushdown automaton. If agents communicate against the OpenClaw framework by exploiting a flat in languages whose validity is undecidable, no monitor can context trust model in which LLMs cannot distinguish reliably determine what they have agreed to do. Formally owner instructions from arbitrary channel input. CBCL’s bounding what agents can express to each other is a lang-scoped dialect mechanism, combined with R1–R3 precondition for oversight.

Availability. The reference implementation, Lean 4 formalization, verified parser binary, and IETF Internet-Draft are available at https://codeberg.org/anuna/cbcl-rs under the Apache 2.0 license. The Nostr transport binding is at https://codeberg.org/anuna/cbcl-nostr. Acknowledgments Thanks to Claire Barnes, David Factor, Mat Mytka, Mark Pesce, Marc Ahrens, Prof. Ingo Weber, Dr Max Ott, Dr Mark Staples, Dr Ho-Pun Lam, Dr Adnene Guabtni, and DZJ for helpful discussions. Thanks to Ric Richardson and the Office for Innovation for championing this effort. This work was inspired by problems encountered during a Science and Industry Endowment Fund project through CSIRO’s Data61, and the need for ad-hoc knowledge sharing across agricultural supply networks. AI Disclosure. In accordance with IEEE policy, the author discloses that AI assistants were used throughout this work, including drafting and editing this manuscript, assisting with the Lean 4 formalization, contributing to the reference implementation, and aiding in literature review. Tools used include llm-md, Anthropic’s Claude Code, and OpenAI’s Codex. Agent orchestration was coordinated using hence, the author’s defeasible-logic meta-control planner for multi-agent LLM task coordination. All work was directed, reviewed, and validated by the author. The author takes full responsibility for the content of this publication. References [1] L. Sassaman, M. L. Patterson, S. Bratus, and M. E. Locasto, “Security applications of formal language theory,” IEEE Systems Journal, vol. 7, no. 3, pp. 489–500, Sep. 2013. [2] S. Bratus, M. E. Locasto, M. L. Patterson, L. Sassaman, and A. Shubina, “Exploit programming: From buffer overflows to ‘weird machines’ and theory of computation,” ;login: USENIX Magazine, vol. 36, no. 6, Dec. 2011. [3] T. Finin, R. Fritzson, D. McKay, and R. McEntire, “KQML as an agent communication language,” in Proc. 3rd Int. Conf. on Information and Knowledge Management, pp. 456–463, 1994. [4] M. T. Kone, A. Shimazu, and T. Nakajima, “The state of the art in agent communication languages,” Knowledge and Information Systems, vol. 2, no. 3, pp. 259–284, 2000. [5] B. Chaib-draa and F. Dignum, “Trends in agent communication language,” Computational Intelligence, vol. 18, no. 2, pp. 89–101, 2002. [6] Foundation for Intelligent Physical Agents, “FIPA ACL specifications,” 2002. [Online]. Available: https://web.archive.org/web/ 2023/http://www.fipa.org/repository/aclspecs.html [7] Anthropic, “Model Context Protocol specification,” 2025. [Online]. Available: https://modelcontextprotocol.io/specification/ 2025-03-26 [8] J. McCarthy and P. J. Hayes, “Some philosophical problems from the standpoint of artificial intelligence,” in Machine Intelligence 4 (B. Meltzer and D. Michie, eds.), pp. 463–502, Edinburgh University Press, 1969. [9] J. McCarthy, “Common business communication language,” in Textverarbeitung und Bürosysteme (A. Endres and J. Reetz, eds.), R. Oldenbourg Verlag, 1982. [Online]. Available: https: //www-formal.stanford.edu/jmc/cbcl2.pdf [10] H. O’Connor, “CBCL: A self-extensible agent communication language,” Internet-Draft draft-cbcl-00, 2025. [11] M. Flatt, “Creating languages in Racket,” Communications of the ACM, vol. 55, no. 1, pp. 48–56, 2012.

[12] T. R. Gruber, “A translation approach to portable ontology specifications,” Knowledge Acquisition, vol. 5, no. 2, pp. 199–220, 1993. [13] J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed. Pearson, 2006. [14] R. L. Rivest and D. E. Eastlake 3rd, “Simple Public Key Infrastructure (SPKI) S-expressions,” RFC 9804, 2025. [15] F. Momot, S. Bratus, S. M. Hallberg, and M. L. Patterson, “The seven turrets of Babel: A taxonomy of LangSec errors and how to expunge them,” in Proc. IEEE Cybersecurity Development (SecDev), pp. 45–52, 2016. [16] D. Kaminsky, M. L. Patterson, and L. Sassaman, “PKI layer cake: New collision attacks against the global X.509 infrastructure,” in Financial Cryptography and Data Security, vol. 6052, pp. 289– 303, 2010. [17] L. Sassaman, M. L. Patterson, S. Bratus, and A. Shubina, “The halting problems of network stack insecurity,” ;login: USENIX Magazine, vol. 36, no. 6, 2011. [18] E. Fazeldehkordi, O. Owe, and T. Ramezanifarkhani, “A language-based approach to prevent DDoS attacks in distributed financial agent systems,” in Computer Security, vol. 11981, pp. 258–277, 2020. [19] M. P. Singh, “Agent communication languages: Rethinking the principles,” Computer, vol. 31, no. 12, pp. 40–47, 1998. [20] F. Zambonelli, N. Bicocchi, G. Cabri, L. Leonardi, and M. Puviani, “On self-adaptation, self-expression, and self-awareness in autonomic service component ensembles,” in Proc. IEEE 5th Conf. on Self-Adaptive and Self-Organizing Systems Workshops (SASOW), pp. 108–113, 2011. [21] Y. Yang et al., “A survey of AI agent protocols,” arXiv:2504.16736, 2025. [22] Z. Deng et al., “AI agents under threat: A survey of key security challenges and future pathways,” ACM Computing Surveys, vol. 57, no. 7, pp. 1–36, 2025. [23] Y. Zhang et al., “ClawWorm: Self-propagating attacks across LLM agent ecosystems,” arXiv:2603.15727, 2026. [24] P. Zhou, Y. Feng, H. Julaiti, and Z. Yang, “Why do AI agents communicate in human language?” arXiv:2506.02739, 2025. [25] N. Borazjanizadeh and S. T. Piantadosi, “Reliable reasoning beyond natural language,” arXiv:2407.11373, 2024. [26] M. Jelasity, A. Montresor, and O. Babaoglu, “Gossip-based aggregation in large dynamic networks,” ACM Trans. Comput. Syst., vol. 23, no. 3, pp. 219–252, 2005. [27] A. Demers et al., “Epidemic algorithms for replicated database maintenance,” in Proc. 6th ACM Symp. on Principles of Distributed Computing (PODC), pp. 1–12, 1987. [28] M. Von Hippel and E. Miyazono, “Research report: AI security is a LangSec problem,” in Proc. IEEE Security and Privacy Workshops (SPW), pp. 73–78, 2025. [29] N. Chomsky, “Three models for the description of language,” IRE Transactions on Information Theory, vol. 2, no. 3, pp. 113–124, 1956. [30] Fiatjaf, “Nostr: Notes and Other Stuff Transmitted by Relays (NIP-01),” 2020. [Online]. Available: https://github.com/ nostr-protocol/nips/blob/master/01.md [31] T. A. Standish, “Extensibility in programming language design,” in Proc. National Computer Conference and Exposition, pp. 287– 290, 1975. [32] R. Alur and P. Madhusudan, “Visibly pushdown languages,” in Proc. 36th ACM Symp. on Theory of Computing (STOC), pp. 202–211, 2004. [33] S. Ginsburg and S. Greibach, “Deterministic context free languages,” Information and Control, vol. 9, no. 6, pp. 620–648, 1966. [34] J. M. Hellerstein and P. Alvaro, “Keeping CALM: When distributed consistency is easy,” Communications of the ACM, vol. 63, no. 9, pp. 72–81, 2020.