Interactive protocol authoring

Explore an Accord protocol.

The diagram shows who talks to whom, which messages they exchange, and the conditions on each step. Pick a preset to study a worked example, or choose Create new to draft your own. Tier 0 language checking (parser, scope, guards, projection, and difference-logic guard entailment) run in your browser, with nothing to install. Abacus is the minimal assured checker for that narrow fragment: it returns a sound accept/reject or a precise refusal when a protocol leaves it. Graph, nuXmv, and Platum generation still need a connected native Tier-1G checker.

In-browser checks: on Abacus: minimal assured checker (on-device)

Participants

Drag from a participant handle at the top of a lifeline across to another participant to add a message. Select an arrow first to insert right after it. Double-click any message to edit its signature. Select an arrow and press Delete to remove it. Ctrl/Cmd+Z undoes the last change.

Editable .acc source

Auto-apply

The bundled Tier 0 checker parses this source in your browser, so Apply and Load work with nothing installed. Invalid or unsupported source keeps the last valid diagram. Choices and scalar state loops can nest at any depth. Tuple payloads and tuple valued loop state stay source only in the current visual importer.

Diagnostics

Checker status, verification, and downloadable artifacts

Editing… Not verified

Verification provenance

Checking service… Authoritative operations are paused until status is known.

Developer

Service endpoint

Visual edits work locally and are labeled as drafts until a checker accepts them. Abacus is the minimal assured browser checker for the supported difference-logic fragment. A connected native checker runs the authoritative Tier 0 language check automatically for each committed revision. The Verify button runs the extracted Abacus difference-logic projectability checker in this page; it does not send source to a prover. Unsupported guards refuse with the exact local F*/Z3 or Lean escalation. Source import stays local; graph, nuXmv, and Platum generation still require the native service.

Generated and verified artifacts

Abacus verifies the supported difference-logic/projectability fragment in the browser. The F* module is emitted from the exact Tier-0 accepted revision; it is source for later verification, not an F*/Z3 verdict. Graph, nuXmv, and Platum downloads independently verify the exact revision at native Tier 1G. F*, Z3, and backend tools still require a checker service or local bridge.

Abacus and F* source emission run in-browser; graph JSON, nuXmv, and Platum artifacts require the native Tier-1G checker.

Guide

The Accord protocol guide

A full walkthrough of what Accord is, the language it uses, and every way to edit a protocol in this page. No prior Accord knowledge is assumed. If you have never seen a session type, start at the top; if you have, skim to The .acc language or The editor, action by action.

1. What Accord is

Accord lets you describe a communication protocol one time, as a single global specification: who the participants are, which messages they send and in what order, and the conditions each value must satisfy. From that one description the tool does three things. It checks the protocol is well formed. It extracts it to F* so the important properties can be proved by machine. And once verified it can generate runtime monitors and per-participant endpoint code from the proven result.

On this page the visual editor and the .acc text are two views of one model. Editing either one updates the other. The diagram is an authoring aid, not the proof: the proof comes from the checker and, at the higher tiers, from F* and the SMT solver Z3.

The running example. Throughout this guide the Authenticate preset is used: a client sends a PIN to a gateway, which forwards the comparison value and retries against a server up to five times. That forwarding is deliberate: the server can evaluate every guarded branch from its own local environment, so this PLDI27-auth revision is projectable and passes Abacus. Load it from the Protocol menu to follow along.

2. Session types and RMPST

A session type is a type for a conversation. Ordinary types describe a single value (an int, a bool). A session type describes a whole sequence of messages between parties: first A sends B a number, then B sends A a yes or no, then the conversation ends. Because the sequence is typed, a compiler can catch a participant that sends the wrong message, sends it at the wrong time, or forgets to handle a reply.

Three ingredients cover almost everything. A message moves a typed value from one party to another. A choice is a branch point: one party decides, and every other party must be ready for each option. A recursion lets the conversation repeat, which is how you get loops like “keep retrying until you succeed or run out of tries”.

