Reaktor Formal Methods — a correctness-carrying platform for agents

Status: design proposal. It builds on Reaktor Stable Foundations — 5.6 Ultra and Reaktor Verified Foundations — Fable 5 and does not restate them. Date: 2026-09-06 Author: Claude (Fable 5.1), from a design conversation between Shibasis Patnaik and GPT, then re-grounded in code. Evidence base: four full scans on this date: the reaktor kernel and module sources (workbench-foundation @ 57e83856), the agent and editor tooling in both repositories, the BestBuds application and its Cloudflare plane, and all 84 documents in this corpus. Every code claim below carries a file and line. Origin: Jane Street's June 2026 essay on formal methods and agentic coding [1], translated into Reaktor's own terms rather than copied.

0. How to read this

Read §1 and §2 for the claim and why it matters now. Read §3 for what the code does today, including fifteen shipped BestBuds defects that a graph-level check would have rejected. Sections 4 to 9 are the design: the boundary, effects, guarantees, the transition system, and the specification language. Section 10 is the tool portfolio. Sections 11 to 14 are the parts that make this useful to agents: the feedback loop, the canvas, conformance testing, and the assurance manifest. Section 15 walks the real BestBuds chat graph through the whole thing. Section 16 is the build order.

Two companion documents already cover the ground beneath this one and are cited by identifier rather than repeated:

• Stable Foundations defines the canonical graph IR, the WFStatic predicate family, the closed GraphPatchOp algebra, GraphAuthority, the reference monitor, the eight evidence levels, and the verification portfolio for the kernel (§4, §5, §8, §10, §20, §21).
• Verified Foundations defines the defect register D-1..D-25, the invariant catalogue INV-*, the security stop-ship set S-1..S-12, the power primitives P-1..P-10, and the ladder L0..L5.

This document adds what neither defines: the application-level story. How an app inherits guarantees by composition, where the boundary of what can be checked lies, what an effect is, how a module contributes an invariant as data, how a solver reads the graph, how a counterexample reaches an agent, and what the resulting report looks like.

1. The claim

Reaktor should be a correctness-carrying platform. An application built inside Reaktor's semantic boundary should automatically inherit a set of explicit, mechanically checked guarantees, plus an honest report of exactly which parts of it remain unchecked.

That sentence has three parts, and each one is a design decision.

The graph is the specification. There is no second, handwritten model that drifts from the code. The same graph that the compiler lowers, the runtime activates, and the canvas draws is the object the verifier reads. The visual-language design already commits to this for programs: the AST is not a tree that compiles to a graph, it is the graph (Visual Language §7.2). Stable Foundations commits to it for the kernel: everything outside the kernel is an interpreter, a projection, or an adapter (§3). This document extends it to correctness properties.

Guarantees come from modules, by composition. reaktor-auth knows what "an unauthenticated path to a mutating handler" means. reaktor-work knows what "a retry that repeats a non-idempotent effect" means. Each module states its invariants as data, and an application that composes those modules inherits their checks without writing any. The product dependency rule in Stable Foundations §3.3 is the mechanism: a product cannot weaken kernel well-formedness, skip the reference monitor, or mutate topology outside GraphAuthority.

Verification output is a feedback channel. A failed check is not a red build. It is a structured counterexample that names the invariant, the graph elements, the patch operation that introduced the problem, and what would discharge it. A human sees it highlighted on the canvas. An agent receives it as data and fixes exactly that.

Two things this is not. It is not "integrate a theorem prover into Reaktor". Theorem proving is one engine among several, used late and narrowly (§10). And it is not a claim that applications built on Reaktor are formally verified. The correct sentence is that every guarantee an application carries has a named evidence level, and every part of the application that carries none is marked as such (§14).

2. Why agents change the economics

Formal methods have been too expensive for ordinary software for fifty years. Two things changed in 2026, and Jane Street's essay [1] names both.

The first is that agents move the bottleneck. When an agent can produce a thousand lines in a minute, writing code stops being the constraint and checking it becomes the constraint. Tests sample behaviour. Review samples attention. Neither scales with the volume an agent produces. A formal obligation is different: it covers every input in its domain, it never gets tired, and its verdict is objective.

The second is that agents also lower the cost. Writing a specification, a model, or a proof used to need a specialist. Agents are already competent at all three when the target is small and well-posed. So the price of a formal check falls at the same time the need for one rises. Jane Street reversed a twenty-five-year scepticism on that basis and started a formal methods team.

Jane Street's particular advantage is that it controls its own language, OxCaml, so it can change the language to make verification easier. Reaktor does not control Kotlin. It controls something smaller and more useful for this purpose: the Reaktor IR. Graph, node, port, edge, scope, contract, command, capability, deployment partition. The IR is already data. It already has a mutation language (commands and patches). It already has interpreters (visitors). Making it a specification language is a much shorter step than making Kotlin one.

The bet, stated as plainly as possible:

Reaktor should give agents a representation in which many incorrect changes are unrepresentable, and most of the remaining ones are mechanically refutable, before they reach a human.

Here is the difference in the loop an agent runs. Today, in this codebase:

agent edits Kotlin  →  CI (not running, §3.6)  →  tests (sample)  →  review (missed §3.7)  →  production

With obligations attached to the graph:

agent proposes GraphPatch  →  checker  →  counterexample  →  agent fixes that one thing  →  human approves

The second loop is better for the agent as well as for the reviewer. "Test ChatActorTest.sendsMessage failed" tells an agent almost nothing about the cause. "Invariant INV-AUTH-3 violated; path PublicRoute → handleRealtimeToken → mintToken carries no ChatMembership capability; introduced by patch op 3" tells it exactly what to change. Section 11 defines that message.

3. What exists today

The verification layer described in this document does not exist. What follows is the honest inventory it would sit on. Status words are the corpus's: implemented means shipped and used, partial means shipped but incomplete or unwired, designed means specified in a document, proposed means named in a plan, absent means not found anywhere.

3.1 The effect surface is invisible to the graph

A node can do anything, and the graph does not know. This is the single fact that blocks every guarantee below, and it is why §5 exists.

3.2 Identity, wiring, mutation, validation

3.3 Authority

The best-shaped structured verdict in the codebase is the auth kernel's, and it is not attached to the graph.

• AuthRequirement is a rich, serializable predicate over audience, app, tenant, scopes, permissions, roles, resource, principal kinds, and delegation (reaktor-auth/.../kernel/AuthKernel.kt:222-243). LocalAuthorizer.authorize is a pure function returning Allow or Deny(reason, statusCode, safeMessage) with a typed reason enum (:246-270, 378-411). implemented.
• SecuredProviderPort and SecuredConsumerPort carry requiredScopes and an AuthRequirement as data on the port (reaktor-auth/.../graph/SecuredPort.kt:27-65). Nothing enforces them: connect does not know they exist, and enforceConnectionSecurity and canConnect have zero call sites outside one test (:37, :52). No production node uses providesSecured or consumesSecured. partial, inert.
• Runtime enforcement happens at the HTTP edge in a Spring filter (reaktor-auth/src/jvmMain/.../ReaktorSecurityWebFilter.kt:30-52). SpringRouter routes to handlers with no auth check of its own (reaktor-service/src/jvmMain/.../SpringRouter.kt:21-60). implemented at the edge, absent on the graph.
• PrincipalKind.AGENT exists (AuthKernel.kt:73-76); the default policy excludes it (:232). implemented, unused.

3.4 The agent path

There is no path today from an agent to a graph mutation.

• The desktop MCP server exposes five tools, all reads: list_apps, graph_snapshot, architecture_snapshot, control_plane_snapshot, operation_plan (bestbuds/targets/reaktorDesktop/.../ReaktorDesktopMcp.kt:174-205). An end-to-end test asserts the tool set is exactly those five and that no tool name contains "execute" (.../ReaktorDesktopMcpE2e.kt:84, 90). reaktor-mcp advertises every tool as read-only by construction (reaktor-mcp/.../McpProtocol.kt:38-39, 112-117). implemented, read-only.
• The agent reads one of three snapshot formats, none of which is the editor's GraphDocument: an ad-hoc JSON builder (bestbuds/modules/engine/src/jvmMain/.../ReaktorGraphDocument.kt:42-60), the runtime serializer (reaktor-graph/.../core/GraphJson.kt:15-99), and the C4 architecture snapshot. implemented, fragmented.
• WorkbenchCommand, GraphPatch, Critic, and the graph:apply permission scope exist only in documents. The CommandQueueActor is real but fixture-backed: ApplyAll flips a status string from failed to compiled and touches no graph (bestbuds/modules/engine/.../CommandQueueRepository.kt:40-46). designed.
• Koog is not integrated anywhere. designed.

