Interactive protocol authoring

Explore a SPECTRE protocol.

The diagram shows who communicates, which messages they exchange, and the conditions that govern each step. You can inspect the verified Authenticate example or use the editor to draft your own protocol. Visual drafting works in the browser. Formal checking and generated artifacts require a connected SPECTRE checker service.

Tier-0 well-formedParser, scope, guards

Verification pendingChecking snapshot metadata

Authenticate · loading revision

Loading protocol model…

Authenticate.spe

Editing… Not verified

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. A connected checker runs the authoritative Tier 0 language check automatically for each committed revision. The Verify button additionally runs the F*/Z3 projectability check when verification is enabled on that service. Source import and artifact generation also stay behind the service. Publishing this static page does not start or authorize a public checker.

Generated and verified artifacts

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 Tier 1G. The browser does not run F*, Z3, OCaml, or backend tools itself.

Requires a connected local checker; verified artifacts additionally require local F*/Z3.

Participants

Diagnostics

Editable .spe source

Source import requires a connected checker because the browser does not duplicate the authoritative parser. Visual controls remain available offline. With a checker connected, 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 remain source only in the current visual importer.

Assurance guide

From local draft to verified output

“Connect a checker and run Tier 0 first” does not require a hidden Tier 0 button. Once the service card says Authoritative checker available, the current diagram is serialized, hashed, and checked automatically. Fix any diagnostics; the status becomes Tier-0 well-formed. Then Tier 1P verification and capability-appropriate downloads become meaningful for that exact revision.

01
Draft locally
Visual controls work offline, but the result remains an unverified browser draft.
02
Tier 0 runs automatically
spe_core parses the source and checks names, scope, kinds, choices, loops, guards, and reachability.
03
Verify Tier 1P explicitly
F*/Z3 checks global validity plus projection to every participant. Editing afterward makes the result stale.
04
Generate for a named capability
Current global outputs use Tier 1G. Future participant bundles must use Tier 1P.

Tier 0

Well-formed language

Fast authoritative parsing, scope, kind, hygiene, continuation, choice, and reachability checks. No F* or Z3.

Tier 1G · global

Verified global extraction

F*/Z3 accepted the global protocol graph. This is the gate for graph JSON, nuXmv, and Platum.

Tier 1P · projectable

Verified participant projections

Tier 1G plus a valid local graph for every role. This is the gate for Rustgen and Facet Artifact 2.

The detailed local setup, editing workflow, failure guide, provenance rules, and examples are in Using the interactive SPECTRE page.

Outputs and roadmap

What each artifact means

Available · Tier 0

F* module

The generated F* source and its `.spe` semantics, ready for an explicit CLI or bridge verification run.

Emission does not run F*, Z3, or establish a verification verdict; the CLI also retains a `.spemap` source map.

Available · Tier 1G

Global graph JSON

The verified protocol-wide state machine: states, transitions, participants, labels, guards, variables, and loop metadata.

Analysis and interchange data—not an executable endpoint or participant-local graph.

Available · Tier 1G

nuXmv model

A retained finite-state .smv model generated by Fact from the verified global extraction.

Downloading a model is separate from running nuXmv and obtaining a property verdict.

Available · Tier 1G

Platum C monitor

A centralized C runtime monitor generated from the global graph using current MAVLink-oriented conventions.

Deployment still needs matching wire-schema bindings, headers, and C validation.

Planned · Tier 1P

Rustgen workspace

One Rust/Flux endpoint crate per participant, generated from that participant’s verified local graph.

CLI generation exists; service exposure still needs final projected-bundle provenance and an isolated production worker.

Planned · Tier 1P

Facet Artifact 2

An OCaml TCP/IP distributed enforcer bundle that deploys each specification local graph at its role boundary.

Next gates: role/endpoint launch policy, canonical runtime packaging, isolated job execution, and allowed/violating trace tests.

Implementation sequencing and exit gates are defined in the Rustgen and Facet Artifact 2 integration plan. The draft shared bundle shape is documented but is not accepted by the current service.

Diagram guide

What the visual model means

Each vertical line represents a participant in the protocol. A horizontal arrow records a message from one participant to another. Its label identifies the message, its payload records the transmitted value, and an optional refinement states the condition that value must satisfy.

Choice frames group alternative branches selected by one participant. Loop frames represent recursive behavior and carry the state needed by later guards. The source view is the textual form of the same editable browser model.

The picture is an authoring aid rather than a proof. When a checker is connected, the serialized source is checked by the authoritative compiler. F*/Z3 verification is a separate explicit action for the exact accepted revision.