cbcl — an agent communication language you can formally verify

The problem

Agent communication chose between frozen and unsafe. Neither works.

Early agent communication languages (KQML, FIPA-ACL) shipped a fixed vocabulary. Evolving it required out-of-band agreement. Modern systems went the other way — agents exchange JSON or natural language — and collapsed every formal guarantee in the process.

What the field has today

FIPA-ACL — fixed performatives, rigorous semantics, impossible to extend without a standards body.

JSON over HTTP — unrestricted input, parser differentials, no semantic contract, no safety argument. Every endpoint is a weird-machine.

"Natural language" protocols — an LLM prompt you hope the other agent understands the same way. No decidability, no compositionality, no proof.

What cbcl gives you

Eight core performatives — tell, ask, reply, hello, bye, ok, error, cancel — formally specified and preserved under all extensions.

Runtime dialect definition — agents exchange pattern-template S-expressions to add domain vocabulary. Resource-bounded; core-preserving.

Formal proofs in Lean 4 — 176 machine-checked theorems, 0 sorries, 0 axioms. dcfl_preserved theorem: installing any R1–R3-verified dialect keeps the language in DCFL.

See it work

From an s-expression to a formally verified dialect.

Two agents. Eight performatives. One new dialect, defined at runtime, verified at admission.

Core vocabulary

Eight performatives. S-expressions. O(n) parse.

Define a dialect

Pattern / template with resource limits.

Verify admission

R1–R3 for DCFL safety, plus optional R4 signature.

Teach a peer

Dialect transmitted by tell, admitted by peer.

The Lean proofs

176 theorems, 0 sorries, verified parser extracted.

cbcl · agent-a ↔ agent-b

; eight core performatives

(hello  agent-a agent-b)
(tell   agent-b "sky is blue")
(ask    agent-b "colour-of sky")
(reply  agent-a "blue")
(ok     msg-42)
(error  msg-43 "dialect not admitted")
(cancel msg-44)
(bye    agent-b)

$ cbcl parse '(tell agent-b "sky is blue")'
✓ well-formed, DCFL, core performative   O(n) · linear-time

; a planning dialect, defined at runtime

(define planning ()  "@anuna"
  (extend propose (?agent ?action ?time)
    (tell ?agent
      ("propose" ?action ?time)))
  (:resource-requirements
    ((:max-depth             8)
     (:max-expansion-size   512)
     (:verification-time-ms  10))))

# An extend clause is a pattern/template rewrite.
# No recursion. Resource bounds are part of the dialect itself.

$ cbcl verify planning.scm

admission check (Lean-verified)

   ✓ R1 — no recursion               pattern head ≠ template tokens
   ✓ R2 — resource bounded           depth=8, expansion=512, time=10ms
   ✓ R3 — core preserving            no shadowing of 8 core verbs
   ✓ R4 — signature                  unsigned accepted; invalid rejected

admitted. language class after extension: DCFL
          parser complexity: O(n)

# If any rule fails, the dialect is rejected.
# The check itself is decidable — bounded in |δ|² by construction.

agent-a  (tell agent-b
             (meta (define planning …)))

agent-b  admission:  ✓ R1–R3 pass · signature verified
         installed:   dialect planning

agent-a  (propose agent-b deploy-v2 2026-04-20)
agent-b  (reply agent-a (ok deploy-v2))

# Peer-to-peer dialect exchange, no central registry.
# Both agents converge on the same language, provably.

$ lake build

LeanCbcl.SExpr / Message / Dialect    ✓
LeanCbcl.Parser / DetParser           ✓
LeanCbcl.R1NoRecursion                ✓
LeanCbcl.R2ResourceBounds             ✓
LeanCbcl.R3CorePreservation           ✓
LeanCbcl.Pipeline / TemplateExpansion ✓

total: 176 theorems · 0 sorries · 0 axioms

$ lake exe cbcl-parse # verified binary extracted from Lean
17 built-in test cases passed

$ cargo test --workspace
833 passed; 19 proptests; 0 failures

$ cargo test -p cbcl-parser --test differential
Rust ≡ Lean  on shared test vectors

Why cbcl

Three properties no other agent language has together.

01 · Small core

Eight verbs, no more.

Every cbcl interaction reduces to one of eight performatives with a formal meaning. New vocabulary is a dialect over these; it never touches the core. The core is a fixed point.

hello, bye — session control
tell, ask, reply — content exchange
ok, error, cancel — coordination
S-expression syntax, no ambiguity
Core provably preserved under all dialects

02 · DCFL

Goldilocks grammar.

Deterministic context-free is the largest class where parsing is decidable in linear time. Unbounded grammars raise parsing to NP or worse and breed weird-machines. cbcl stays in DCFL — by construction, and by proof.

O(n) parse time, linear in input
No parser differentials — one canonical parser
LangSec by construction
No recursion in dialect templates
Resource limits per dialect

