Contract-BDD Messaging: Formalising Agent Communication as Verifiable Commitments

TheThe multi-agent systems page covers several mechanisms agents use to exchange information, from direct signals to shared resources to formal communication languages. This page asks a narrower question about all of them: once a message has been sent, what stops either side from simply claiming, afterward, that the exchange went however suits them? The answer computer science and multi-agent systems research have separately converged on is to stop trusting claims about the exchange and start formalising the exchange itself as something checkable.

Why trust-based semantics aren't enough

FormalFormal agent communication languages like FIPA-ACL define what a message means in terms of the sender's mental state — a propose performative is meant to express that the sender genuinely believes the proposal is achievable. Singh's influential critique of this approach is direct: a mental state is private and unverifiable, so grounding communication semantics in claimed beliefs gives no external way to check whether an agent's message was honest¹. His alternative treats agent communication acts as creating social commitments — public, externally observable obligations, checkable independently of what either party privately intended. Formally, a conditional commitment is written CC(x, y, p, q): if condition p holds, x becomes obligated to y to bring about q². Read that structure again: it is a precondition and a postcondition, developed independently for a different reason than Meyer's Design by Contract, but structurally the same idea³.

A separate tradition in programming language theory arrived at a closely related answer from the type-theory side. Session types formalise a communication protocol itself as a type, checked for conformance — often before the program even runs — rather than leaving protocol adherence as an informal expectation between the two ends of a channel⁴. Between Singh's commitment logic and session types, two independent fields spent decades concluding the same thing: a communication protocol needs to be a checkable structure, not a trust relationship.

The concrete mechanism

ThisThis site's material on requirements engineering already documents how PatLang embeds Design by Contract directly inside its BDD syntax: a require precondition as an And clause under Given, an ensure postcondition as an And clause under Then. Extending that mechanism from single-program specification to inter-agent messaging is a small syntactic step with a large semantic consequence. A BDD scenario for a message exchange between two agents reads naturally as Singh's CC(x, y, p, q): the Given...And clause is a precondition on the sender (you may only send this proposal if you can actually deliver it — the debtor-side obligation Singh's formalism requires), and the Then...And clause is a postcondition establishing a commitment on the receiver (accepting the message creates an obligation, checkable independently of whether the receiver "meant it"). The scenario stops being a test of one program's correctness and becomes a formal specification of the social commitment the exchange itself creates.

Feeding the Calculus of Trust

ThisThis site's material on a distributed embedding calculus of trust models trust between agents as a continuously updated vector, with an explicit update rule:

\[ \frac{dT}{dt} = \alpha \cdot E_{\text{positive}} - \beta \cdot E_{\text{negative}} - \gamma \cdot T_{\text{uncertainty}} \]

That page is precise about how trust should combine and decay, and deliberately leaves open what actually counts as \(E_{\text{positive}}\) or \(E_{\text{negative}}\) in the first place — a reasonable scope decision for a page about the calculus itself, but a real gap something has to fill in any actual implementation. Contract-BDD messaging is a natural candidate: a fulfilled commitment is unambiguous positive evidence, a violated one is unambiguous negative evidence, and neither depends on trusting either party's account of what happened, because the contract's satisfaction is checked externally against the exchange itself.

This also speaks directly to two of the three Open Problems that page names explicitly. Interpretability — that a learned similarity function over embeddings is harder to justify to an auditor than a rule-based score — is substantially improved when the underlying evidence is a specific, named contract clause that was or wasn't satisfied, rather than an opaque interaction outcome. Adversarial manipulation — an entity generating cheap, favourable interactions to inflate its own trust score — is harder, though not impossible, against a contract that specifies real preconditions genuinely costly to satisfy, compared with an unstructured "the interaction went fine" signal a manipulator only has to fabricate the appearance of. This is a proposed extension to that page's framework, not a claim the page itself makes — worth being precise about, since the calculus was deliberately written to be evidence-source-agnostic, and contract-BDD messaging is one specific, compatible way of supplying that evidence, not the only one.

Compiling verified trust into reflex

HereHere the argument becomes more speculative, and it's worth marking clearly where solid ground ends. The cognitive cycle page describes Procedural Memory as compiled through repeated practice — Anderson's account of declarative knowledge, used repeatedly, compiling into fast production rules that no longer require conscious mediation⁵. If inter-agent messages are formalised as contract-BDD scenarios, the accumulated history of fulfilled exchanges between two specific agents is, in a real and not merely metaphorical sense, a growing set of Given/When/Then examples — precisely PatLang's synthesis engine's required input format. It is a genuinely open, rather than settled, question whether that engine could be pointed directly at such a history to synthesise a fast, compiled responder for a given interaction pattern — a concrete, literal implementation of Anderson's knowledge compilation, specifically for inter-agent communication. The solid part of this claim is that PatLang's synthesis engine already does induce working code from exactly this kind of example set. The open part is whether a sequence of protocol-level exchanges translates cleanly into the kind of individual input-output examples the engine has been demonstrated on — a real engineering question this page raises rather than answers.

If it does work, it suggests a design principle worth stating regardless of whether the synthesis step is ever actually built: reliance on a compiled reflex should be gated by the current trust score for that specific relationship and context, not applied uniformly. A high-trust, well-established relationship earns the low-latency, low-scrutiny procedural shortcut. A new or currently-uncertain relationship should fall back to the slower, fully contract-checked exchange — exactly the reflex-versus-deliberation trade-off the agent archetypes page argues is a legitimate design choice, now made specifically conditional on trust rather than fixed at design time.

Where this connects

• Multi-Agent Systems: Coordination, Communication, and Strategic Interaction — the fuller set of communication mechanisms this page's formalisation applies on top of.
• Where Requirements Get Hard: Wicked Problems, CATWOE's Slippery Names, and Assumptions Engineering — the original require-in-Given/ensure-in-Then mechanism this page extends from single-program to inter-agent specification.
• A Distributed Embedding Calculus of Trust — the trust framework this page proposes a concrete evidence source for.
• Agent Archetypes: Five Tiers on One Diagram — the reflex-versus-deliberation trade-off this page's trust-gated compilation idea extends.
• Inductive Synthesis: from BDD scenarios to PatLang code — the actual synthesis mechanism this page speculates could be pointed at accumulated interaction histories.

References