Vertep

Agent protocols (Kolyada)

Kolyada lets an agent say, in a form a stranger can verify, how to talk to it: who sends which message, in which order, to whom. A protocol is one JSON-LD document; its identity is the hash of its graph; every role runs a projection of it; and every message is signed before any transport carries it, so a peer that trusts nobody can still check each step.

Kolyada is milestone M10, in progress. The core crate vertep-kolyada is built and tested: documents, identity, shapes, projection, signed envelopes, the conformance check, causal delivery, history, sub-protocols, offers and the RDF bridge. Not built yet: the join policy, sealed fan-out and the inbound and outbound checks in the mailbox and send path (in vertep-federation), the vt:plays chart declaration, vt kolyada, and the Lean model. Until then you drive an Instance yourself, as below.

Grants, and what they cannot say

A grant says "this DID may send this event to this actor". That is enough for a client calling a service. It cannot say "first you ask, then I quote, then you order or cancel, and the auditor sees the quote but nothing else". A protocol says exactly that, in one document every party checks on its own. Inside a protocol instance the role is the authority: a DID bound to a role may send what that role's projection allows, and nothing else, without any grant.

The idea follows the Decentralised Web Node notion of published protocols, with three differences. Agents are statecharts, so a protocol is a chart over roles. Mailboxes hold only ciphertext, so a shared space is a logical grouping, not a shared store. And everything is checkable: documents by hash, messages by signature.

A protocol document

A protocol names its roles, its message types with payload shapes, and a choreography: states and transitions of the form "role X sends message M to roles Y". This one is a quote between a buyer, a seller and an auditor:

{
  "@context": "https://w3id.org/vertep/kolyada/1.0",
  "type": "Protocol",
  "version": "1.0",
  "roles": ["buyer", "seller", "auditor"],
  "messages": [
    { "id": "quote.request", "payload": { "fields": [
      { "name": "item", "datatype": "string", "min": 1, "max": 1 },
      { "name": "qty", "datatype": "integer", "min": 1, "max": 1 } ] } },
    { "id": "quote", "payload": { "fields": [
      { "name": "price", "datatype": "number", "min": 1, "max": 1 },
      { "name": "currency", "datatype": "string", "in": ["EUR", "USD"] } ] } },
    { "id": "order" },
    { "id": "cancel" },
    { "id": "receipt" }
  ],
  "initial": "Idle",
  "final": ["Cancelled", "Done"],
  "transitions": [
    { "from": "Idle", "sender": "buyer", "receivers": ["seller"], "message": "quote.request", "to": "Quoting" },
    { "from": "Quoting", "sender": "seller", "receivers": ["buyer", "auditor"], "message": "quote", "to": "Decided" },
    { "from": "Decided", "sender": "buyer", "receivers": ["seller"], "message": "order", "to": "Ordered" },
    { "from": "Decided", "sender": "buyer", "receivers": ["seller"], "message": "cancel", "to": "Cancelled" },
    { "from": "Ordered", "sender": "seller", "receivers": ["buyer"], "message": "receipt", "to": "Done" }
  ],
  "limits": { "bufferSize": 4, "timeoutMs": 1000 }
}
MemberMeaning
@contextAlways https://w3id.org/vertep/kolyada/1.0, embedded in the crate. A document that references any other context is rejected without a network request.
rolesThe role names.
messagesMessage types. A payload shape lists fields with name, datatype (string, integer, number, boolean), min, max and an optional in list: a small SHACL subset the checker interprets itself.
initial, finalThe start state and the end states.
transitionsfrom, sender, receivers, message, to. Timeouts and cancellations are ordinary messages.
limitsbufferSize and timeoutMs of causal delivery.

Well-formed choreographies allow sequence, loops and choice made by one role. A branching state whose options are sent by different roles, or regions running in parallel across roles, is rejected with the state named: one role must decide at every branching point, so each role's projection is well defined.

Identity and projection

The identity is the SHA-256 of the RDFC-1.0 canonical form of the document's graph, the same scheme as chart version IRIs: two JSON-LD spellings of one protocol have one identity, and a peer fetches a document by hash from anywhere and checks it. The projection onto a role keeps its sends and receives and makes everything else silent; its interface lists, per state, what the role accepts and from whom.

let protocol = Arc::new(Protocol::parse(QUOTE.as_bytes())?);
println!("protocol {}", protocol.id().as_str());
let interface = protocol.interface("seller").ok_or("no seller role")?;
protocol urn:vertep:protocol:sha256:45790502561699ae0a09e8e6c58096fcf6de7eca7bb242f3c0ca7b329e287bc6
  seller accepts in Decided: cancel from buyer
  seller accepts in Decided: order from buyer
  seller accepts in Idle: quote.request from buyer

An agent may implement its role with any chart or code; the projection fixes only what is visible on the wire.

Opening a space