Accord adds one more ingredient: refinements. A payload is not just an int; it is an int that must satisfy a stated condition, such as a PIN between 0 and 999999, or a reply that equals an earlier value. This is what turns a plain session type into a refined session type, and it is where F* and Z3 earn their keep: they check the conditions are consistent and actually hold.

Refined multiparty session types (RMPST). A global type is the choreography shared by all roles: who sends which labelled message, in what order, with which branch and loop. Projection turns that global type into one local type per participant; merge checks that a participant can follow every branch it does not choose without ambiguity. Refinements add predicates to the payloads and let later guards refer to values or loop state already introduced by the conversation. In the running example, the PIN and forwarded comparison value are refined integers, and the gateway's retry loop is a small RMPST choreography whose local machines must agree. Accord gives this story an executable checker and an F* proof path rather than leaving it as a diagram alone.

3. Why F*, refinements, and RCFSMs

Why F* (formal semantics). F* is a proof-oriented programming language with refinement types and an SMT solver behind it. Writing the protocol out in F* gives it a precise mathematical meaning instead of an informal description. A refinement type like x:int{x > 0} is the type of integers that are positive, and the compiler will not accept a value unless it can prove the condition. That is exactly the machinery a refined session type needs.

Why extract to F* (so the proofs hold). Generating an F* module means the properties are machine-checked proofs, not tests that happened to pass. The same .acc source always produces the same proof obligations, so a green result is reproducible and reviewable. The tool never “believes” the diagram; it believes the checker.

Why an RCFSM (the semantics used for the proofs). Underneath, a protocol denotes a refined communicating finite-state machine (RCFSM). Each role runs a small state machine, the machines exchange messages, and the refinements on payloads travel along the transitions. This is the classical communicating finite-state machine view of protocols, extended with refinements. It is what makes two questions precise: does the global protocol make sense, and can it be projected onto each participant so that everyone’s local machine agrees. Proving both is the heart of the verification.

4. The .acc language

A protocol names its roles, then lists what happens, top to bottom. Here is a complete tiny protocol:

protocol Ping {
  roles Client = 0, Server = 1;
  Client -> Server : Request(n: int { n > 0 }) {
    Server -> Client : Reply(ok: bool);
    end;
  }
}

Reading it piece by piece:

roles Client = 0, Server = 1;: The participants, each with a fixed numeric id used when the protocol is projected and compiled.
Client -> Server : Request(n: int { n > 0 }): A message: from Client to Server, with label Request and a payload named n of type int refined by n > 0. Payload types are unit, int, or bool. The refinement in braces is optional; when present it must hold for the value sent.
the { ... } after a message: Simply what happens next. Nesting a continuation inside a message’s braces is how the protocol sequences, so it reads like a story.
choice A -> B { Branch(..) {guard} -> ... }: An external choice: role A picks a branch and B (and anyone downstream) must handle each one. Each branch has a label, a payload, and an optional guard, a condition saying when that branch applies. Guards may refer to earlier payloads and to loop state.
loop T(count: int { 0 < count } = 1) { ... continue T(count + 1) ... }: Recursion carrying state. The loop declares a state variable, an invariant it must always keep, and an initial value. continue T(expr) jumps back to the top and updates the state. This is the μ you see in the session-type view.
end: A branch or the protocol finishes.

Projectability and merge. For a protocol to pass, it must be projectable: every role must be able to run its own local machine consistently, and wherever branches rejoin, their continuations must agree so the merge is well defined. If a choice cannot be projected (for example, a role cannot tell which branch was taken), the checker rejects it and the diagram keeps the last valid revision. A guard can also be well-formed but fail projectability when its receiver cannot see a referenced binder. The original authentication example used expected_code in a Server guard before Server had that value; the displayed revision forwards it as rq_expected so the success, retry, and lockout branches are genuinely checkable.

5. The editor, action by action

Everything below works with nothing installed. The bundled Tier 0 checker runs in your browser, so each committed change is checked immediately and the diagram, the session-type view, and the .acc text stay in sync.

Drag handle to handle to add a message.

Add a message

Each lifeline has a labelled round handle at the top. Press on one participant’s handle and drag across to another, then release. A new message appears between them, and you can rename it next.

