Protocols & Sessions

Markdown Open in ChatGPT Open in Claude

A protocol is a session type: it declares the legal shape of a multi-turn interaction — a generative conversation, a tool exchange, an operator recovery workflow — as a state machine of named transitions. The runtime checks a session against it, so an illegal interaction sequence is caught rather than silently allowed. The insight that makes this work with models is simple and sharp:

Message content is stochastic; message structure is not.

A simulate may produce any text at a given step, but which step comes next is a compile-time fact. That turns fidelity, progress, and deadlock-freedom into things the compiler can reason about, even for a conversation whose words are generated.

Why interaction shape belongs in the type

Multi-turn LLM code — an agent loop, a critique/revise exchange, a tool-calling session — usually has an implicit protocol living in prose and conditionals: “the model proposes, then we critique, then it either revises or we accept.” Nothing checks that the sequence is actually followed; a bug that accepts before critiquing, or loops forever, is invisible to the type system. Sema lifts that protocol into a declaration and checks every transition, subsuming MCP-style tool schemas as degenerate two-party sessions.

Syntax

A protocol declares states and their outgoing transitions. Each line is state: PayloadType -> target | target | ...:

protocol Review:                        # session type for a multi-turn generative exchange
    propose:  Draft    -> critique
    critique: Critique -> revise | accept
    revise:   Draft    -> critique
    accept:   Final    -> end

Read it as a state machine: from propose (carrying a Draft) you may only go to critique; from critique (carrying a Critique) you may go to revise or accept; and so on. A state with no outgoing transition is terminal — end is the optional explicit terminal.

The verified robotics-cell corpus declares two operational protocols this way — an operator recovery workflow and the cell supervisor lifecycle:

protocol OperatorRecovery:
    fault: FaultEvent -> propose
    propose: RecoveryPlan -> approve | reject | request_more_evidence
    request_more_evidence: WorkOrder -> propose
    approve: RecoveryPlan -> close
    reject: RecoveryPlan -> close

protocol CellSupervisor:
    order: WorkOrder -> running | rejected
    running: WorkOrder -> complete | fault
    fault: FaultEvent -> safe_stop | maintenance_review
    safe_stop: FaultEvent -> maintenance_review
    maintenance_review: RecoveryPlan -> resume | manual_hold

These make the deterministic shape of a workflow explicit even though individual payloads (a RecoveryPlan, a human approval) are stochastic or human-authored.

The protocol runtime

A protocol compiles to a session-type state machine (states plus declared transitions). The protocol.* operations check a live session against it:

protocol.open(name) — starts a session at the initial state.
protocol.step(session, to) — advances the session, only if state -> to is a declared transition; otherwise it raises ProtocolViolation.
protocol.state(session) — reads the current state.
protocol.can(session, to) — tests a transition without taking it.

An illegal sequence — say, stepping from propose straight to accept in Review — does not quietly succeed; it raises ProtocolViolation at the step.

Constraining a `simulate` or session

A simulate site or a context declaration binds to a session type with use protocol <Name>. Once bound, the multi-turn conversation is typed against the protocol: the content each turn produces is up to the model, but the structure — the sequence of turns and their payload types — is checked against the declared transitions. Fidelity, progress, and deadlock-freedom become compile-time facts rather than hopes.

Structured concurrency: `scope`, `spawn`, `parallel`

Protocols live alongside Sema’s structured-concurrency constructs, and both obey the same discipline: no orphan tasks. A scope is a structured nursery — children that outlive the scope are an error; scope exit joins all children, and a failure cancels siblings and propagates typed:

scope:                                  # structured nursery
    a = spawn summarize(article)
    b = spawn classify(article)
    c = spawn embed_related(article)
    # scope exit joins all; failures cancel siblings and propagate typed

results = parallel [summarize(x) for x in feed] # data-parallel; scheduler batches model calls

spawn returns a Task[T] handle with join() -> Result[T, TaskError] and cancel(); cancellation is cooperative, propagates the scope’s cancellation token, and is journaled.
parallel / scope bodies compile to independent dataflow branches — parallel by default — and the compiler maps shared prefixes and forks onto KV-cache reuse and batching.
scope/spawn closures obey the same capture rule as parallel lambdas: immutable captures unless the type is thread-safe.

Failure modes

A declared-illegal transition → ProtocolViolation at protocol.step, or a compile error where the interaction shape is statically known — independent of the payloads.
A protocol with no reachable terminal → surfaces in analysis as a progress/deadlock concern.
Unbatchable serial chains in a concurrent scope → visible in the observability tool as scheduler stalls, not mystery latency.

How it’s checked

sema check <project> compiles each protocol to a state machine and validates use protocol bindings and transition targets.
sema assure <project> exercises multi-turn simulate interactions against their bound protocols.
protocol.step violations and spawn cancellations are journaled, so replay reproduces the exact interaction and concurrency trace.