03 · Lean-verified

The proofs are code.

176 machine-checked theorems in Lean 4 prove parser soundness and completeness, R1–R3 verification, pipeline totality, and DCFL preservation under dialect installation. A verified parser binary is extracted from the proofs; a differential harness cross-checks the Rust implementation against it.

Lean 4 proofs — 0 sorries
833 Rust tests, 19 property tests
Rust ↔ Lean differential fuzzing
WASM + C FFI for embedding
Apache-2.0

How it works

A small core. A bounded extension mechanism. A formal guarantee.

Dialects are pattern-template rewrites checked against three safety rules (R1 no-recursion, R2 resource-bounded, R3 core-preserving) at admission, plus an optional R4 signature check. If any rule fails, the dialect is rejected and nothing changes.

┌──────────────────┐ ┌──────────────────┐ ┌──────────────────┐ │ incoming msg │ │ cbcl runtime │ │ peer agent │ │ │ │ │ │ │ │ s-expression │─────►│ lex → parse │─────►│ admitted msg │ │ (meta (define …)│ │ class: DCFL │ │ │ │ or performative│ │ bounds check │ │ core preserved │ │ or extended) │ │ │ │ dialect logged │ └──────────────────┘ │ if dialect: │ └──────────────────┘ │ admit? │ │ rule 1 no-rec │ │ rule 2 bounds │ │ rule 3 core │ └────────┬─────────┘ │ on reject ▼ ┌────────┴─────────┐ │ reject + error │ │ proof witness │ └──────────────────┘ ┌──────────────────────────────────────┐ │ Lean 4 theorems │ │ decidability preserved │ │ DCFL class preserved │ │ core performative semantics stable│ └──────────────────────────────────────┘

Core is a fixed point

No dialect can shadow, rebind, or override a core performative. Proven, not promised.

Dialects are declarative

Pattern and template, no imperative code, no side effects. Just a rewrite rule with resource bounds.

Bounded by construction

Every dialect declares max-depth, max-expansion-size, and verification-time-ms. The runtime enforces them before admission.

Runtime contracts

Dialects can carry causal protocols (which message types may follow which) and shape constraints (required parameters, types, depth). Verification is a monotone predicate on the append-only message store — coordination-free per CALM, with a three-valued verdict (Valid / Violation / Unknown) stable under store growth.

Parser is deterministic

One canonical parser. No parser differentials between implementations. Same input, same tree, every time.

Portable core

no_std + alloc Rust, WASM build, C FFI. Ship it on a microcontroller or a browser.

Peer-to-peer, no registry

Agents teach dialects through meta teach messages. Epidemic propagation converges in O(log n) rounds — a 100-agent network in ~2.6 ms. The proof travels with the definition.

Fast enough to ignore

Parse a tell in 78 ns. End-to-end pipeline for a simple message: 386 ns. Full R1–R3 verification of a meta define: ~1 µs. Criterion benchmarks, Apple M4.

Canonical on the wire

Signing and hashing use the RFC 9804 canonical S-expression form. Structurally identical messages produce identical bytes — no signature drift across implementations.

Standardised

IETF Internet-Draft registers the application/cbcl media type. A Nostr transport binding (cbcl-nostr) carries messages and Lightning micropayments over decentralised relays.

Questions

Frequently asked questions.

Why not just JSON?

JSON has no semantic layer, no verb vocabulary, and every schema is parsed by a handful of subtly-different libraries. Parser differentials are a live attack surface. cbcl is a deterministic grammar with a fixed-point core and proved invariants.

Why not FIPA-ACL?

FIPA fixed the vocabulary in the 1990s and couldn't evolve. cbcl takes FIPA's semantic rigour and adds a bounded, verifiable extension mechanism. The core performatives are a proper subset of FIPA's; the dialect mechanism is what's new.

What does "DCFL" buy me in practice?

Linear-time parsing, single unambiguous parse tree, no parser differential attacks, and decidable membership. The same class as a well-behaved programming-language syntax. Larger classes either cost polynomial time or admit weird-machines.

"Zero sorries" — what does that mean?

In Lean 4, sorry is a placeholder for an unfinished proof. Zero sorries means every theorem in the codebase has a complete, machine-checked proof. 176 theorems across ~5,400 lines of Lean, all discharged, no custom axioms.

Can I embed this?

Yes. The core is pure Rust, no_std + alloc. WASM build for browsers and edge; C FFI for native embedding; pure-Rust for servers and CLIs.

Where's the source?

Open source, Apache-2.0, at codeberg.org/anuna/cbcl-rs — Rust implementation (~11,000 LOC across five crates), Lean 4 formalisation (~5,400 LOC, 16 modules), IETF draft, and test vectors in one repo. Nostr transport at cbcl-nostr.

An agent language that extends itself, safely.