Double-click a message to retype it, refinement and all.

Edit a message signature

Double-click any message, including one inside a choice branch, and type a full signature such as Hello(n: int { n > 3 }). Press Enter to apply. The checker validates it and the .acc text updates. Use _ or omit the binder for a plain payload like Ack(unit).

Select a run of messages, then wrap it in a loop.

Wrap a run of messages

Each message has a small circle toggle. Click one, then another further down, to select a contiguous run; the inspector then offers to wrap that run in a loop or a choice, or to clear the selection. This is the quick way to turn a straight-line sequence into a retry loop or a branch.

Drag a message past its neighbour to swap the order.

Reorder messages

Drag a message by its grip handle to move it within a block. Dragging one message past an adjacent one swaps their order, so you can put message one ahead of message two without retyping either.

Select an arrow, then press Delete or Backspace.

Delete an arrow

Select a message and press Delete or Backspace to remove it. Deletion is ignored while you are typing in a field, so it never eats text.

Undo restores the last edit; Reset starts a fresh, undoable draft.

Undo and reset

Undo the last change with the Undo button or Ctrl/Cmd⁠+⁠Z; the history holds the last fifty steps. Reset returns to a fresh two-participant protocol, and Reset is itself undoable.

Add a participant, then rename its generated identifier.

Add participants and frames

Use + participant, + loop (μ), and + choice (alt). A new loop or choice is inserted into whichever block is selected, so click into a loop body or a branch first to nest.

Edit the loop invariant and its continue-state update.

Edit loops and continues

Select a loop to edit its name, state variable, state type, invariant, and initial value in the inspector. Select a continue row to edit how the state updates on each pass, for example count + 1. These are the loop condition and the recurrence you see in the session-type view.

Select an arrow first to insert the next message directly after it.

Insert in the right place

New messages land at the end of the current block by default. To place one mid-sequence, first click an existing arrow to select it, then drag a new arrow in the same block: the new message is inserted directly after the selected one.

Edit refinements and branch guards with variables that are in scope.

Refinements and guards

Select a message to set a payload refinement, or a choice branch to set a guard. When a checker is connected, the inspector suggests the variables in scope at that point, so a guard can reference an earlier payload or the loop counter.

Type source directly; Auto-apply redraws while manual Apply remains available.

Edit the .acc text directly

The editable source sits full width below the diagram. Turn on Auto-apply to parse and redraw while you type, or leave it off and press Apply to diagram when ready. Swap puts the source above the diagram. Revert source discards text edits. Tab inserts indentation instead of leaving the field. Invalid text keeps the last valid diagram.

Switch presets, load a local .acc file, create fresh, or export the current source.

Load, export, and switch presets

Pick a preset from the Protocol menu to study a worked example, or Create new to start blank. Load .acc reads a file from disk; Export .acc downloads the current protocol.

Refused edits show a diagnostic and never replace the last valid diagram.

Why some edits are refused

You can nest loops and choices freely, but the checker refuses anything that is not well formed or not projectable, and the diagram keeps the last valid revision. That is by design: an unsound protocol should never look accepted.

6. Tiers: what actually gets proved

Accord is careful to separate “the text is well formed” from “the properties are proved”. The page distinguishes Tier 0, the browser Abacus assurance boundary, and the native Tier 1 profiles; it never blurs them.

Tier 0

Well-formed language

Fast, authoritative parsing plus checks on names, scope, kinds, hygiene, continuations, choices, loops, guards, and reachability. No F* or Z3. This runs in your browser here.

Abacus

Minimal assured browser checker

An extracted, verified difference-logic checker for the supported int/bool/unit fragment. It checks projectability and guard entailment on-device, with no network or external prover. It is deliberately not a full F*/Z3 proof or backend generator.

Tier 1G

Verified global extraction

F* and Z3 accepted the global protocol graph. This is the gate for the graph JSON, the nuXmv model, and the Platum monitor. It needs a connected checker with F* and Z3.

Tier 1P

Verified projections

Tier 1G plus a valid local graph for every role, so the protocol projects onto each participant. This is the gate for per-participant endpoint code.