3.5 Evidence machinery that already exists

Five things in the codebase already have the right shape and should be reused, not replaced.

1. The operations control plane's approval fingerprint. requestRun builds a plan with approvalFingerprint(task, env, target, command, workingDirectory, toolingFingerprint); approval requires a typed confirmation phrase and, for some tasks, an independent second approver; and the executor re-derives the plan and refuses to run if it differs from the approved one (bestbuds/modules/engine/src/jvmMain/.../OperationalControlPlane.kt:117-190, .../OperationExecutor.kt:74-81). This is the closest thing in either repository to a verifier, and it is the spine the mutation broker must reuse (Symphony Plan decision D11).
2. The ten-class TaskEffect lattice from LiveRead to Destructive, classified per task (.../BestBudsOperationalCatalog.kt:1837-1845). Decision D3 makes it canonical for operations and adds an eight-class authoring-effect scale for drafts. The effect vocabulary in §6 must map onto it, not beside it.
3. WiringReport (§3.2). Each entry names graph, owner, port key, port type, and outcome. It is rendered in the workbench Diagnostics drawer (bestbuds/modules/engine/src/jvmMain/.../Workbench.kt:205, 653; .../BottomDrawer.kt:129-260), and GraphWiringHealthTest fails the engine build on any unmatched consumer (.../GraphWiringHealthTest.kt:27-33). That is a counterexample list and a gate, for one invariant.
4. TruthClass and Fact<T> (reaktor-core/.../truth/Fact.kt:3-30): Live, Source, Inferred, Imported, Stale, Partial, Fixture, Failed, Unknown, with provesHealth. The assurance manifest in §14 is a Fact about a claim, and its evidence levels are a refinement of this idea, not a competitor to it.
5. AuthDecision (§3.3) and the tenant-parameterization guard on every Cypher query (reaktor-db/.../graph/GraphDbPolicy.kt:38-58, applied at GraphDb.kt:64, 72). One is a typed verdict; the other is a real, enforced invariant, even if it is a regex rather than a parser.

3.6 Tests and CI

• The reaktor repository has no active CI: both workflow files are entirely commented out, and one is not even under .github/workflows (reaktor/.github/workflows/documentation.yml, reaktor/.github/publish.yml).
• BestBuds CI is workflow_dispatch only; the file says push and pull-request triggers are deliberately absent (bestbuds/.github/workflows/ci.yml:6-23). The Dagger pr gate runs reaktor-core, reaktor-graph, and reaktor-performance JVM tests, the app, design, and engine JVM tests, the app JS tests, and two grep-based architecture tests (bestbuds/.dagger/src/index.ts:195-256). It does not run reaktor-flow tests, the desktop tests, or any Maestro flow.
• Fifteen reaktor modules have zero tests, including reaktor-work, reaktor-cloudflare, reaktor-telemetry, reaktor-mcp, and reaktor-security. There is no property-based testing and no Lincheck anywhere in either repository.
• The one differential harness, FlexBufferHardeningTest, shells out to a C++ oracle for golden and fuzz fixtures (reaktor-flexbuffer/src/jvmTest/.../FlexBufferHardeningTest.kt:20-85). It is the model for §13.
• The "architecture tests" read source text and assert substrings: for example, that the auth runtime graph file contains the literal "requireFullyWired()" (reaktor-auth/src/jvmTest/.../AuthArchitectureTest.kt:38-65; bestbuds/modules/app/src/jvmTest/.../AppArchitectureVitalsTest.kt). They are graph invariants expressed as grep. This document is, among other things, the plan to express them as graph invariants.

3.7 What review did not catch

The strongest argument for this design is the defects that shipped. All fifteen below are present in the BestBuds tree on the scan date, except (h), which the repository's own notes say was fixed in production on 2026-08-05 without a committed migration. Each was written by a human or an agent, passed whatever review existed, and would have been rejected by the one-line invariant beside it. About one commit in eight in both repositories carries agent co-authorship, so this is evidence about the review loop, not about who wrote the code.

Four of these, (a), (k), (l), and (o), are one invariant stated four times. That is the point of §7: the module states it once, and every graph that composes the module is checked against it.

4. One graph, many interpreters

The architecture is a single graph read by several interpreters, one of which is a verifier.

                      Human at the canvas · Agent over MCP
                                      │
                                      ▼
                          ┌───────────────────────┐
                          │     Reaktor Graph      │
                          │                        │
                          │  nodes  ports  edges   │
                          │  scopes  contracts     │
                          │  effects  authority    │
                          │  invariants  partitions│
                          └───────────┬────────────┘
                                      │
          ┌───────────────┬───────────┼────────────┬────────────────┐
          ▼               ▼           ▼            ▼                ▼
      compiler        verifier    simulator    deployment      agent context
      Kotlin/JVM      structural  generated    planner         snapshot +
      JS · native     SMT · Alloy traces       partitions      findings
                      TLA+/Quint  DST          bindings
                      Lean
          │               │           │            │                │
          └───────────────┴─────┬─────┴────────────┴────────────────┘
                                ▼
                             runtime
                                │
                                ▼
                         runtime traces  ──►  model conformance (§13)

Four rules keep this honest.

1. The graph is the model. No verifier input is written by hand beside the code. Invariants, effects, and authority are graph data contributed by modules and applications through the same commands everything else uses. Where a document and the graph disagree, the graph is right, and where the graph and the code disagree, the code is right (Kernel Law 9, "code remains truth").
2. Certifiable facts are finite, total data. Stable Foundations §3.1 already decides this: a facet, policy, effect, or protocol that must be certified is a finite data language, and an opaque executable callback cannot participate in static certification. Every artifact in §6 to §9 obeys it. A Kotlin lambda is not an invariant.
3. No eleventh kernel primitive. The kernel stays at Graph, Node, Port, Edge, Facet, Capability, Visitor, Snapshot, Command, and Event (Graph Kernel). Effects arrive as contract vocabulary, invariants as validator data, findings as visitor results, and the manifest as a visitor output. reaktor-verify is a module like any other and can be removed without touching the kernel.
4. Verification is a return edge, not a gate on a diagram. The kernel's AI command loop, shape 8, already runs GraphSnapshot → AI context → GraphCommand → Validator → PatchPlanner → Compile/Test. It has no edge from Validator back to the agent. Section 11 adds it.

5. The semantic boundary

Reaktor needs a line between the part of a system it can reason about and the part it cannot, and that line must be visible on the graph.

Today a node exposes its coroutine scope, a controller exposes a mutable state flow, an actor's store is globally openable, and twelve Feature slots hand any code a database, a task manager, or a push service (§3.1). As long as that is true, no claim of the form "Reaktor systems are free of X" can be made, because any node can do X behind the verifier's back.

So there are two regions.

The modeled region. A node in this region performs effects only through primitives the graph knows about (§6). It does not receive a raw CoroutineScope. It does not hold a raw MutableStateFlow. It reaches storage, network, time, randomness, secrets, and concurrency through typed handles that it declared, and the declaration is data on the node's contract. Everything the verifier says applies to this region.

The opaque region. Everything else: a Kotlin lambda that does arbitrary work, a third-party SDK, a TypeScript worker outside the Kotlin bundle, a foreign service. Code here is legal. It is marked. It is entered through one door:

opaque("PaymentSDK.charge") {
    stripe.charges.create(...)     // arbitrary Kotlin; the graph records only the label
}

The door has three rules.

