← All papers
First page of CBCL: Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication

Hugo O'Connor

cs.CR Apr 16, 2026 · v1
Three CBCL safety invariants machine-checked in Lean 4 (with a verified Rust parser).
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.

Agent communication languages must be extensible to support diverse domains, but expressive extension mechanisms can push input languages beyond complexity classes where full validation is tractable, creating security vulnerabilities including stack-bombing and Turing-complete payloads.

The authors present CBCL (Common Business Communication Language), which constrains all messages, including runtime dialect extensions, to the deterministic context-free language (DCFL) class. Agents can define, transmit, and adopt domain-specific dialect extensions as first-class protocol objects while maintaining O(n) parsing with no backtracking. Safety properties (no recursion, no weird machines, completeness) are formally verified in Lean 4 using structural induction and fuel-bounded evaluation models.

The Lean 4 formalization covers parsing, validation, dialect verification, and a fuel-bounded evaluation model with 101 verified theorems across core modules (S-Expression types, parser, serializer, message parser, R1-R3 safety properties). The implementation totals approximately 11,050 lines of Rust across five crates. CBCL achieves DCFL complexity with full extensibility verification while existing protocols (KQML, FIPA-ACL, MCP) permit CFL or RE complexity.