In short: drafting, Tier 0, Abacus's supported fragment, and F* source emission are local; native Tier 1 verification and global artifact generation need the pinned toolchain, and editing after a verified result makes it stale.

7. Artifacts you can generate

Once a revision clears the right tier, it can produce concrete outputs. The Checker status, verification, and downloadable artifacts panel at the bottom of the workspace is where these live.

Getting the F* module, graph, nuXmv, and Platum buttons to work locally. Abacus Verify and the F* source module work in your browser for their supported boundary. The graph, nuXmv, and Platum downloads, plus wider F*/Z3 verification, need the local checker running, not just F* and Z3 on your PATH. npm run preview only serves the static page, so native artifact buttons remain unavailable. In the website repo, run npm run checker:local in another terminal. It builds and starts the verifier-enabled compiler bridge on port 8137 and the gateway on port 8138. Make sure the editor’s Developer → Service endpoint is http://127.0.0.1:8138. Then the panel flips to “checker available” and the downloads run against your exact revision.

If F* says “Namespace Accord cannot be found”. The downloaded .fst is source, not a standalone proof file. It imports the pinned Accord, AccordMeta, PLDI27 adapter, and tactic modules, so running fstar.exe from an arbitrary download directory leaves those namespaces off the include path. From the sibling guidsl checkout, use the project verifier so the core bundle is checked:

cd /absolute/path/to/Datum/guidsl
make
./acc verify /absolute/path/to/protocol.acc --profile projectable --core-dir ../PLDI27

A direct F* invocation must include the matching guidsl, PLDI27, and adapter roots. If the command stops on a core-bundle hash mismatch, the checkout does not match the manifest's pinned revision; sync the exact PLDI27/core bundle or use its matching release. Do not disable the fail-closed identity check.

What the browser can and cannot do today. Abacus is a minimal assured checker: it can accept, reject, or refuse the narrow difference-logic/projectability fragment without requiring visitors to install F*, Z3, or anything else. The browser can also emit the compact F* source. It does not yet contain the serializers and native validation needed for verified global graph JSON, nuXmv models, or Platum C monitors, so those remain native Tier-1G outputs. Lean/AccordLean is a promising future common verified foundation and can eventually compile to WebAssembly, but it does not automatically generate the current artifacts until the backends are ported and tied to the same verified intermediate representation. A future no-install path would use an authenticated, sandboxed hosted worker with pinned toolchain hashes, exact source/revision binding, resource limits, and a bounded queue. Visitors do not need local F* for browser Abacus or source emission; local native verification and artifact generation do need the native F*/Z3/backend toolchain today.

F* module Tier 0: The compact generated F* source: the protocol plus the global model_check_extract value, ready for an explicit verification run. Emitting it does not by itself run F* or Z3; it is the input to that step. The larger --profile projectable module is an internal compiler artifact for additional projection checks and is not part of this download.
Global graph JSON Native Tier 1G: The verified protocol-wide state machine: states, transitions, participants, labels, guards, variables, and loop metadata. Analysis and interchange data, not an executable endpoint.
nuXmv model Native Tier 1G: A finite-state .smv model for the nuXmv model checker, generated from the verified global extraction. Downloading it is separate from running nuXmv and getting a property verdict.
Platum C monitor Native Tier 1G: A centralized C runtime monitor generated from the global graph. Deploying it still needs matching wire-schema bindings, headers, and C validation.
Per-participant endpoints Tier 1P, planned: One endpoint per role, generated from that role’s verified local graph. This is gated on the projectable tier and is being wired up.

8. Reading the diagram

Each vertical line is a participant. A horizontal arrow is a message from one participant to another; its label names the message, its payload is the value sent, and a refinement in braces is the condition the value must satisfy. A choice frame groups the alternative branches one participant may pick. A loop frame is a recursion and carries the state that later guards read. The session-type view in the preset intro is the same information in mathematical notation.

The picture is an authoring aid, not a proof. Tier 0 checks the serialized source as you edit; F* and Z3 verification is a separate, explicit action for the exact accepted revision.