• It is an effect. opaque(label) produces the effect Opaque(label) on the enclosing node's contract (§6). It cannot be hidden.
• It contaminates. A guarantee whose proof would have to look inside an opaque block is downgraded to OPAQUE in the manifest (§14), with the label and the assumption that replaces the proof. Contamination is transitive along the effect order, and it stops at a declared assumption: a contract such as StripeContract that states what the block is assumed to do.
• It is the only door. Raw scope, raw state, and Feature resolution from inside a modeled node are compile errors once the modeled node type exists, and findings until then.

This is not new to the corpus; it is the generalisation of three existing precedents. Stable Foundations §7.1 allows an explicitly labeled unsafe or partial activation in development that must never be confused with a certified snapshot. The flexbuffer design keeps the unchecked fast readers behind a validation obligation, so untrusted bytes first become a validated payload (Essays, Codex; Stable Foundations §14.1). The FFI design keeps an untyped cells.dynamic surface and calls it the escape hatch (FFI §6). One construct, one word, everywhere.

5.1 The modeled node

The concrete change is a node type that cannot reach the invisible channels.

abstract class ModeledNode(graph: Graph) : Node(graph) {
    // no coroutineScope, no MutableStateFlow, no Feature.* in scope

    protected fun <S> state(initial: S): StateHandle<S>           // Read/Write(State)
    protected fun <T : Request> call(endpoint: ServiceEndpoint<T>): CallHandle<T>   // Call(endpoint)
    protected fun <M> mailbox(key: ActorKey<M>): MailboxHandle<M>  // Emit(mailbox)
    protected fun store(descriptor: DataDescriptor): StoreHandle    // Read/Write(store)
    protected fun timer(): TimerHandle                               // Timer
    protected fun clock(): ClockHandle                               // Clock
    protected fun random(): RandomHandle                             // Random
    protected fun secret(name: SecretName): SecretHandle             // Secret(name)
    protected fun <R> opaque(label: String, block: () -> R): R       // Opaque(label)
}

Every handle constructor records an effect on the node's contract. There is no other way to obtain one. StateInteractor (§3.1) is the existing precedent: private state, a read-only view, a protected reducer. ModeledNode is that discipline applied to every effect channel.

Today's Node stays exactly as it is during migration and becomes the opaque region by definition: a legacy Node is a node whose whole body is one Opaque effect. The refinement plan already names ChatGraph as the pilot for the port-shape work (Graph Refinement Plan); it is the pilot for this too (§15).

5.2 What the canvas shows

The boundary is only useful if people can see it. For a scope, the canvas shows the rollup:

Checkout

  graph.referential-integrity       by construction
  auth.protected-mutations          bounded-model-checked   scope 6
  secret.partition-isolation        runtime-checked
  deploy.binding-parity             runtime-checked
  order.state-machine               bounded-model-checked   states ≤ 10⁶
  PaymentSDK.charge                 OPAQUE   assumes StripeContract
  AnalyticsNode                     OPAQUE   legacy Node

That is more honest and more useful than a green tick on the whole application.

6. Effects and capabilities

An effect is what an action does. A capability is what a component is allowed to do. Reaktor needs both, as data, and needs the rule that an effect can only happen by discharging a capability.

6.1 The effect vocabulary

The kernel design already has OperationContract.effects: Set<EffectKind>, NodeSpec.effects, and PortContract.effects as fields with no vocabulary (Graph Kernel §kernel; Stable Foundations §4). This is the vocabulary. It is deliberately small; everything a module adds is an attribute or a store name, not a new kind.

Each effect carries attributes, and the attributes are what the invariants actually consume:

• idempotent: Boolean, default false. The shadow-environment design already decides the default: an unannotated handler is non-idempotent (Shadow §9). This attribute is what defect (d) and the retry invariants in §7 read.
• reversibility, one of the ten TaskEffect classes for operations or the eight authoring-effect classes for drafts (decision D3). The graph's visible effect for a scope is the maximum transitive effect, as D3 states.
• scope: the tenant and the deployment partition the effect touches. Defect (l) is an effect whose tenant scope is not derived from the authorization predicate.
• durability: fireAndForget, atLeastOnce, effectivelyOnce. The corpus's delivery table applies (Distributed Actors §14); nothing may claim exactly-once.

Clock and Random are separate kinds, rather than one "nondeterminism" kind, because deterministic simulation (§13) must virtualise each independently and the shadow replay must read each from the captured envelope.

6.2 Capability offers, grants, decisions, effects

