# Protocols & Sessions > Session-typed generative exchanges in Sema — protocol declarations compiled to state machines, transition checking, and structured concurrency. 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 | ...`: ```sema 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: ```sema 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`](/neurosymbolic/simulate/) site or a `context` declaration binds to a session type with **`use protocol `**. 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. :::note[Inside `simulate` the protocol can be implicit] When a `simulate def` returns a schema-typed value, the protocol is implicit — the return type *is* the schema. `use protocol ` is the explicit form for multi-turn exchanges where you want the whole interaction shape, not just a single return, checked. ::: ## 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: ```sema 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](/governance/budget/). - `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 ` compiles each `protocol` to a state machine and validates `use protocol` bindings and transition targets. - `sema assure ` 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. ## See also - [Simulate](/neurosymbolic/simulate/) — `use protocol ` and schema-typed returns. - [Events](/governance/events/) — asynchronous typed signals (vs. synchronous session transitions). - [Budgets & Metering](/governance/budget/) — how the scheduler batches concurrent model calls. - [Construct Catalog](/reference/language-spec/05-construct-catalog/) — the full `protocol` and concurrency grammar.