Status: Design proposal (2026-05-27) — for review before implementation.
Goal: Promote PULSE from a structural schema (named phases + named tokens) to a typed protocol (session-typed phases + linear tokens + projected choreography). Bring formal-spec quality to the level of behavioral type systems without losing the implementation maturity of v0.1.1.
PULSE v0.1.1 declares 5 phase kinds, 6 cross-loop tokens, and 7 invariants. The schema validates names and shapes but cannot answer:
| Question v0.1.1 cannot answer | What's needed |
|---|---|
| Is this manifest deadlock-free? | Session-typed phase graph |
Will every emitted SurpriseSignal be consumed? | Linear token typing |
Is loop@v2 a safe drop-in replacement for loop@v1? | Behavioral subtyping |
| If loop A sends X, will loop B receive a compatible X? | Multiparty choreography + projection |
| Does this phase's declared effect match its runtime behavior? | Effect rows + runtime fidelity check |
| Are the declared invariants actually true of this manifest? | Refinement-type checker |
Behavioral type systems (session types, multiparty session types, behavioral contracts) answer exactly these questions — but as preprints, not as running software. PULSE v0.2 ports the answers into a JSON-Schema-grounded substrate that already has 5 reference manifests and a conformance suite.
| Axis | v0.1.1 | v0.2 | Why |
|---|---|---|---|
| Formality | 8 | 10 | Session-type-grade; refinement types on cadence/invariants; effect rows on phases |
| Compositionality | 7 | 10 | Choreography + projection; linear tokens; behavioral subtyping |
| Substrate independence | 9 | 10 | Typed protocol portable to any language with a type system |
| Closure | 7 | 9 | Liveness + fidelity machine-checked; loses 1 for new verifier dependency |
| Total / 40 | 31 | 39 |
For external context see docs/V0.2-BEHAVIORAL-TYPES-RATIONALE.md (planned) which compares this against Agent Behavioral Contracts (preprint), AgentRFC, and the CCS/CSP ceiling.
File: schemas/pulse-tokens.v0.2.json (new)
Each canonical token gets a payload schema, a linearity annotation, a variance annotation, and a TTL.
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"tokens": {
"TopologyContext": {
"payload_schema": "schemas/tokens/topology_context.v0.2.json",
"linearity": "linear",
"variance": "covariant",
"ttl_ms": 60000,
"description": "Emitted by retrieve, consumed by route. Loss would blind routing — must be consumed."
},
"DeliberationRequest": {
"payload_schema": "schemas/tokens/deliberation_request.v0.2.json",
"linearity": "linear",
"variance": "invariant",
"ttl_ms": 300000,
"description": "Triggers an inner deliberation loop. Loss would silently skip κ-resolution."
},
"DeliberationResult": {
"payload_schema": "schemas/tokens/deliberation_result.v0.2.json",
"linearity": "linear",
"variance": "invariant",
"ttl_ms": 300000
},
"OutcomeSignal": {
"payload_schema": "schemas/tokens/outcome_signal.v0.2.json",
"linearity": "linear",
"variance": "covariant",
"ttl_ms": 3600000,
"description": "Audit primitive. Every action result must produce one — drop = audit failure."
},
"ReputationUpdate": {
"payload_schema": "schemas/tokens/reputation_update.v0.2.json",
"linearity": "affine",
"variance": "covariant",
"ttl_ms": 86400000,
"description": "Long-window aggregation; tolerates loss (drop down from linear because the next update overrides anyway)."
},
"ConsolidationEvent": {
"payload_schema": "schemas/tokens/consolidation_event.v0.2.json",
"linearity": "affine",
"variance": "covariant",
"ttl_ms": 3600000,
"description": "Housekeeping signal; consolidate is idempotent."
},
"SurpriseSignal": {
"payload_schema": "schemas/tokens/surprise_signal.v0.2.json",
"linearity": "linear",
"variance": "invariant",
"ttl_ms": 60000,
"description": "OS-011 forward-model-prediction-error. Must be consumed."
},
"SessionFidelityViolation": {
"payload_schema": "schemas/tokens/session_fidelity_violation.v0.2.json",
"linearity": "linear",
"variance": "invariant",
"ttl_ms": 86400000,
"description": "Runtime-observed protocol violation. Must be reported, never silently dropped."
}
}
}Default for new canonical tokens: `linear`. Authors must explicitly opt down to affine only when the token is observational, idempotent, or inherently lossy-tolerant (next emission overrides previous). This default flows from OS-010's "every consequential signal must be audited" thesis — silent loss is an audit failure; duplication is detected via idempotency keys at the substrate boundary.
Linearity values:
| Value | Meaning | Checker enforces |
|---|---|---|
linear | Exactly-once consumption | Emit ⇒ exactly one consumer; consumer is unique |
affine | At-most-once consumption | Emit ⇒ at most one consumer (may drop) |
relevant | At-least-once consumption | Emit ⇒ at least one consumer (may duplicate) |
unrestricted | Any consumption | No constraint |
Variance values:
| Value | Meaning |
|---|---|
covariant | Subtype payloads acceptable on the consumer side |
contravariant | Supertype payloads acceptable on the producer side |
invariant | Exact payload schema match required |
Required payload schemas: Each token gets its own JSON Schema under schemas/tokens/. Eight new schema files (the six v0.1.1 canonical tokens + two added in v0.2: DeliberationRequest, SessionFidelityViolation).
Token payload evolution happens in the global registry, never per-loop. This flows from OS-010 §1019–1051 ("canonical tokens stable through v1.0; additive-only without minor bump; vendor-namespacing for custom tokens").
Additive-only within a minor version. Adding optional fields to a
token's payload schema is allowed without bumping the token's version. Removing or renaming fields requires a minor version bump and 12-month notice (per OS-010 stability policy).
Registry tracks the partial order. The registry asserts
topology_context.v0.2 <: topology_context.v0.1 when the v0.2 schema is an additive extension of v0.1. The behavioral subtyping checker (§5) consults the registry rather than re-deriving compatibility.
No per-loop token variants. A loop that needs a custom payload
must register a vendor-namespaced token (e.g. acme.v1.AcmeOutcome) in the registry and reference it canonically from its manifest. Loops never declare local subtypes of canonical tokens — that would explode the cross-loop vocabulary and break PRISM's ability to benchmark heterogeneous systems against a shared evaluation grammar.
Change: Extend the existing phases[] entries in pulse-loop-manifest.v0.2.json with inputs, outputs, effects, successors, and refinements.
{
"phases": [
{
"id": "retrieve_context",
"kind": "retrieve",
"inputs": { "tokens": [], "substrates": ["memory"] },
"outputs": { "tokens": ["TopologyContext"] },
"effects": {
"calls": ["memory.retrieve_context", "memory.topology_analyze"],
"mutates": [],
"may_emit": [],
"external": []
},
"successors": ["route_topology"],
"refinements": {
"latency_ms_max": 200,
"deterministic": false
}
},
{
"id": "route_topology",
"kind": "route",
"inputs": { "tokens": ["TopologyContext"], "substrates": [] },
"outputs": { "tokens": [] },
"effects": {
"calls": [],
"mutates": [],
"may_emit": ["DeliberationRequest"],
"external": []
},
"successors": ["deliberate", "act_node_write"],
"refinements": {
"branch_predicate": "topology.routing"
}
}
]
}Effect row fields:
| Field | What it tracks |
|---|---|
calls | Substrate operation IDs invoked (e.g. memory.retrieve_context, policy.check_policy) |
mutates | Substrate operation IDs that change state (e.g. memory.store_node, audit.append_event) |
may_emit | Token names this phase may produce |
external | External resources touched (e.g. http://*, mcp://prism) |
Granularity is operation-level, not storage-level. Effect rows reference the substrate API surface defined in OS-010 §9 (e.g. memory.retrieve_context, audit.append_event), never specific storage paths like sqlite.kg.nodes. This flows from the "substrate independence" thesis: the spec must not assume a relational backend, and graphonomous swapping SQLite for Postgres should not require manifest changes.
Refinement values: key-value predicates. A small vendored evaluator handles the supported subset; unknown keys are passed through as documentation.
Supported refinement predicates (vendored mini-evaluator):
Comparison: ≤, <, ≥, >, ==, != on numeric or string literals
Boolean conjunction (∧ / &&) and disjunction (∨ / ||) over the above
Set membership: value in [a, b, c]
Negation of any of the above
No Z3, no external SMT solver, no optional peer dependency. The vendored evaluator is a few hundred lines of TypeScript in src/refinement.ts and runs in any environment that runs npm. The ≤25KB processor target from STACK_ARCHITECTURE_GAP_REVIEW.md applies here too.
Recognized refinement keys in v0.2:
latency_ms_max (number) — checker emits a benchmark assertion
deterministic (boolean) — flagged in conformance T-DET
branch_predicate (string) — referenced expression must appear in a
consumed token's payload schema
idempotent (boolean) — extends existing T03 phase-idempotency check
requires_kappa (string, e.g. "== 0", "> 0") — routing precondition
Not stored in the manifest — derived by the checker from the phase graph. Expressed internally as a regular expression over phase IDs (or an equivalent finite automaton).
For graphonomous.continual_learning the derived session type is:
loop = retrieve_context · route_topology
· ( deliberate · act_node_write
| act_node_write )
· learn_outcome
· ( consolidate )?Checker proves:
| Property | How |
|---|---|
| Reachability | Every declared phase is reachable from an entry phase |
| Progress | From any reachable phase a successor exists, or the loop terminates explicitly |
| No deadlock | The successor relation has no cycles that can't make progress |
| Token discipline | Every linear token emit has exactly one matching consumer reachable downstream; every affine has at most one |
| Effect monotonicity | A phase's declared effect row is a superset of its successors' assumed reads |
Output of pulse check <manifest>:
✓ session type derives: retrieve · route · (deliberate? · act) · learn · consolidate?
✓ all 8 canonical token consumers resolved
✓ all linear tokens have unique consumers
✓ all 7 invariants hold under refinement (vendored evaluator)
✓ progress: from any reachable phase, a successor exists
✓ liveness: retrieve is reachable from all phasesSchema: schemas/pulse-choreography.v0.2.json (new) File pattern: manifests/<name>.choreography.json
Choreographies live alongside loop manifests in `manifests/`, not in a separate top-level directory. This flows from the "Topology as Authority" thesis: a choreography is a higher-arity topology declaration (3+ participants) but still the same kind of artifact. Co-location keeps the authority for cross-loop topology in one place. No new choreographies/ directory is created.
Currently each manifest is local. v0.2 adds an optional global type that describes the cross-loop dance and projects to per-loop connection blocks.
{
"$schema": "https://opensentience.org/schemas/pulse-choreography.v0.2.json",
"choreography_id": "ecosystem.continual_learning_with_prism",
"version": "0.2.0",
"participants": [
"graphonomous.continual_learning",
"prism.benchmark",
"agentromatic.deliberation"
],
"global_type": [
{
"step": 1,
"from": "graphonomous.continual_learning",
"to": "agentromatic.deliberation",
"token": "DeliberationRequest",
"guard": "topology.kappa > 0"
},
{
"step": 2,
"from": "agentromatic.deliberation",
"to": "graphonomous.continual_learning",
"token": "DeliberationResult",
"after": [1]
},
{
"step": 3,
"from": "graphonomous.continual_learning",
"to": "prism.benchmark",
"token": "OutcomeSignal",
"cadence": "per_action",
"after": [2]
}
]
}Projection algorithm. Given a choreography C and participant P, produce the local view C↓P — a sequence of "emit X" / "expect X" obligations that the participant's PULSE manifest must satisfy. The checker then verifies each participant's connections block is consistent with its projection.
Soundness theorem (informal, follows MPST canon): If every participant locally type-checks against its projection, the choreography is deadlock-free, communication-safe, and progresses to termination.
A choreography can declare nesting (sub-choreographies) and parallel branches (parallel: [step_a, step_b]) using existing PULSE primitives.
New CLI: pulse compat <loop_a@v> <loop_b@v>
Replaces the de-facto policy of "bump the version and pray" with a machine-checked subtyping relation:
A <: B iff
phases: A.phases ⊇ B.phases (extension allowed)
inputs: ∀ p ∈ B: p_A.inputs ⊆ p_B.inputs (contravariant)
outputs: ∀ p ∈ B: p_A.outputs ⊇ p_B.outputs (covariant)
effects: ∀ p ∈ B: p_A.effects ⊆ p_B.effects (subeffecting)
linearity: A.linear_tokens ⊇ B.linear_tokens (no relaxation)
invariants: A.invariants ⊇ B.invariants (only added, not dropped)
cadence: A.cadence refines B.cadence (tighter, not looser)Output:
$ pulse compat [email protected] \
[email protected]
✓ phases: superset (added: episodic_replay)
✓ inputs: contravariant (no widenings broken)
✓ outputs: covariant
✓ effects: subeffecting holds
✓ linearity: SurpriseSignal added as linear (additive)
✓ invariants: superset (added: I7-episodic-monotonic)
✓ cadence: unchanged
VERDICT: 0.4.4 IS a safe behavioral subtype of 0.4.3.Failed-compat verdict includes a counterexample trace.
Existing: src/conformance.ts already runs the 12 v0.1 tests. v0.2 adds:
Offline checks (new):
| ID | Test |
|---|---|
| T13 | Session-type derivation succeeds |
| T14 | Reachability of all declared phases |
| T15 | Progress (no stuck states) |
| T16 | Linear-token consumer uniqueness |
| T17 | Affine-token consumer cap |
| T18 | Effect row monotonicity |
| T19 | Refinement satisfiability (vendored mini-evaluator) |
| T20 | Choreography projection consistency (if member) |
Runtime checks (new):
| ID | Test |
|---|---|
| T21 | Session fidelity — observed phase trace matches derived session type |
| T22 | Linear-token actually-consumed-once (over trace window) |
| T23 | Effect-row honesty — observed substrate calls ⊆ declared calls + mutates |
On violation the checker emits a new canonical token, SessionFidelityViolation, itself PULSE-typed, so violations flow through the same envelope plumbing as other signals.
v0.2 adds two tokens to the canonical set:
| Token | Phase emitter | Linearity | Purpose |
|---|---|---|---|
DeliberationRequest | route | linear | Triggers an inner deliberation loop (split out of overloaded routing) |
SessionFidelityViolation | conformance runtime | linear | Reports a runtime-observed protocol violation |
Total canonical tokens in v0.2: 8 (was 6 in v0.1.1).
v0.1.1 manifests continue to validate under v0.2 — every new field is optional. A v0.1.1 manifest validated under v0.2 schema receives:
| Field | Default when absent |
|---|---|
phases[].inputs | { "tokens": [], "substrates": [] } |
phases[].outputs | { "tokens": [] } |
phases[].effects | { "calls": [], "mutates": [], "may_emit": [], "external": [] } |
phases[].refinements | {} |
| Token registry lookups | Falls back to v0.1.1 implicit semantics (linear by default for canonical tokens, invariant, TTL = ∞) |
The checker reports v0.1.1-default manifests with degraded_checks: true — they pass T01–T12 but cannot pass T13–T23. Owners are nudged to enrich.
Not a process-algebra spec. PULSE v0.2 is session-typed, not
CCS/CSP-modeled. Process-algebra-grade deadlock-freedom across parallel sub-agents is a future v0.3 question.
Not an SMT/Z3 dependency. The refinement checker is a vendored
mini-evaluator over ≤/≥/==/membership/conjunction/disjunction. Z3 is neither a runtime dependency nor an optional peer dep. If a complex constraint can't be evaluated locally, the checker emits a warning and runtime fidelity (T21–T23) catches violations.
Not an MPST formalization paper. v0.2 follows MPST principles but
targets working software, not formal verification literature.
All five open questions are resolved against the project's stated thesis (see docs/V0.2-RATIONALE.md for the per-question evidence trail across OS-010, STACK_ARCHITECTURE_GAP_REVIEW.md, STACK_PLANNING.md, and the prompt set).
Linearity default. Resolved: `linear` for new canonical tokens.
Authors opt down to affine only for observational/idempotent/lossy- tolerant tokens. Flows from OS-010 §7.3 + §10.2 ("fail loud, leave a trace; silent loss is an audit failure").
Choreography artifact location. **Resolved: co-located in
manifests/.** No new top-level directory. Flows from STACK_TOPOLOGY_AS_AUTHORITY thesis — a choreography is a higher-arity topology artifact, same kind as a loop manifest.
Effect row granularity. **Resolved: operation-level, not
storage-level.** Effect rows reference substrate API operations from OS-010 §9 (e.g. memory.retrieve_context), never storage paths. Flows from "substrate independence" (OS-010 §3.4) and the "falsifiable processor" gate (STACK_ARCHITECTURE_GAP_REVIEW Finding 1).
Refinement checker dependency. **Resolved: vendor a tiny
evaluator.** No Z3, no SMT, no optional peer dep. Covers ≤/≥/==/ membership/∧/∨/¬. Flows from "tiny core, max portability" and the ≤25KB processor target (STACK_ARCHITECTURE_GAP_REVIEW Finding 2).
Per-loop token subtyping. Resolved: prohibited. Token payload
evolution happens only in the global registry, by additive-only rules. Custom payloads must vendor-namespace (e.g. acme.v1.X). Flows from OS-010 §1019–1051 (ecosystem-wide vocabulary stability) and STACK_PLANNING.md vendor-namespace pattern.