A space is an instance id, a role binding and a history. The initiator signs a genesis that binds a DID to every role; its hash is the instance id. Every other participant reads it and countersigns with join (or decline); no role may speak before its join.

let (genesis, mut b) = Instance::create(protocol.clone(), &buyer, "buyer", &bindings, None)?;
let mut s = Instance::from_genesis(protocol.clone(), &genesis, SELLER, &verifier, None)
    .map_err(|reason| reason.as_str())?;
let join = s.join(&seller)?;          // sealed to every other role by the transport
b.receive(&join, &verifier, now_ms);

Signer and Verifier are traits: in Vertep they come from the key manager and the DID resolver, and the testkit feature has in-memory ones. The crate itself holds no keys and opens no connection.

Messages and the check

A message body carries the protocol identity, the instance id, the sender's role and a rising sequence number, the hashes it depends on, the roles it is sealed to, its type and its payload. It is signed with the sender's DID key before any transport seals it, so authenticity never depends on the transport (DIDComm authcrypt, for one, convinces only the recipient). Instance::send checks the sender's own projection first, so an agent cannot emit what its role may not send; Instance::receive runs the pure check:

  1. the signature, against the sender's DID;
  2. the instance, and that the sender is bound to the role it claims in an open instance;
  3. the dependencies: a message whose dependencies are missing is held, in a buffer the protocol bounds;
  4. the state: some state the participant may be in enables this message from this role;
  5. the payload, against its shape.

The result is Applied, Held, Duplicate or Refused with a reason from a fixed list: signature, wrong instance, role not permitted, not open, missing dependencies, not enabled in state, unknown message, payload shape, recipients, sequence, equivocation, buffer full, bad genesis, already joined. A refused message is kept as a Violation that anyone can re-check, and two different signed messages with one sequence number prove equivocation.

The tour runs the whole quote. The auditor holds the seller's quote until it is told the hash of the request it may not read; it cannot place an order; a seller who signs a receipt before any order is refused with proof:

instance 60e4e1b6f1223ab14efa47917db7b8460943a1bb4355506e19f125177d3ac01a
status after the joins: Open
seller <- quote.request: applied c3fb1ef77651
buyer  <- quote: applied 564cc9cf8e48
auditor <- quote: held 564cc9cf8e48
auditor <- hash of the hidden request: applied 564cc9cf8e48
auditor -> order: refused before sending (role not permitted)
buyer  <- receipt: refused (not enabled in state); violation re-checks: true
seller <- order: applied f9e37a4cc0c4
buyer  <- receipt: applied 7879aa311338
complete: buyer true, seller true

Hidden messages and history

Each copy of a message is sealed separately to each recipient, so a message sealed to a subset is unreadable to the other roles. Every message still lists the hashes it depends on, so participants compare heads (heads, missing_from) to find a gap, and a participant outside a subset is told the hash alone (observe_hidden), which releases whatever was waiting for it. A late joiner receives the history it may read (history_for), with hidden messages as hashes, and the chain still verifies. A participant knows the protocol state only through what it sees, so its checker keeps the set of states consistent with it.

A transition may open a child instance (a payment inside a purchase): its roles are bound from the parent's, participants already in the parent need no new join, and the child's completion ends the parent's waiting state. A space is then a tree of instances under one root genesis.

Offers and discovery

An agent says which roles it plays with a signed Offer (optionally expiring, optionally limited to some initiators) and lists its protocols in a VertepProtocol service entry of its DID document. There is no registry: a peer reads the entry, fetches the document by its hash from any source and verifies it (verify_fetched). The RDF bridge adds documents and offers to a graph, so "who offers the seller role of this protocol" is a SPARQL query.

offer verifies: true
service entry: {"id":"did:example:seller#kolyada","serviceEndpoint":[{"protocol":"urn:vertep:protocol:sha256:4579…7bc6","roles":["seller"]}],"type":"VertepProtocol"}

Test vectors

Another implementation proves it agrees without any Rust: crates/vertep-kolyada/vectors/ holds protocol identities, projections, envelope hashes and signatures, and verdict sequences as JSON, and check.mjs checks the envelopes with Node's crypto alone.

What is next

The binding to Vertep actors: a chart declares the roles it plays (vt:plays), the mailbox runs the check where grants run, before any journal append, and journals the verdict with the input, and the send path runs the same check on the actor's own projection. Then vt kolyada (validate, hash, project, offer, check), and a Lean model proving that accepted messages are enabled by the projection, that unbound roles are never accepted and that causally consistent orders converge, with a checker that replays recorded histories.

The design notes are in tg.md/views/kolyada.md; the requirements in openspec/changes/m10-agent-protocols (capabilities agent-protocols, protocol-conformance and protocol-spaces); the tour in crates/vertep-kolyada/examples/quote.rs. The article A protocol a stranger can check tells the story behind it.