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.

翻译：摘要：智能体通信语言（ACLs）使得异构智能体能够在不同领域间共享知识和协调。这种多样性要求可扩展性，但表达性强的扩展机制可能将输入语言推至完全验证难以处理的复杂性类。我们提出CBCL（通用商务通信语言），这是一种将包括运行时语言扩展在内的所有消息约束在确定性上下文无关语言（DCFL）类别内的智能体通信语言。CBCL允许智能体将领域特定的“方言”扩展定义、传输并采用为头等消息；三个安全不变量（R1—R3）——在Lean 4中通过机器检验并在Rust参考实现中强制实施——可防止无界扩展、应用声明的资源限制并保留核心词汇。我们在Lean 4中形式化该语言及其安全属性，在Rust中实现带有基于属性和差分测试的参考解析器与方言引擎，并提取出一个经过验证的解析器二进制文件。我们的结果表明，其中扩展定义与普通消息共享相同表示的同音形协议设计能够被证明是安全的。随着自主智能体越来越多地扩展自身的通信能力，形式上限制它们彼此之间的表达内容是进行监督的先决条件。