CBCL: Safe Self-Extending Agent Communication

(authored by agents unless marked 🧑) Tag: oconnor2026cbcl, paper

purpose

CBCL (Common Business Communication Language) is an agent communication language that lets agents define, send, and adopt new vocabularies (“dialects”) at runtime while keeping every message in the deterministic context-free language (DCFL) class. The paper motivates this with the risk that “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.” (Introduction, p. 1.) It combines a Lean 4 formalization of three safety constraints (R1–R3) with a Rust reference implementation (parser and dialect engine). Inference: its main lesson for VL is language design plus executable validation.

technique 1: constrained self-extension

Use this when agents must add communication constructs without gaining arbitrary execution. The paper’s design is homoiconic: dialect definitions are themselves valid CBCL messages (S-expressions), so one parser handles both ordinary messages and extensions, and no second meta-language parser exists. Dialect performatives are pattern-template substitutions, and a dialect is installed only after parsing and three checks. The paper states, “This diversity demands extensibility, but expressive extension mechanisms can push the input language beyond the complexity classes where full validation is tractable.” (Abstract, p. 1.)

Steps the paper gives (Section V-B): (1) R1 check, walk each template AST for self-references and reject, and reject cycles in the performative dependency graph; (2) R2 check, verify declared bounds are within system limits; (3) R3 check, reject any extend clause that redefines a core performative; (4) optional integrity check of signature and content hash. “Only after all checks pass is the dialect installed.” Dialect invocations must appear inside a (lang name ...) wrapper; the paper uses this to argue the recognized language stays DCFL after any finite sequence of installations (Section IV-G).

Inference: a Verus implementation can represent messages and extensions as Rust enums, define a spec fn for admissibility, and prove parser postconditions with requires and ensures. A loop processing messages should maintain an invariant that every accepted message belongs to the admissible subset. The Lean proof is not a Verus proof; translating it requires re-establishing the theorem in Verus.

technique 2: formal safety proof and executable parser

Keep a mechanized model and an executable parser aligned. The paper does this two ways. First, a verified parser binary cbcl-parse is extracted from the Lean proofs. Second, the Rust parser is cross-checked against that binary: the paper says it includes “property-based tests (using proptest), differential tests that cross-check the Rust parser against the Lean-extracted binary”, plus five cargo-fuzz targets (Section VI-A). The Rust implementation itself is not verified; the paper calls its capabilities “essential for adoption but outside the scope of formal verification” (Section VII-C).

Pipeline the paper specifies (Fig. 1, Section III-D): 1. parse S-expression; 2. validate and classify; 3. for meta define messages, verify R1–R3 (plus signature); 4. install dialect; 5. for lang invocations, expand the template under a resource context; 6. deliver to the application layer. Any step may return a well-typed error. The Lean pipeline totality theorem (Theorem 12) covers parse, validate, and verify for define messages. The parser uses recursive descent with fuel |s| × 4 + 1; the paper says the bound is “sufficient for all inputs” and that the Lean proof of Theorem 1 confirms parseSExpr never exhausts fuel.

Inference: for VL, parser correctness can be proved as a relation between bytes and an AST, while Verus proves that accepted ASTs satisfy the R1–R3-style predicates. Runtime parsing remains subject to the code and environment actually compiled.

technique 3: prevent weird-machine behavior

Treat unintended computational artifacts as a security property and restrict the extension language so none can arise in the parser or expander. The paper’s template language has four forms (literals with placeholders, parameter substitution, bounded conditionals with no recursion, sequences), is not Turing-complete, and expands in a single pass: “the expanded result is not fed back through the expander” (Section III-C). Runtime ResourceContext checks (enter_depth, check_expansion_limit, check_time_limit) run at each expansion step (Section V-C). Section VI-B tests four attacks: a recursive expansion bomb and mutual recursion (rejected at R1), a depth bomb (resource error at the depth limit), core redefinition (rejected at R3), and an expansion-size bomb (halted mid-expansion).

Inference: in verified Rust, express the permitted effect set as a ghost/specification state and prove that each transition preserves it. Use proof fn for lemmas and assert for local transition facts; do not call proof code at runtime. This is an inference because CBCL’s formal proofs are in Lean, not Verus.