Stable Foundations §10 already forbids collapsing four things into one word: a capability offer (what a component can provide), an authority grant (permission for a principal to request an effect in a context), a policy decision (the reference monitor's verdict), and an effect (what happened). And reaktor-core §3 warns that none of Reaktor's existing "capability" meanings is object-capability security: they grant no authority.

This section sharpens §10 into a typing discipline rather than adding an axis:

A node's contract declares   effects(n)        what its actions do             (§6.1)
The graph's authority data   grants(n, ctx)    what n may request in a context (GraphPatchOp.GrantAuthority)
The rule                     ∀ e ∈ effects(n): ∃ g ∈ grants(n, ctx) covering e
Non-amplification            grants(after) ⊆ grants(before) ∪ ApprovedExplicitGrants   (Stable Foundations §10.2)
At runtime                   an effect is produced only by a handle obtained through a declared effect (§5.1)

With those two sets on the graph, the checker can ask questions that no amount of code review answers reliably:

1. Does every effect a node declares have a grant that covers it?
2. Can a Secret(name) flow into a node whose partition is browser?
3. Can a node write a store owned by another node?
4. Can two actions that may run concurrently both Write the same store outside an actor?
5. Can a public route reach an effect that requires an authenticated principal? (Defects a, f, k.)
6. Can a Timer or a queue redelivery repeat an effect whose idempotent attribute is false? (Defects d, i.)

Quint's effect system is worth studying for the same reason it was built: it tracks reads and updates of state separately from types, and it guarantees each variable is updated exactly once per step [5]. Reaktor should borrow the idea, not the syntax.

7. Guarantees as data

A module states its invariants as data, the graph carries them, and every application that composes the module is checked against them. This is what "inherits guarantees" means mechanically.

7.1 The vocabulary

Six small types. They are visitor results and validator data, not kernel primitives.

data class Invariant(
    val id: InvariantId,             // "INV-AUTH-3": the catalogue identifier, stable forever
    val statement: String,           // one plain sentence
    val formula: Formula,            // §9: solver-readable, never a lambda
    val scope: InvariantScope,       // Static | Transition | Temporal | Refinement
    val required: EvidenceLevel,     // the minimum level a release needs
)
data class Assumption(val id: String, val statement: String, val about: ElementRef)   // what replaces a proof at an opaque edge
data class Obligation(val invariant: InvariantId, val subject: ElementRef, val introducedBy: PatchOpRef?)
sealed interface Evidence { val level: EvidenceLevel; val engine: String; val bounds: Bounds?; val artifact: ArtifactRef }
sealed interface Verdict { data class Holds(val evidence: Evidence) : Verdict; data class Fails(val finding: Finding) : Verdict }
data class OpaqueBoundary(val element: ElementRef, val label: String, val assumption: Assumption?)

EvidenceLevel is the eight-level scale that Stable Foundations §1 makes binding, in its order: TypeEnforced, RuntimeChecked, PropertyTested, ConcurrencyTested, BoundedModelChecked, MechanicallyProved, TranslationValidated, OperationallyAttested. Two more states, Opaque and Unverified, are not levels; they are the absence of one, and they are the two states this document adds (§14).

7.2 Where they live

The module interface already has the slot. ReaktorModule declares facets(), capabilities(), contracts(), validators(), visitors(), commandHandlers(), renderers(), inspectors(), codegen(), and runtimeAdapters() (Graph Kernel §module-model). Today a validator is a function. It becomes a function with an identity:

interface GraphValidator {
    val invariant: Invariant
    fun check(snapshot: GraphSnapshot): Verdict          // the deterministic engine, always available
    fun obligations(patch: GraphPatch): List<Obligation> // what this patch must discharge
}

The prose twin is the per-module SPEC.md that Verified Foundations L1 already prescribes, containing that module's section of the INV-* catalogue. The rule is: every Invariant.id in code appears in a SPEC.md, and every SPEC.md entry has a validator. A test that defends an invariant cites its id.

7.3 What each module contributes

The table uses the catalogue identifiers where they exist and proposes new families where they do not.

An application adds its own invariants in the same shape. INV-CHAT-1 in §15 is one. But the point of the table is that a product gets the module rows for free.

8. Mutation as a transition system

Every change to a Reaktor graph should be a transition in a system with stated laws, so that the question "can this change break a guarantee" has a mechanical answer.

8.1 Which patch

The corpus has two types called GraphPatch, and this document must say which one the laws are stated over.

• The visitors design defines a four-case value, ConnectPort, AttachNode, SetAttribute, Composite, applied through Graph.apply(patch, dryRun) and returning findings (Graph Visitors). The control-plane design calls it the canonical mutation value.
• Stable Foundations §8 defines a closed, versioned algebra: GraphPatch(patchSchemaVersion, patchId, graphId, expectedRevision, expectedBaseDigest, operations, intent) over a GraphPatchOp set that covers every field of GraphState, including protocols, policies, facets, and authority grants.

The laws below are stated over the second. It is the only one closed over the whole state, and closure is what makes "every legal patch preserves the invariants" a finite statement. The first is a projection of the second: ConnectPort is AddEdge, AttachNode is AddNode plus its ports, SetAttribute is ReplaceFacet. The editor's GraphCommand set in reaktor-flow (§3.2) is a third projection, over the document rather than the runtime state; it maps one-to-one onto the algebra and should be regenerated from it rather than maintained beside it. That resolves the naming conflict without discarding either design.

8.2 The laws

For a state S, a patch operation op, and the operation's independent precondition Pre_op:

(Preservation)   WFStatic(S) ∧ Pre_op(S)        ⇒  WFStatic(apply(op, S))
(Transition)     WFStatic(S) ∧ Pre_op(S)        ⇒  ValidTransition(S, planInput, op, apply(op, S))
(Failed no-op)   ¬Pre_op(S)                     ⇒  apply(op, S) = S
(Patch)          a patch op₁ … opₙ commits only if every step holds; otherwise S′ = S

WFStatic(S)  =  ⋀ { INV(S) : INV ∈ SPEC(m), m installed, INV.scope = Static }

Three constraints from the foundation documents apply and are worth restating because they are easy to get wrong.

• WFStatic is the conjunction of module invariants, and only the static ones. Stable Foundations §5 splits validity into WFStatic, ValidTransition, WFActivation, RuntimeInv, ProtocolSafety, NormalizeLaws, and ReconciliationInv on purpose. This document's Valid(G) is WFStatic; the transition, activation, protocol, and reconciliation obligations stay separate and are discharged by different engines (§10).
• Pre_op is independent. Stable Foundations §20.1 forbids defining validity as "apply, then check WFStatic", which would make the preservation theorem a tautology. Each operation states what it needs before it runs. The editor commands already do this correctly in the small: AddEdge checks that both nodes exist and that the ports have the right roles before it copies the document (GraphCommands.kt:81-99). What they lack is the global conjunction.
• The principal is not in the patch. The authenticated principal comes from the reference monitor's context, never from a caller-authored field (§8, step 1).

8.3 Where the obligations plug in

GraphAuthority (Stable Foundations §8) is a nine-step plan, validate, commit protocol. This document's obligations are step 4, "run static, transition, contract, policy, lifecycle-plan, and migration validators", made concrete:

1. AuthenticatedPlanInput   principal, patch, versions, evidence snapshot, expiry
2. read snapshot r          verify graph id, revision, base digest
3. normalise + apply        in memory, per-op independent preconditions
4. obligations              ⋃ validator.obligations(patch)  →  verdicts        ◄── §7, §9, §10
5. PatchPlan                diff, findings, effects, safety class, approvals, rollback
6. approvals                bound to the complete plan fingerprint             ◄── same shape as OperationalControlPlane (§3.5)
7. atomic commit            snapshot r+1, digest, journal, certificate
8. publish                  readers see r or r+1, never a partial patch
9. reconcile                runtime activations follow the committed snapshot

Step 4 returns a list of verdicts. A Fails verdict is a Finding (§11) and the plan cannot reach step 6. Bounded engines (Alloy, SMT, TLC) run at step 4 only for the invariants a patch's obligations touch; the deterministic engine runs for all of them, every time.

8.4 What changes in the editor first

The editor's GraphCommand set is the cheapest place to make this real, because it is already pure and already transactional (§3.2). Four changes:

1. Add validate(document): List<Finding> and call it after every apply in GraphEditorSession.execute, rejecting on any Error finding. Start with five invariants: edges reference existing nodes, edges run provider to consumer, contracts are compatible, scope containment is acyclic, and a consumer has at most one edge.
2. Make AddEdge compare DocPort.type across the edge. Today it checks roles only.
3. Replace GraphCommandException(message: String) with a Finding.
4. Put :reaktor-flow:jvmTest in the CI gate. It is not there today (§3.6).

Then run the Alloy experiment in §16 against the same five invariants.

9. The specification IR

An invariant must be written in a language a solver can read. A Kotlin lambda is not one.

The premise is already decided (Stable Foundations §3.1): a fact that must be certified is a finite, total data language. Invariants are such facts. So Reaktor needs a small formula language, built by a Kotlin DSL at authoring time, stored on the graph as data, and consumed by every engine in §10.

9.1 The language

Formula  :=  Atom
          |  Not(F)  |  And(F, F)  |  Or(F, F)  |  Implies(F, F)
          |  Forall(sort, x, F)  |  Exists(sort, x, F)
          |  Always(F)  |  Eventually(F)  |  Until(F, F)          -- temporal fragment, protocol specs only

Atom     :=  Rel(name, term…)                                     -- edge(a,b) provides(n,p) grants(pr,e) reaches(a,b)
          |  Eq(term, term)  |  In(term, set)  |  Card(set) ⋈ n

Term     :=  Var  |  Const(id)  |  Fn(name, term…)                -- fingerprint(p) scope(n) effects(n) partition(n) owner(s)

Sorts    :=  Node  Port  Edge  Scope  Contract  Principal  Effect  Store  Partition  Route

Relations come from two places. Structural relations (edge, provides, consumes, contains, partition) are read from the snapshot. Semantic relations (reaches, grants, requires, owns, mutates) are contributed by modules as derived relations, each with its own finite definition. A module that contributes a relation contributes the visitor that computes it.

Identity in the IR is by fingerprint, the content-derived digest that Verified Foundations §12 makes the keystone P-1 and that Kernel Law 2 calls ContractId. Not the simple-name string of today's Port.Type, not the full KType, and not a hand-typed label. This is the one identity both foundation documents endorse, and it is the reason INV-PORT-1 cannot be stated until D-6 is closed.

9.2 The DSL

The Kotlin surface is deeply embedded: it records a formula, it does not evaluate one.

val protectedMutations = invariant("INV-AUTH-1", scope = Static, required = BoundedModelChecked) {
    forall<Route> { route ->
        forall(reachableHandlers(route)) { handler ->
            handler.effects.any { it.mutates } implies handler.requires(Authenticated)
        }
    }
}

val membershipReads = invariant("INV-AUTH-3", scope = Static, required = RuntimeChecked) {
    forall<Node> { n ->
        forall(n.effects.filter { it.tenantScoped }) { e ->
            exists(n.consumes) { port -> port.contract.isMembershipFor(e.tenant) }
        }
    }
}

val retrySafety = invariant("INV-WORK-1", scope = Temporal, required = BoundedModelChecked) {
    always(forall<WorkRun> { run -> run.attempts <= 1 or run.effect.replaySafe })
}

Here replaySafe means the declared effect protocol has evidence for this retry: an intrinsically idempotent effect, an atomic deduplication boundary, or reconciliation that proves retry eligibility. A boolean declaration alone supplies no guarantee.

Two properties of the DSL matter more than its syntax. Every combinator produces Formula data, so the same invariant is what the deterministic checker evaluates, what the Alloy translator emits, what the Quint translator emits, and what the manifest prints. And nothing in the DSL accepts an arbitrary (Graph) -> Boolean. If a property cannot be written in the IR, it is not an invariant; it is a test, and it goes in the property-test layer of §10 with the evidence level that implies.

The IR does not replace the visual language's own semantics. The typing judgments, the small-step rules, and the purity discipline in Visual Language §7 define what a program means. This IR states properties about graphs, including program graphs. Verified Foundations §9.2 already names transcribing §7.5 to §7.6 into Lean as the cheapest proof target; that proof is about the semantics, and the invariants here are about the structures the semantics run over.

10. The verification portfolio

No single tool fits every property. The portfolio is organised by the class of claim, not by phase, and each engine publishes its bounds.

Four notes on the choices.

The deterministic pass comes first, always. Do not invoke a solver to learn that an edge points at a node that does not exist. Reference, type, cardinality, scope, ownership, capability coverage, serialisation compatibility, and partition placement are cheap, exact, and run continuously in the canvas. Most of the fifteen defects in §3.7 fall to this engine alone.

SMT is the new rung, and it has to earn its place. The corpus's decided portfolio is Lean, TLA+ with Apalache, Alloy, Lincheck, and property, fuzz, and differential testing (Stable Foundations §20; Verified Foundations Appendix B). SMT appears nowhere in it. The case for adding it is Jane Street's Z3 note [2]: they did not prove a compiler, they asked Z3 whether specific rewrites preserved meaning and got counterexamples when they did not. Reaktor has the same shape of problem in partitioning, route lowering, port fusion, constant propagation, capability rewrites, generated deployment configuration, and schema migration. Alloy is the better tool for pure relational structure and gives visual counterexamples; SMT is the better tool once arithmetic, bit-vectors, arrays, quotas, version numbers, or capacity enter the property. KSMT [4] is the reason it is affordable: a Kotlin and JVM API over four solvers with process isolation and a solver-independent expression layer, which fits the JVM build. It lives behind reaktor-verify-smt, and no solver type leaks into any Reaktor public API.

Alloy first, TLA+ second, Lean last. Alloy is almost comically well matched to a relational IR (§9.1), and its counterexamples are small graphs that the canvas can render directly. Practical Alloy's structural and behavioural chapters are enough to build the first prototype [8]. TLA+ or Quint apply to the runtime primitives, not to applications at first: graph lifecycle, hot replacement, service retry, actor delivery, background work, client and server version skew, offline sync, deployment, patch transactions, and concurrent multi-agent editing. Once a primitive is correct, every application on it benefits. Lean comes last and narrowest, for the pure targets Verified Foundations §9 already ranks; there is no Lean-to-Kotlin toolchain and none is coming, so a Lean result is a verified reference with a conformance binding, never a proof of the Kotlin.

Every gate is non-vacuous and publishes its trusted base. Stable Foundations §20.8 and §20.9 apply verbatim: satisfiable witnesses alongside every check, mutated counterexamples that the gate must catch, scope and solver and seed recorded, reject-all and deny-all cannot pass, and every proof package lists what it trusts. A bounded result is reported as "no counterexample within the stated bound", never as "proved".

Sequencing follows the ladder. This document adopts Verified Foundations §8 as normative: L0 hygiene before anything (there is no CI today), L1 written invariants, L2 Lincheck and property and differential testing, L3 model-checked protocols, L4 Lean, L5 simulation. The portfolio above is which engine handles which claim; the ladder is when each becomes worth running. Codex's Stable Foundations §24 schedules Alloy and Lean scaffolding earlier and in parallel; the difference is one of calendar, not of tool, and the Alloy experiment in §16 is compatible with both.

11. The agent loop

A verification result should reach an agent as data it can act on, not as a red build it has to interpret.

11.1 The pipeline

Claude · Codex · Koog
        │
        ▼
proposed GraphPatch                (structured output; never prose, never a raw diff)
        │
        ▼
schema and type validation         (reject malformed patches before any semantics)
        │
        ▼
affected obligations               ⋃ validator.obligations(patch)
        │
        ├── deterministic passes   (always)
        ├── SMT                    (when an obligation's formula needs a theory)
        ├── Alloy / TLC / Apalache (when an obligation is universal or temporal)
        └── generated traces       (when a runtime primitive is touched)
        │
        ▼
VerificationReport                 verdicts, findings, evidence, manifest delta
        │
   ┌────┴────┐
 holds     fails
   │          │
   │          └──► Finding with witness ──► agent revises the patch ──► (bounded retries)
   ▼
PatchPlan → approval → commit      (GraphAuthority, §8.3; the OperationalControlPlane spine, §3.5)

This is the kernel's AI command loop with its missing return edge. The semantic constitution in bestbuds/AGENTS.md §2.2 already states the target path in one line: snapshot or query, proposal, typed patch or command, normalise and validate, fingerprinted plan, authority and policy and approval, execute, reconcile, receipt. The loop above is that sentence with the validate step opened up.

11.2 The finding

The carrier is the existing Finding shape from the visitors design, with its stable string codes, extended rather than replaced. New codes are additive; renames are breaking.

data class Finding(
    val code: String,                 // stable: "auth.path.unauthenticated", "effect.retry.nonidempotent"
    val severity: Severity,
    val message: String,
    val hint: String?,
    val cause: Throwable?,
    // added by reaktor-verify
    val invariant: InvariantId,       // "INV-AUTH-3"
    val elements: List<ElementRef>,   // the nodes, ports, edges, scopes involved
    val witness: Witness?,            // Structural(subgraph) | Trace(steps) | Model(assignment)
    val introducedBy: PatchOpRef?,    // which operation in the proposed patch created the violation
    val missing: List<Requirement>,   // what would discharge it: a capability, an edge, an attribute
    val bounds: Bounds?,              // scope, steps, solver, seed for bounded engines
)

Rendered for an agent, a finding for defect (a) looks like this:

finding        auth.path.unauthenticated                       severity ERROR
invariant      INV-AUTH-3   a tenant-scoped effect consumes a membership capability for that tenant
elements       route:/realtime/token → node:handleRealtimeToken → effect:Emit(realtime:connect, room)
witness        structural   [PublicRoute, handleRealtimeToken, mintDelegatedToken]  (3 nodes, 2 edges)
introducedBy   op 3   AddNode(handleRealtimeToken)
missing        ConsumerPort<ChatMembership>   an edge from handleRealtimeToken to a provider of ChatMembership(room)
engine         deterministic   exact

Every field is machine-readable, and missing is the field that makes the loop converge: the agent's next patch is usually "add exactly that". A temporal finding carries a Trace witness instead, a list of steps with the state after each, and the canvas animates it (§12).

Call these proof obligations attached to diffs. "Proof-carrying code" would overclaim unless Reaktor is shipping machine-checked certificates, which it is not.

11.3 How agents reach it

The agent-facing surface is the MCP server that exists (§3.4), extended in the order the Symphony Plan already fixes.

• Read first. graph_snapshot gains a findings field and a manifest field. An agent can see today's verdicts without proposing anything. This needs no new permission.
• Propose second. A propose_patch tool that runs the loop in §11.1 through step "VerificationReport" and returns it, without committing. Decision D11 puts the MCP mutation broker at Gate 4, behind the same requestRun, plan, approval spine the desktop uses. This tool is that broker's dry-run half and can ship first, because it mutates nothing.
• Apply last, and not by the agent that proposed. The Critic gates by withholding approval and never applies (Control Plane §change). graph:apply is a scope a principal holds, and the default auth policy excludes PrincipalKind.AGENT today (§3.3); enabling it is a policy patch, reviewed like any other.
• Retries are bounded. A proposing agent gets a fixed number of revisions per obligation before the plan is escalated to a human with the full finding history. Unbounded agent-verifier loops are how a system burns a budget on a property it cannot satisfy.

Why this beats the status quo is not subtle. In the loop of §2, a failing test tells the agent that something is wrong. A finding tells it which invariant, which elements, which of its own operations, and what is missing. The first invites guessing; the second invites a one-line fix. And because the invariants are universal over their domain, an agent cannot satisfy the checker by making the tests pass.

12. The canvas as the verification interface

A counterexample should be drawn, not printed. Reaktor already has the drawing.

Traditional formal tools show a counterexample as a list of states. Reaktor already holds the application's structure as a graph and already renders it in reaktor-flow and the workbench Graph pane, so a structural witness is a highlighted subgraph: three nodes and two edges, with the missing edge drawn dashed and labeled with what would discharge the finding. A temporal witness is an animated path:

t0   WorkRun created
t1   job dequeued
t2   request sent
t3   worker crashes
t4   job dequeued again
t5   duplicate charge                ✗  INV-WORK-1

The seed already exists. The Diagnostics drawer renders the wiring report per entry with stable row identifiers (§3.5), and the header pill counts findings. Findings from §11 land in the same drawer with the same shape; a click selects the witness on the canvas. Alloy's own visualiser is the model for structural witnesses [7]; Quint's ITF trace format is the model for temporal ones [5].

The consequence worth stating: the human interface, the agent interface, and the formal model's interface become one object. A reviewer sees the same finding the agent received, on the same graph the agent proposed to change. That is why the visual-language design says an agent needs no special API; it reads the snapshot, proposes patches, and reads findings, exactly as the editor does (Visual Language §11).

The Symphony Plan's decision D4 still applies: the shipped canvas says Inspect and Map until the mutation proof passes. Findings are inspection. They ship before editing does.

13. Closing the gap between model and implementation

A model check proves the model. It does not prove the Kotlin. Reaktor controls the runtime, so it can close that gap more cheaply than most systems.

Two directions, both already named in the corpus under other headings.

Model to implementation. Generate traces from the checked model and replay them against the real system. Quint's model-based testing does exactly this: the model emits traces in ITF format, and a small library replays each action against the implementation and compares state after every step [5]. Reaktor's version replaces hand-written acceptance lists with generated ones. The acceptance tests linked from Work are the first target: write the WorkRun state machine in Quint, check INV-WORK-1..4, generate a few thousand traces, and drive the real TaskManager through them via its adapters. The FlexBufferHardeningTest harness (§3.6) is the existing precedent for the shape: one external oracle, many generated fixtures, machine-checked agreement.

Implementation to model. Take traces from staging or production and ask the model whether each observed transition is one it permits. This is the direction that catches drift after the fact. It needs two things that do not exist today: GraphTelemetry emits no span for a graph mutation or a port invocation, only for wiring changes and navigation (reaktor-telemetry/.../GraphTelemetry.kt:61-92), and no OpenTelemetry exporter is configured anywhere (.../TelemetryAdapter.kt:12-19). Once mutation and invocation spans exist, a trace is a sequence of effects with their attributes, and conformance is a visitor over that sequence and the model.

The comparison vocabulary is the shadow environment's, reused rather than reinvented: Strict byte equality after canonicalisation, Shape with stable fields, Statistical within tolerance, and Side-effect classification (Shadow Dev Environment §18). Shadow replay compares a replay against a capture; conformance compares a capture against a model; the diff language is the same.

Two words are reserved and must not be used loosely. Sampled agreement between model and implementation is model-based conformance, evidence level PropertyTested. Translation validation means an independent checker run on every generated artifact against its exact certified source (Stable Foundations §20.7), and nothing in this section reaches it.

Deterministic simulation, L5, is where the two directions meet: the whole product on virtual time, every effect kind in §6 virtualised, a seed driving reordering and faults, and every trace checked against the model as it runs. Reaktor is unusually placed for this because all input and output already pass through adapters and the system's structure is already data. It is the capstone, and it is last.

14. The assurance manifest

The output of all of this is a machine-readable statement of what is claimed, at what level, with what evidence, and what is not claimed at all.

The corpus already has the human-readable form: the claim template in Stable Foundations §22 (subject, claim, evidence, assumptions, implementation link, artifact, limitations) and the VerificationAttestation that §30 asks CI to produce. This section gives it a schema and two states the template lacks.

subject: bestbuds.chat                   # a graph, a scope, or a node; content-addressed
revision: 1842
digest: sha256:9f3c…                     # of the certified snapshot
kernel: { version: 0.9.2, normalizer: 3, registry: sha256:… }
claims:
  - id: INV-GRAPH-3
    statement: no two live nodes share an identifier
    level: type-enforced                 # one of the eight levels, Stable Foundations §1
    method: by-construction
    engine: kotlin
    bounds: none
  - id: INV-AUTH-1
    statement: a mutating handler is reachable only through an authenticated route
    level: bounded-model-checked
    method: alloy
    engine: { name: alloy, version: 6.1.0, solver: sat4j }
    bounds: { scope: 6, bitwidth: 4 }
    non-vacuity: { satisfiable-witnesses: 3, mutated-counterexamples-caught: 5 }
    assumptions: [ AuthAdapterConformsToAuthContract ]
    artifact: verify/alloy/INV-AUTH-1.als@sha256:…
  - id: INV-WORK-1
    statement: a retry requires a qualified replay-safe effect protocol
    level: bounded-model-checked
    method: quint-apalache
    bounds: { workers: 3, retries: 5, length: 20 }
    conformance: { method: model-based, traces: 50000, level: property-tested }
  - id: chat.realtime-token.membership
    level: unverified
    reason: obligation INV-AUTH-3 fails; see finding f-2231
opaque:
  - element: chat-service.onBeforeConnect
    label: TypeScript outside the Kotlin bundle
    assumption: ChatMembershipContract
  - element: AnalyticsNode
    label: legacy Node; whole body is Opaque
trusted:
  - lean kernel 4.x
  - kotlin compiler 2.3 and the JVM, JS, native backends
  - cloudflare workers runtime
  - postgres transaction semantics as relied upon
  - build provenance and signing

Rules for the manifest:

• Levels are the corpus's eight. type-enforced, runtime-checked, property-tested, concurrency-tested, bounded-model-checked, mechanically-proved, translation-validated, operationally-attested. Nothing is written as "verified" without one of them.
• opaque and unverified are the two states this document adds. opaque means the subject sits outside the boundary of §5 and carries an assumption instead of evidence. unverified means it is inside the boundary and an obligation is failing or has not been run. They are different situations and must be reported differently. opaque is a design decision; unverified is work.
• Bounds and non-vacuity are mandatory for bounded engines. A bounded claim without its scope is not a claim.
• The trusted base is listed and expected to shrink. Stable Foundations §20.9.
• The manifest is a visitor output, content-addressed to the snapshot digest. A manifest for revision 1842 says nothing about revision 1843. CI regenerates it on every commit; the canvas shows the delta a patch would cause before the patch commits (§11.1).

For the canvas, a five-badge rollup is convenient: PROVED for mechanically-proved and translation-validated, CHECKED for bounded-model-checked and concurrency-tested, TESTED for property-tested and operationally-attested, OPAQUE, and UNVERIFIED. The badge is a display projection. The record is the eight-level entry, and it is what an agent reads.

15. Worked example: BestBuds chat

This section runs the real chat feature through everything above, so that the design is judged on a graph that exists rather than on a diagram.

15.1 The graph today

ChatGraph is a Kotlin class extending Graph, declared with the other feature graphs in one file (bestbuds/modules/app/src/commonMain/.../BestBuds.kt:130-182). Its shape, from the code:

ChatGraph                                            runs on: Android, iOS, desktop
  MessageRepository          RepositoryNode over "message_store"; consumes UserRepository, MessagingApi
  ChatSessionOperations, ChatSessionState, ChatTimeline, ChatAnalytics   interactors
  ChatSocketInteractor       provides ChatSocketInteractor; consumes ChatActors.Session
  ChatTypingInteractor       consumes ChatActors.Session
  ChatActor                  ActorNode<ChatMsg>; consumes six named ports
  ChatListInteractor, ChatSessionInteractor          consume ChatActors.Session (+ StickerRepository)
  routes  /chats  /chats/{id}  /chats/profile/friend/{id}  /chats/profile/group/{id}
  screens ChatScreen, ChatListScreen
  autoWire()

MessagingServiceNode (root)   provides MessagingApi; MessagingRequest is the shared wire contract
chat-service (Cloudflare DO)  ChatService.kt behind a 137-line TypeScript PartyServer shell
messaging-service (worker)    Postgres through Hyperdrive
bot-service (worker)          reached from the DO over a service binding

Wiring is autoWire(), which silently skips any consumer it cannot match (§3.2). The DO, the messaging worker, and the bot are outside the client graph entirely; the Kotlin inside them is real, but the TypeScript shell around the DO (bestbuds/targets/chatServer/src/index.ts:10-36) is not Kotlin at all.

15.2 The invariant

reaktor-auth contributes INV-AUTH-3 (§7.3): a tenant-scoped effect consumes a membership capability for that tenant. BestBuds instantiates it once for chat, as application data:

val chatMembership = invariant("INV-CHAT-1", scope = Static, required = RuntimeChecked) {
    forall<Node> { n ->
        forall(n.effects.filter { it.tenant == ChatRoom }) { e ->
            exists(n.consumes) { p -> p.contract == fingerprint<ChatMembership>() && p.boundTo(e.tenantId) }
        }
    }
}

Every read of messages, every reaction, every realtime token, and every bot fan-out for a room is a tenant-scoped effect on that room. One sentence, four defects (a, k, l, o).

15.3 The patch and the finding

Suppose an agent proposes the realtime-token handler as it exists today: a node that consumes AuthContext, checks that the requested context equals the room, and emits a delegated realtime:connect token (ChatService.kt:146-184). As a patch:

op 1  AddNode      handleRealtimeToken   effects: [Read(AuthContext), Emit(realtime:connect, tenant=room)]
op 2  AddEdge      route:/realtime/token → handleRealtimeToken
op 3  AddEdge      handleRealtimeToken.auth ← AuthNode.context

The deterministic pass evaluates INV-CHAT-1 over the snapshot after the patch and returns the finding shown in §11.2: the emit effect is tenant-scoped, the node consumes no ChatMembership port, introducedBy is op 1, and missing is a consumer port for ChatMembership(room) wired to a provider. The plan cannot reach approval.

The agent's revision is the fix a reviewer would have asked for, had a reviewer noticed:

op 4  AddPort      handleRealtimeToken.membership : ConsumerPort<ChatMembership>
op 5  AddEdge      handleRealtimeToken.membership ← MembershipRepository.forRoom

The pass re-runs. INV-CHAT-1 holds for the node. Defects (k) and (l) are the same finding on the messaging worker's read and reaction handlers, and (o) is a second finding under INV-AUTH-4, delegation narrows, because the bot read runs under a service credential with wider grants than the mentioning user holds.

15.4 The boundary

Not everything in chat can be checked, and the manifest says so. The PartyServer onBeforeConnect gate is TypeScript; it is opaque, with the assumption ChatMembershipContract that states what it is assumed to enforce. The Postgres transaction semantics the messaging worker relies on are in trusted. ChatActor is a legacy Node today, so its body is one Opaque effect until it is migrated to ModeledNode; the refinement plan already makes ChatGraph the pilot, and after migration its state, its mailbox, and its timers are declared effects.

15.5 What the manifest says

bestbuds.chat @ r1843

  INV-GRAPH-3   identifiers unique                     type-enforced
  INV-PORT-3    consumer exclusivity                    runtime-checked
  INV-CHAT-1    membership on every room effect         runtime-checked      (was: unverified, f-2231)
  INV-AUTH-1    authenticated mutating routes           bounded-model-checked  alloy scope 6
  INV-AUTH-4    delegation narrows                      unverified           f-2232 bot fan-out
  INV-SVC-3     mutating requests declare idempotency   unverified           MessagingRequest lacks the attribute
  chat-service.onBeforeConnect                          opaque               assumes ChatMembershipContract
  ChatActor                                             opaque               legacy Node, migration pending

Two rows are red and two are opaque. That is a truthful description of the chat feature on the scan date, and it is more useful to the next engineer, human or agent, than either "tests pass" or "formally verified".

16. What to build, in what order

Ten steps. Each names its ladder rung from Verified Foundations §8 and an exit signal that either holds or does not.

0. Close the stop-ship set. S-1 to S-12, Verified Foundations §7 and Phase 0. A verification program over an exploitable plane is decoration. Defects (a), (b), (c), (d), (e), (f), (g), (i), and (j) in §3.7 are on that list. Exit: no unauthenticated route mutates state; membership is enforced on every chat read and write.
1. L0 hygiene. CI on every push in both repositories, binary-compatibility dumps, tags, and the reaktor-graph-core extraction. Add :reaktor-flow:jvmTest and :reaktorDesktop:test to the gate. Exit: a red build blocks a merge.
2. The guarantee vocabulary as code. Invariant, Assumption, Obligation, Evidence, Verdict, OpaqueBoundary, EvidenceLevel, and the Finding extension (§7.1, §11.2). Extend GraphValidator with an identity. Write SPEC.md for reaktor-graph, reaktor-auth, reaktor-db, reaktor-service, reaktor-work with their INV-* sections. L1. Exit: every invariant id in code appears in a SPEC.md, and every entry has a validator.
3. Make the editor globally invariant-preserving. The four changes in §8.4, then the Alloy experiment below. L1 and L2. Exit: GraphEditorSession.execute rejects a document that violates any of the five structural invariants, with a Finding, and Alloy has produced at least one counterexample that changed a command.
4. The effect IR and the modeled node. EffectKind with attributes (§6.1), ModeledNode (§5.1), the opaque door, and declared effects on NodeSpec, PortContract, and OperationContract. Migrate ChatGraph as the pilot. L1. Exit: ChatGraph contains no legacy Node; every effect in it is declared; the manifest for bestbuds.chat has no opaque row for a Kotlin node.
5. Module guarantees. Turn the inert secured ports on at wire time so INV-AUTH-1 and -3 are enforced by connect; add ownership and policy-edge checks to reaktor-db; add the idempotent attribute and the sealed-status rule to reaktor-service; add binding parity to reaktor-cloudflare. L1 and L2. Exit: defects (a), (b), (c), (f), (h), (k), (l), (m), and (n) each have a named invariant whose validator fails on the pre-fix tree and passes on the post-fix tree.
6. reaktor-verify. The deterministic engine over snapshots, the specification IR (§9), the Alloy translator, and KSMT behind reaktor-verify-smt. L2 and L3. Exit: every invariant in step 2 has a deterministic check; the first SMT obligation (partition lowering preserves the reachable handler set) runs in CI with its bounds published.
7. One runtime primitive in Quint. reaktor-work retry and cancellation, using Work acceptance tests as the property list; or hot rewire, INV-GRAPH-6, if the code-push story moves first. L3. Exit: a checked specification, at least one counterexample that changed the design, and an implementation that cites the specification.
8. Model-based conformance. Generate traces from the step-7 model and replay them through the real TaskManager or ActorNode via adapters, on JVM and JS. L2 and L3. Exit: the differential harness runs in CI on both targets and fails when an implementation is missing.
9. The agent return edge. findings and manifest in graph_snapshot; a propose_patch tool that returns a VerificationReport without committing; the mutation broker at Gate 4 behind the operations control plane's approval spine (D11); an AGENT policy patch for graph:propose. Exit: an agent proposes the defect-(a) handler over MCP and receives the §11.2 finding; the same agent's revised patch passes; a human approves the plan.
10. Trace conformance and the manifest in CI. Mutation and invocation spans in GraphTelemetry, an OpenTelemetry exporter, the conformance visitor, and a VerificationAttestation per commit. Then L4 on the two targets Verified Foundations §9 ranks first, flexbuffer and the visual-language semantics, and L5 deterministic simulation as the capstone. Exit: a nightly run checks production-shaped traces against the model; a failing seed reproduces exactly.

16.1 The first experiment

Do not design the whole verification subsystem first. Take GraphDocument and its eleven commands and build a small Alloy model of Node, Port, Edge, Scope, and the five commands AddNode, RemoveNode, AddEdge, RemoveEdge, SetNodeScope. Encode five invariants: edges reference existing nodes, edges run provider to consumer, contracts are compatible, scope containment is acyclic, and a valid document stays valid after every legal command. Then break RemoveScope or AddEdge deliberately and make Alloy find the counterexample. Finally, turn the counterexample into a GraphDocument and render it in ReaktorDocumentEditor.

If that feels compelling in practice, create reaktor-verify. If it does not, this document has cost a week and nothing is built on it. That is the right bet size.

17. What this does not claim

• Not "Reaktor is formally verified". Stable Foundations §22 forbids the sentence, and §3 shows the current state: no specifications, no CI, fifteen shipped invariant violations. Every claim carries a level.
• Not a proof of the Kotlin. A Lean theorem is about an executable specification; the Kotlin is bound to it by conformance vectors. There is no Lean-to-Kotlin toolchain (Verified Foundations §9).
• Not unbounded. Alloy, TLC, Apalache, and SMT within a timeout are bounded. The manifest says "no counterexample within the stated bound".
• Not total coverage. The opaque region is real and will stay real: third-party SDKs, TypeScript shells, provider behaviour. The design makes it visible and named; it does not make it disappear.
• Not a replacement for testing. Jane Street's own stack keeps unit tests, simulated networking, randomised orderings, version-skew tests, fuzzing, performance labs, chaos, and deterministic simulation beside its proofs [3]. Reaktor derives several of those from the same invariant (§13), which is the unification; it does not drop any of them.
• Not exactly-once. Every durability attribute in §6 obeys the delivery table in Distributed Actors §14. The handler still must not charge a card twice.
• Not a new kernel. Ten primitives, unchanged. Everything here is a module.

18. Open questions

1. Which identity closes D-6 first. The specification IR keys on the fingerprint (§9.1). Until P-1 lands, the deterministic engine keys on the type string with a collision diagnostic, as decision D7(d) says, and INV-PORT-1 stays unstated.
2. Effect granularity. Read(store) at the store level is enough for ownership and tenancy. Field-level effects would let the checker reason about defect (b), owner columns are insert-only, without a database-specific rule. Start coarse.
3. Where temporal invariants live. Protocol specifications are written in Quint or TLA+ by hand today (step 7). Whether the IR's temporal fragment should generate them, or only reference them, is undecided. Referencing is enough for the manifest.
4. Concurrent agents. Two agents patching the same port surface as a patch.conflict finding, which the visitors design leaves unresolved. A patch's expectedRevision makes the second one fail cleanly; merging is a separate problem.
5. Cost budget. A bounded engine at step 4 of GraphAuthority adds latency to every plan. The rule should be that the deterministic engine is synchronous and everything else is asynchronous with a plan that waits, but the numbers have to be measured, in keeping with the design bar: performance is earned with harnesses, not guessed.
6. The opaque assumption language. An Assumption is prose today. Making it a contract in the IR (what the opaque block reads and writes, at what durability) would let contamination stop precisely. It is the same finite-data rule applied one level down.

19. Reading list

In the order that pays back fastest for this design.

1. Lamport, A Science of Concurrent Programs (Cambridge, April 2026) [9]. Abstract programs, safety, liveness, and fairness in chapter 4, refinement in chapter 6, auxiliary variables in chapter 7. It is the mental model for §8 and §13, and Lamport provides the PDF and the TLA+ specifications for its examples.
2. Cunha, Macedo, Brunel, Chemouil, Practical Alloy [8]. The structural and behavioural modelling chapters are the whole of what §16.1 needs. Reaktor's IR maps onto Alloy's relations almost directly.
3. Lamport, Specifying Systems, chapters 1 to 7 [10]. Lamport says the first seven chapters, 83 pages, are most of what engineers need. Read them while writing the step-7 specification, not before.
4. Leino and Leino, Program Proofs [11]. Pre- and post-conditions, invariants, termination, lemmas, and automated deductive verification through Dafny. This is where "the model holds" becomes "the program implements the contract", and it is the background for the Lean targets.
5. Jane Street, Proofs (and Refutations) using Z3 [2]. Ten minutes, and exactly the attitude §10 takes toward SMT: ask about one rewrite, accept the counterexample.
6. Jane Street, Formal methods and the future of programming [1] and Getting from tested to battle-tested [3]. The argument of §2 and the testing stack of §17, from the people making the same bet with a language they control.
7. Quint documentation [5], in particular the model-based testing page and the effect-system decision record. The shortest path from a specification to generated tests, and the effect discipline §6 borrows.
8. Theorem Proving in Lean 4 [12], later. Worth learning for its own sake and for the L4 targets, but not the highest-leverage starting point for Reaktor today.

Related docs

• Stable Foundations 5.6 Ultra - The canonical graph IR, WFStatic, the GraphPatchOp algebra, GraphAuthority, the reference monitor, the eight evidence levels, and the kernel verification portfolio this document builds on.
• Verified Foundations Fable 5 - The defect register, the INV-* catalogue, the stop-ship set, the fingerprint keystone, and the L0 to L5 ladder this document sequences by.
• Reaktor Essays - The shortest statement of why the graph is the system and why a small trusted semantic base matters.
• Graph Kernel - The ten primitives, the ten laws, ReaktorModule.validators(), and the AI command loop this document adds a return edge to.
• Graph Visitors - Finding, GraphPatch, dryRun, and passes; the carrier for every counterexample here.
• Graph Refinement Plan - Transactional Wiring, the five port shapes, and ChatGraph as the pilot.
• Control Plane - The mutation spine, the Critic, permission scopes, and the two dry-runs this document's loop runs inside.
• Visual Language - The formal semantics of program graphs and the purity discipline that §6 generalises to every node.
• Reaktor Server - Command-shaped APIs, transition records, idempotency, and effectively-once delivery.
• Actor Model and Distributed Actors - The mailbox guarantees and the delivery-semantics table every durability attribute obeys.
• Reaktor Work - The WorkRequest contract and the acceptance tests that become the first Quint model.
• Shadow Dev Environment - Capture as a visitor, deterministic replay by recording, the side-effect classification, and the comparison policies reused for conformance.
• Auth Architecture - AuthContext, AuthRequirement, LocalAuthorizer, and the secured ports that step 5 turns on.
• Desktop Master Plan - Decisions D3, D4, D7, D11, and D12, which fix the effect scale, the inspect-before-edit rule, port identity, the MCP mutation broker, and the concurrency blockers.

References

1. Yaron Minsky, "Formal methods and the future of programming", Jane Street, 7 June 2026. https://blog.janestreet.com/formal-methods-at-jane-street-index/
2. Jane Street, "Proofs (and Refutations) using Z3", 15 February 2018. https://blog.janestreet.com/proofs-and-refutations-using-z3/
3. Jane Street, "Getting from tested to battle-tested", 3 December 2025. https://blog.janestreet.com/getting-from-tested-to-battle-tested/
4. KSMT, a Kotlin and Java API over Z3, cvc5, Yices 2, and Bitwuzla. https://github.com/UnitTestBot/ksmt
5. Quint, executable specifications with TLA+ semantics, checked by TLC and Apalache. https://quint.sh/ · Model-based testing and trace validation: https://quint.sh/docs/model-based-testing · Effect system decision record: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system
6. Apalache, symbolic bounded model checker for TLA+. https://apalache-mc.org/docs/apalache/index.html
7. Alloy 6, language and analyzer; the analyzer jar can be embedded as an API. https://alloytools.org/ · https://github.com/AlloyTools/org.alloytools.alloy
8. Cunha, Macedo, Brunel, Chemouil, Practical Alloy. https://practicalalloy.github.io/
9. Leslie Lamport, A Science of Concurrent Programs, Cambridge University Press, April 2026. https://lamport.azurewebsites.net/tla/science-book.html
10. Leslie Lamport, Specifying Systems, Addison-Wesley. https://lamport.azurewebsites.net/tla/book.html
11. K. Rustan M. Leino and Kaleb Leino, Program Proofs, MIT Press, 2023. https://program-proofs.com/
12. Theorem Proving in Lean 4. https://lean-lang.org/theorem_proving_in_lean4/
13. Kotlin Lincheck. https://kotlinlang.org/docs/lincheck-guide.html