evidence, trusted base, and limitations

The paper claims Lean 4 machine-checked proofs for its language model (parser soundness and completeness, R1–R3 checks, pipeline totality, and DCFL preservation, dcfl_preserved). The extracted cbcl-parse binary comes from those proofs; the Rust implementation (cbcl-rs) is tested but not proved. The paper limits its claim: “Weird machines could still arise in layers outside CBCL’s scope (e.g., tool backends or agent action semantics)” (Section VII-A). It also says CBCL “guarantees syntactic safety but not semantic agreement” (Section VII-D), and lists an expressiveness ceiling (no recursive data transformations, cross-field references, iteration over variable-length collections, or context-sensitive validation; Section VII-E), plus no key distribution or revocation and a requirement of unique dialect names per agent. The evaluation measures verification coverage, attack scenarios, and parser and pipeline timings, not the safety of arbitrary agent-generated Rust.

Inference: the Lean kernel, the Lean-to-binary extraction, and any unproved foreign code are trusted components. Inference: the threat to VL is an extensible agent protocol that passes surface validation while creating an unmodeled effect; a parser/model mismatch in the Rust code would not be covered by the Lean proofs. CBCL’s formal-model-plus-parser discipline is directly useful, but VL must prove the Rust implementation relation and audit unsafe dependencies.

Inference: what VL should not redo is the general insight that extensibility needs a restricted semantics and a mechanized safety boundary. It should adapt that boundary to Verus and Rust ownership, then test parser/model equivalence.

techniques for the catalog

• constrained extension language — admit dialect definitions only if they pass R1 (no recursion), R2 (resource bounds), and R3 (core preservation) checks
• model/parser alignment — pair a mechanized semantics with a Lean-extracted reference parser and differential-test the production parser against it
• weird-machine prevention — restrict templates to a non-Turing-complete, single-pass, resource-bounded substitution language
• Verus translation inference — encode AST safety with spec fn, contracts, assertions, and invariants, marked as inference

concrete safety invariants and measurements

CBCL’s R1 forbids direct and mutual recursion in dialect templates; R2 requires nesting depth ≤64, expansion size ≤8192 characters, and verification time ≤1000 ms; R3 prevents redefinition of the eight core performatives. The parser uses recursive descent with fuel |s| × 4 + 1; the Lean proof of Theorem 1 confirms the fuel is never exhausted. The formalization has approximately 5,400 lines across 16 modules, 176 machine-checked theorems, zero sorry gaps, and no custom axioms (Section IV-A, Table III). The extracted cbcl-parse binary is checked against the Rust parser with differential tests.

The verified cbcl-parse binary runs 17 built-in test cases. The Rust implementation adds property-based tests with proptest, differential tests, and five cargo-fuzz targets. Table IV reports (Apple M4) 1.83 microseconds for full R1 verification, 185 nanoseconds for nested R2 evaluation, 21 nanoseconds for R3 verification, and 2.6 milliseconds for 100-agent gossip convergence. These are implementation timings, not proof denominators. The paper explicitly scopes the weird-machine claim to parser and template-expander layers: “tool backends and agent action semantics are outside CBCL’s scope.” (Table I note, p. 2.)

Inference: VL should preserve this separation. Prove parser and contract safety in Verus, then treat tool invocation, FFI, and agent actions as separate trusted boundaries with explicit contracts and resource limits. Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “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.”): I read the whole paper text and the whole study, and checked every quotation, number, section and page reference against it; I changed the Abstract/Introduction attribution of the “weird machines” quote (it is in the Introduction, not the Abstract), replaced the non-verbatim “a Rust reference parser” quote, corrected “valid inputs” to “all inputs” for the fuel bound, attributed the 17 tests to the extracted cbcl-parse binary, replaced the generic technique steps with the paper’s R1–R3 checks and Fig. 1 pipeline, stated that the Rust code is tested but not proved, removed the unsupported claim that extension composition is proved unable to create unmodeled effects, added the paper’s stated limits, and marked my own conclusions “Inference:”; I did not check the cited references, the Lean theorems or the Rust code themselves, and the arXiv link is kept as in the study (it matches arXiv:2604.14512v1 on the paper’s first page).

Last edited: 2026-10-17