Reaktor Stable Foundations — 5.6 Ultra

Audit date: 2026-08-27
Scope: the Reaktor framework and its use by BestBuds
Document type: code-grounded target architecture, migration plan, and verification contract
Status vocabulary: implemented, partial, designed, and proposed have distinct meanings throughout this document

Executive decision

Reaktor already has enough breadth to demonstrate the shape of a serious application framework: graph assembly, typed ports, lifecycle hooks, actors, visitors, a typed HTTP service abstraction plus descriptors for additional transports, auth, persistence, tooling plans, FlexBuffers, multiplatform targets, and a substantial product integration in BestBuds. The next step is not to add another broad subsystem. It is to make a much smaller subset of the existing system unambiguous and hard to misuse.

The central architectural decision is:

Reaktor should have one immutable, versioned, serializable graph intermediate representation; one versioned certification contract made from explicit static, transition, activation, and runtime predicates; and one transactional mutation protocol. Runtime graphs, editors, manifests, deployment plans, agents, visual tools, tests, and product adapters should all project from or propose changes to that same kernel.

This is the stability boundary. Everything else is an interpreter, projection, adapter, or product policy.

The current code contains several strong seeds for this direction:

• reaktor-flow/src/commonMain/kotlin/dev/shibasis/reaktor/flow/graph/document/GraphDocument.kt provides a pure document-shaped representation.
• reaktor-flow/src/commonMain/kotlin/dev/shibasis/reaktor/flow/graph/document/GraphCommands.kt models in-memory, undoable graph changes as commands.
• reaktor-flow/src/commonMain/kotlin/dev/shibasis/reaktor/flow/graph/document/GraphEditorSession.kt maintains in-memory memento history; it is a design seed, not yet a durable replay log.
• reaktor-tooling/src/commonMain/kotlin/dev/shibasis/reaktor/tooling/ToolingModels.kt separates plan, safety classification, approval, execution, and events.
• reaktor-flexbuffer/src/commonMain/kotlin/dev/shibasis/reaktor/flexbuffer/flatbuffers/FlexBufferValidator.kt and its JVM hardening tests show how a boundary can fail closed.
• BestBuds exercises the runtime across UI, actors, persistence, services, workers, notifications, and realtime chat.

Those pieces do not yet constitute a single stable foundation. The runtime graph is mutable, semantic concepts are represented more than once, lifecycle ownership can escape its parent, authorization is not a universal reference monitor, actor delivery and persistence do not expose one durable protocol, service/choreography metadata is not enforced end to end, and no formal specifications currently establish the core laws.

The correct claim today is therefore:

Reaktor is a promising multiplatform graph framework with meaningful implemented components and a strong product test bed. It is not yet a formally verified or semantically closed foundation.

The achievable claim after this program is:

Reaktor's small semantic kernel is mechanically checked against stated laws; its temporal protocols are bounded-model-checked to published bounds; its implementations are translation-validated and subjected to property, concurrency, fault, fuzz, and compatibility testing; and every stronger claim names its assumptions and evidence.

That is both more defensible and more valuable than claiming that an entire Kotlin, native, JavaScript, database, network, and cloud system has been “formally proved.”

Strategic thesis: why Reaktor, why Kotlin, and where the power comes from

Reaktor's thesis is larger than dependency injection, a UI framework, an actor library, or a visual editor. Modern products are heterogeneous distributed programs: mobile and web clients, desktop tools, edge workers, servers, queues, actors, databases, analytics systems, native libraries, cloud resources, deployment pipelines, and humans or agents operating them. Conventional frameworks expose each surface through a separate configuration language and observability product. The relationships among them are reconstructed after the fact in diagrams, dashboards, and developer memory.

Reaktor can make those relationships executable. A nested heterogeneous port graph can represent the components, interfaces, ownership, flows, authority, placement, and evidence of the system. The graph is not valuable merely because it is visual. It is valuable because the same stable structure can drive compilation, runtime wiring, validation, navigation, telemetry, impact analysis, deployment, debugging, policy, simulation, and agent tools.

Why a Blueprint-style graph

Unreal Engine demonstrates an important division of labor: a high-performance runtime and deeply engineered native subsystems can coexist with a graph surface that makes composition visible and editable. Reaktor should adopt the useful part of that model without assuming that arbitrary visual graphs are automatically understandable or correct.

For distributed applications, the equivalent of a gameplay node may be a screen, worker, service, actor, database projection, queue, native kernel, protocol endpoint, deployment unit, or diagnostic pass. Hierarchical subgraphs let a user enter the relevant scale: a whole product, one feature, one request flow, one actor, or one hot path. Typed boundary ports prevent hierarchy from becoming a collection of opaque boxes.

The graph should complement source code, not replace it. Source remains the best medium for algorithms and precise local logic. The graph becomes the best medium for composition, cross-system flow, ownership, contracts, and operational context. Stable source maps keep the two synchronized.

Why keep a runtime graph

Compiling away every graph object can minimize overhead, but it also erases a valuable control and evidence plane. A carefully designed runtime projection enables:

• live topology and activation inspection;
• graph-correlated metrics, traces, profiles, and failures;
• safe, transactional rewiring of explicitly replaceable regions;
• agentic and human queries over the actual running revision;
• comparison of desired, compiled, deployed, and observed state;
• targeted fault injection, replay, and test selection;
• graceful degradation based on observed capability offers.

The runtime graph must not be a second mutable truth. It is a lightweight projection of a certified immutable snapshot plus activation/evidence state. Hot paths should compile to direct calls, generated dispatch tables, or bounded binary adapters. The runtime graph provides identity and observability without requiring every data item to traverse a reflective graph interpreter.

Why visitors

Once components share a canonical graph contract, cross-cutting behavior can be expressed as queries, compiler passes, monitors, or patch proposals instead of invasive base classes. Visitors can detect unbound ports, compute lifecycle order, derive routes, install telemetry plans, verify authorization coverage, choose deployment partitions, generate protocol monitors, identify affected tests, or produce an agent-readable explanation.

The power comes from combining a small semantic substrate with a growing analysis ecosystem. The safety boundary is that queries remain pure and rewrites return patches. A visitor does not acquire ambient permission to mutate a live product.

Why Kotlin

Kotlin is unusually well matched to this program:

• Kotlin Multiplatform supplies a common semantic language across JVM/server, Android, iOS/native, JavaScript, and Wasm targets.
• Sealed interfaces, value classes, generics, delegation, extension functions, and DSLs can make the kernel expressive without an external modeling language for ordinary users.
• Coroutines and Flow provide a common vocabulary for cancellation, asynchronous work, and streams—provided Reaktor specifies ownership and delivery rather than treating the library primitives as the full protocol.
• KSP and compiler tooling can generate stable registries, schemas, monitors, source maps, bindings, and invalid-case tests.
• JVM interoperability opens the Java ecosystem; Kotlin/Native and C interop reach native systems; Kotlin/JS connects to the TypeScript/JavaScript ecosystem.
• The language is concise enough for high-level architecture APIs while remaining statically typed and capable of direct systems integration.

Kotlin does not remove the hard problems. expect/actual declarations do not guarantee behavioral parity, coroutine code is not automatically leak-free, generics do not define wire compatibility, and a shared source set does not prove a platform implementation. Reaktor's opportunity is to add the missing semantic and evidence layer around Kotlin's reach.

Why a deliberately polyglot core

Kotlin should own the canonical model and most orchestration. TypeScript/JavaScript is valuable for dynamic edge surfaces, browser ecosystems, Hermes-hosted logic, and constrained code replacement. C++ is valuable for native integration and tight performance loops. Python can add scientific, ML, data, and automation ecosystems when the boundary is robust enough. Other languages remain possible through generated envelopes and adapters.

The goal is not to make language boundaries invisible. It is to make them uniform, explicit, measured, and safe. Reaktor FFI should be a versioned superset of the interaction shapes needed by the system—sync call, request/response, stream, cancellation, credit, error, and lifecycle—while using local zero-copy or direct invocation where valid and network protocols where remote. FlexBuffers can be a high-performance schema-flexible payload representation, but semantic schema IDs, resource bounds, ownership, and compatibility still need an envelope.

Why opinionated infrastructure

An opinionated default stack can create leverage because the graph compiler and tooling can understand concrete guarantees. PostgreSQL, ClickHouse, Memgraph, Cloudflare Workers/Durable Objects/D1/R2/Queues, GCP Pub/Sub, and Kubernetes on compute instances can form a productive default vocabulary. Reaktor can generate safer plans, tailored tests, dashboards, and evidence when it knows the actual substrate.

Opinionated must not mean semantically dishonest. Each provider adapter declares its real transaction, durability, locality, consistency, identity, and failure properties. Replaceability comes from satisfying contracts and passing compatibility suites, not from pretending every cloud or database is equivalent. Cloudflare may remain a preferred high-leverage dependency while the graph makes that dependency and its fallback cost explicit.

The highest-leverage power expansions

The following primitives add more expressive power than another collection of platform wrappers:

1. Canonical graph IR and contract language. This turns runtime, visual, build, deploy, and agent surfaces into projections of one meaning.
2. Transactional patch algebra. Safe change becomes composable across editor, codegen, AI, runtime rewiring, and deployment.
3. Effect and authority algebra. Tools can reason about what a composition may do and who may trigger it.
4. Global protocols with endpoint projection. Cross-process flows become checkable programs instead of conventions spread across clients and servers.
5. Operation envelope and durable effect protocol. Retry, offline, workers, actors, sockets, and databases share identity and reconciliation semantics.
6. Capability constraint solver. Platform adaptation and graceful degradation become explainable, testable resolution rather than branching explosion.
7. Evidence/provenance plane. Desired, observed, inferred, simulated, checked, and attested state can coexist without being confused.
8. Query/rewrite SDK. Humans, IDEs, visitors, and agents gain one bounded interface for analysis and typed change proposals.
9. Polyglot envelope plus generated bindings. Kotlin, TypeScript, C++, and eventually Python participate without hand-written semantic drift.
10. Restricted signed replacement protocol. Stateless and later carefully bounded stateful graph regions can update without a full deployment.
11. Durable workflow and actor protocols. These become powerful once identity, effects, revisions, fencing, and persistence are already stable.
12. Graph-aware integration catalog. Profilers, benchmarks, debuggers, test tools, deployers, IDEs, MCP/A2A tools, and domain services attach through contracts and emit evidence tied to graph revisions.

The first eight items strengthen the basis from which many product categories can be generated. The later items should not be used to postpone that foundation.

1. What “stable” means

Stability is not one property. Reaktor needs seven separately testable kinds of stability.

Each guarantee also needs an evidence level. Reaktor documentation and tooling should use the following labels instead of the unqualified word “verified”:

1. Type-enforced — illegal states are unrepresentable within the typed API, subject to language and unsafe-code assumptions.
2. Runtime-checked — a validator or reference monitor rejects invalid input at a named boundary.
3. Property-tested — generated cases exercise algebraic or state-machine properties.
4. Concurrency-tested — linearizability or memory-order properties are checked by an appropriate concurrency harness.
5. Bounded-model-checked — a temporal or structural model has been exhaustively checked within published bounds.
6. Mechanically proved — a theorem and its assumptions are checked by a proof assistant.
7. Translation-validated — a generated artifact is independently checked against the source semantic object.
8. Operationally attested — a signed record identifies the input, toolchain, checks, bounds, result, and artifact digest.

An attestation is evidence that a process ran. It is not, by itself, a mathematical proof that the implementation is correct.

2. Audit basis and current evidence

This design is based on source inspection of the sibling reaktor repository and the bestbuds product repository, not only on architecture prose. The most relevant implemented surfaces are:

• reaktor-graph and reaktor-graph-port: mutable runtime graph, lifecycle, navigation, typed ports, connection helpers, visitors, and actors.
• reaktor-flow: immutable-looking graph documents, commands, editor sessions, and architecture adapters.
• reaktor-core: concurrency and global feature facilities.
• reaktor-auth: authentication and authorization kernel plus secured ports.
• reaktor-db: object database and persistence abstractions.
• reaktor-service: request/response and transport abstractions.
• reaktor-tooling: plans, safety, approvals, execution, event streams, and process supervision.
• reaktor-flexbuffer and reaktor-ffi: binary validation and cross-language payload boundaries.
• BestBuds application, chat, messaging, worker, notification, and timeline code: a cross-runtime integration proof.

Targeted JVM tests passed during the audit:

./gradlew :reaktor-graph:jvmTest :reaktor-graph-port:jvmTest :reaktor-auth:jvmTest --no-daemon
./gradlew :reaktor-core:jvmTest --tests '*ConcurrentHashMapMigrationTest' --no-daemon
./gradlew :app:jvmTest --no-daemon

Passing tests are useful evidence that the inspected happy paths and regression cases work. They are not evidence that all schedules, failure points, wire versions, authority contexts, or platform implementations satisfy the proposed laws.

The builds also reported version and compatibility warnings involving embedded/requested Kotlin versions, Kotlin DSL expectations, experimental JS language flags, Kotlin Multiplatform/Android Gradle Plugin compatibility, and Compose version alignment. These warnings do not invalidate the passing tests, but they are evidence that the toolchain itself must become part of the compatibility contract.

2.1 What is already strong

The current system has real strengths worth preserving:

• Graph construction and typed ports make dependencies inspectable rather than hiding all composition in object constructors.
• GraphDocument commands show that graph editing can be made pure and undoable; durable replay still requires the versioned patch log proposed here.
• Tooling plans already contain the right control-plane instincts: describe, classify, approve, fingerprint, execute, and emit evidence.
• The FlexBuffer validator and hardening suite treat hostile binary input as a boundary problem rather than trusting generated accessors.
• The local actor implementation gives Reaktor a concrete execution model to refine.
• BestBuds crosses enough boundaries to expose real architectural weaknesses that toy examples would miss.
• Existing graph-kernel and refinement documents already argue for a small graph vocabulary with modules adding meaning.

2.2 What currently blocks a “stable foundation” claim

The important blockers are not the absence of fashionable abstractions. They are contradictions and gaps at existing boundaries:

• Port identity can depend on runtime type naming (reaktor-graph-port/src/commonMain/kotlin/dev/shibasis/reaktor/portgraph/port/Port.kt:35-54), which is unstable across obfuscation, refactoring, JS/native compilation, and compiler versions.
• Bulk connection helpers can partially mutate before a later mismatch is discovered (reaktor-graph-port/src/commonMain/kotlin/dev/shibasis/reaktor/portgraph/graph/connect.kt:62-80).
• Public Edge construction, disconnect, and graph attach paths do not yet establish one owner/type/state invariant, and container ownership does not automatically close child graphs.
• Graph.autoWire performs mutable runtime matching (reaktor-graph/src/commonMain/kotlin/dev/shibasis/reaktor/graph/core/Graph.kt:211-243) rather than compiling and committing a deterministic binding plan.
• Invalid lifecycle transitions can still lead to callback behavior that should be excluded by construction (reaktor-graph/src/commonMain/kotlin/dev/shibasis/reaktor/graph/capabilities/LifecycleCapability.kt:31-41).
• A SupervisorJob is created without preserving the intended parent relationship (reaktor-core/src/commonMain/kotlin/dev/shibasis/reaktor/core/capabilities/ConcurrencyCapability.kt:31-42), weakening structured ownership.
• Feature is a global registry (reaktor-core/src/commonMain/kotlin/dev/shibasis/reaktor/core/framework/Feature.kt:18-45), so independent sessions and tests can interfere unless every use is carefully reset.
• Authorization composition and resource matching have correctness gaps in reaktor-auth/src/commonMain/kotlin/dev/shibasis/reaktor/auth/kernel/AuthKernel.kt:378-411,464-468, including mixed anyOf behavior and incomplete use of ResourceRef type/id.
• SecuredPort is a wrapper (reaktor-auth/src/commonMain/kotlin/dev/shibasis/reaktor/auth/graph/SecuredPort.kt:27-69), not a mandatory reference monitor for every invocation and edge.
• Persistence surfaces do not yet expose one portable transaction/revision/idempotency contract (reaktor-db/src/commonMain/kotlin/dev.shibasis.reaktor.db/ObjectDatabase.kt:15-33,106-121,201-221).
• Actor processing launches work and catches failure, but does not yet define a durable mailbox, fencing, one explicit delivery disposition, or a pure reducer/effect split (reaktor-graph/src/commonMain/kotlin/dev/shibasis/reaktor/graph/core/node/ActorNode.kt:46-63,135-211,261-318).
• Service transports are named, but a declared transport does not yet imply a generated, monitored end-to-end protocol (reaktor-service/src/commonMain/kotlin/dev/shibasis/reaktor/service/ServiceTransport.kt:5-14; Service.kt:56-113).
• FlexBuffer validation exists, while public raw decode and FFI payload access paths can still expose arbitrary/mutable data without carrying a proof-of-validation type (reaktor-flexbuffer/src/commonMain/kotlin/dev/shibasis/reaktor/flexbuffer/core/FlexBuffers.kt:120-126,174-180; reaktor-ffi/src/commonMain/kotlin/dev/shibasis/reaktor/ffi/payload/FlexPayload.kt:8-51).
• BestBuds has multiple mutable/global entry points and retry-sensitive flows, including application-wide state (bestbuds/modules/app/src/commonMain/kotlin/ai/bestbuds/app/BestBuds.kt:121-128,376-420), chat socket behavior (bestbuds/modules/app/src/jsMain/kotlin/ai/bestbuds/app/cloudflare/chat/ChatService.kt:146-192,399-451), message writes, worker retries, and timeline reconciliation.

These are fixable. The mistake would be to hide them behind a broader framework story.

3. The stable foundation: four layers

The target architecture has four layers with one-way dependency pressure. The arrows below mean depends on lower semantics/artifacts; they are not a runtime data-flow diagram.

┌──────────────────────────────────────────────────────────────────────┐
│ Products and control planes                                         │
│ BestBuds · Reaktor Desktop · CLI · agents · deploy/UI projections   │
└───────────────────────────────┬──────────────────────────────────────┘
                                │ depends on runtime APIs
┌───────────────────────────────▼──────────────────────────────────────┐
│ Runtime interpreters                                                │
│ local graph · actors · services · persistence · UI · cloud · FFI    │
└───────────────────────────────┬──────────────────────────────────────┘
                                │ depends on compiler output
┌───────────────────────────────▼──────────────────────────────────────┐
│ Compiler and validators                                             │
│ normalize · typecheck · solve wiring · policy · plan · codegen      │
└───────────────────────────────┬──────────────────────────────────────┘
                                │ depends on pure kernel semantics
┌───────────────────────────────▼──────────────────────────────────────┐
│ reaktor-kernel                                                      │
│ canonical IDs · GraphState · contracts · patches · laws · digest    │
└──────────────────────────────────────────────────────────────────────┘

3.1 Kernel dependency rule

reaktor-kernel must remain a small Kotlin Multiplatform module with no dependency on:

• Compose or Android lifecycle APIs;
• Koin or another dependency-injection container;
• Ktor, HTTP, WebSocket, database, or cloud SDKs;
• coroutine dispatchers or actor runtimes;
• reflection-based type discovery;
• platform clocks, random identifiers, filesystem access, or global registries.

The kernel may depend on a deliberately small serialization and immutable-collection substrate if the project accepts that as part of the trusted computing base. Certifiable facets, policies, effects, and protocols must be finite, total data languages; an opaque executable callback cannot participate in static certification. All nondeterministic inputs—time, entropy, identity allocation, environment, observed capabilities—must enter as explicit values.

3.2 Runtime dependency rule

Runtime modules may interpret a certified graph snapshot. They may not silently invent kernel semantics. If a platform cannot satisfy a declared contract, activation returns a structured finding or a declared degraded mode; it does not reinterpret the contract.

3.3 Product dependency rule

BestBuds can add domain node kinds, port schemas, policies, protocols, and projections. It cannot weaken kernel well-formedness, skip the reference monitor, mutate topology outside GraphAuthority, or depend on an undocumented platform-specific interpretation.

4. Canonical graph intermediate representation

The stable unit is a value, not a living object graph.

@JvmInline value class GraphId(val value: String)
@JvmInline value class NodeId(val value: String)
@JvmInline value class PortId(val value: String)
@JvmInline value class EdgeId(val value: String)
@JvmInline value class PolicyId(val value: String)
@JvmInline value class ProtocolId(val value: String)
@JvmInline value class PatchId(val value: String)
@JvmInline value class ActivationId(val value: String)
@JvmInline value class ContractId(val value: String)
@JvmInline value class SchemaId(val value: String)
@JvmInline value class Revision(val value: ULong)
@JvmInline value class Epoch(val value: ULong)

data class GraphState(
    val graphId: GraphId,
    val schemaVersion: UInt,
    val revision: Revision,
    val nodes: PersistentMap<NodeId, NodeSpec>,
    val ports: PersistentMap<PortId, PortSpec>,
    val edges: PersistentMap<EdgeId, EdgeSpec>,
    val containment: PersistentSet<Contains>,
    val protocols: PersistentMap<ProtocolId, ProtocolSpec>,
    val policies: PersistentMap<PolicyId, PolicySpec>,
)

data class NodeSpec(
    val id: NodeId,
    val kind: NodeKind,
    val ports: PersistentSet<PortId>,
    val facets: PersistentMap<FacetKey, FacetValue>,
    val lifecycle: LifecycleContract,
    val effects: EffectSet,
    val source: SourceRef?,
)

data class CertifiedGraph(
    val state: GraphState,
    val digest: GraphDigest,
    val kernelVersion: KernelVersion,
    val normalizerVersion: NormalizerVersion,
    val registryDigest: RegistryDigest,
)

The exact Kotlin spelling can change; the semantic distinctions cannot.

4.1 Definition identity is not activation identity

A graph definition answers “what is this component in the program?” An activation answers “which running instance, in which session and epoch, is this?” Conflating them causes stale messages, session leaks, and misleading telemetry.

Every runtime handle should carry at least:

data class RuntimeIdentity(
    val definition: NodeId,
    val activation: ActivationId,
    val graphRevision: Revision,
    val epoch: Epoch,
)

Messages and completions aimed at an older epoch are rejected or explicitly migrated. An epoch is allocated by the owning durable authority or lease/revision store, not by an in-memory counter that can reset after a crash. Observability can then aggregate by stable definition while still distinguishing individual runs.

4.2 Stable identifiers

Stable IDs must be explicit in source or deterministically generated from stable, versioned inputs. They must not be derived solely from:

• KClass.simpleName or Java class names;
• source ordering;
• memory addresses or hash-map iteration;
• UI labels;
• compiler-generated anonymous names;
• random UUIDs allocated during every build.

Renames and moves require an alias/migration record. A graph compiler should reject accidental duplicate IDs and warn when a previously published ID disappears without a declared migration. Type-specific IDs prevent a node ID from being accidentally supplied where an edge, port, policy, or protocol ID is required.

The graph digest is computed over canonical bytes of GraphState plus the kernel, normalizer, compiler-contract, and registry versions. It is not a field inside the bytes it hashes. Revision increment is checked; exhausting ULong is a terminal migration condition, never wraparound. Collision resistance of the selected digest is a trusted cryptographic assumption, not a Lean theorem about the graph.

4.3 Port contracts

A port is more than a generic Kotlin type.

data class PortContract(
    val id: ContractId,
    val role: PortRole,
    val schema: SchemaId,
    val schemaRange: VersionRange,
    val cardinality: Cardinality,
    val interaction: InteractionMode,
    val delivery: DeliveryContract,
    val errors: ErrorContract,
    val effects: EffectSet,
    val authority: AuthorityRequirement,
    val qos: QualityOfService,
)

enum class PortRole { PRODUCER, CONSUMER, BIDIRECTIONAL, GATEWAY }
enum class InteractionMode { VALUE, STREAM, REQUEST_RESPONSE, COMMAND, EVENT }

The contract must state whether absence is allowed, how errors appear, whether ordering and deduplication are promised, what cancellation means, and which effects or permissions are required. Generic types remain useful implementation checks, but they cannot carry the entire cross-process and cross-version contract.

4.4 Edges and gateways

An edge binds two declared endpoints under a contract. If schemas, authority domains, process locations, or protocols differ, the compiler inserts or requires an explicit gateway node. Adaptation is therefore visible in the graph.

data class EdgeSpec(
    val id: EdgeId,
    val consumer: EndpointRef,
    val provider: EndpointRef,
    val contract: ContractId,
    val adapter: NodeId?,
    val policy: PolicyId?,
)

The canonical structural orientation is consumer/requester → provider/dependency, matching current Edge construction and JSON export. The interaction contract separately states the direction of request, response, value, event, and stream frames; UI projections may draw data flow in the opposite direction but must label that projection. Import adapters map current source=consumer.owner, destination=provider.owner without reversal and reject an edge whose endpoint roles contradict that rule. This removes the ambiguity of generic from/to fields.

There is no invisible “compatible enough” runtime cast. Schema conversion, retry, serialization, authorization, rate limiting, and process transport are first-class adapters with their own evidence and lifecycle.

5. Certification predicates and invariants

“Valid graph” must not mix a finite snapshot property with live-resource or temporal claims. The versioned certification contract therefore separates:

WFStatic(kernelVersion, registrySnapshot, graphState)
ValidTransition(certifiedGraph, authenticatedPlanInput, patch, nextGraph)
WFActivation(environmentSnapshot, certifiedGraph, activationPlan)
RuntimeInv(certifiedGraph, runtimeObservation)
ProtocolSafety(protocol, trace)
NormalizeLaws(normalizerVersion)
ReconciliationInv(desiredRevision, observedState, journal)

The compiler, editor, runtime activator, importers, code generators, and formal models must agree on the definitions relevant to their boundary. A GraphCertificate aggregates results; it does not collapse them into one unary predicate.

5.1 Static graph laws

At minimum, WFStatic includes these finite laws:

1. Unique identity: node, port, edge, protocol, and policy identifiers are unique in their namespaces.
2. Declaration ownership: each port is owned by exactly one node.
3. Endpoint existence: every edge endpoint and adapter exists.
4. Role compatibility: the source and target roles permit the selected interaction mode.
5. Contract compatibility: a concrete schema version can be selected from the compatible ranges; error, cancellation, delivery, and effect requirements are compatible or an explicit adapter discharges the difference.
6. Cardinality: edge counts respect exact/optional/one-or-more/many bounds.
7. Required binding: every required consumer is bound before activation.
8. Containment validity: the containment relation is acyclic and each contained node has the permitted number of parents.
9. Boundary closure: an edge crossing a graph boundary passes through a declared boundary port or gateway.
10. Protocol projectability: roles are coherent and mergeable projections of one supported global protocol version.
11. Static effect ceiling: declared composition cannot exceed the statically supplied grant ceiling.
12. Lifecycle topology: synchronous dependency cycles are rejected; permitted strongly connected regions require an explicit activation barrier and cycle protocol.
13. Schema integrity: referenced schemas and migrations exist and form supported version paths.
14. Source traceability: generated entities retain source and generator provenance sufficient for diagnostics and impact analysis.

NormalizeLaws separately covers idempotence and order independence. ValidTransition covers patch preconditions, authenticated authority, revision/base digest, non-amplification, and next-state preservation. WFActivation covers environment offers and activation ordering. RuntimeInv covers the rule that each live resource has exactly one activation owner. Protocol and reconciliation properties are trace/state-machine obligations rather than snapshot facts.

Use a structured result rather than Boolean:

sealed interface CertificationResult {
    data class Certified(
        val snapshot: CertifiedGraph,
        val certificate: GraphCertificate,
    ) : CertificationResult

    data class Rejected(
        val findings: PersistentList<GraphFinding>,
    ) : CertificationResult
}

CertifiedGraph should be constructible only by the validator inside the trusted module. Deserialization returns untrusted GraphState until canonicalization, registry/schema resolution, digest, and WFStatic have been checked. Static decidability applies only because the kernel languages and registries are finite and total.

6. Hierarchy and open composition

Reaktor needs a precise answer to “how do graphs compose?” A plain directed multigraph is insufficient once components expose boundaries, contain subgraphs, deploy across runtimes, and have independent authority domains.

The practical model should combine:

• a typed directed multigraph for nodes, ports, and edges;
• a place graph for containment and ownership;
• a link graph for connectivity that may cross containment boundaries only through declared interfaces;
• an open-graph interface describing inputs and outputs available for composition.

This is close in spirit to bigraphs for place/link separation and structured cospans for open-system composition. Reaktor does not need to expose category-theory terminology in day-to-day APIs, but it does need the corresponding laws:

• composition is structurally associative modulo an explicit alpha-renaming/canonical-isomorphism relation, under fresh-ID, disjointness, and interface-compatibility premises;
• composition with an identity boundary is structurally isomorphic to the original graph;
• hiding an internal node cannot create an undeclared external edge;
• composition preserves WFStatic when interface obligations match;
• authority and effects at the composite boundary are derived, never guessed.

6.1 “Eigen” primitives

The useful interpretation of eigen primitives is not that arbitrary components are literal eigenvectors. It is that the framework has a small generating basis—node, port, edge, containment, contract, protocol, authority, patch—from which larger structures are built by typed composition.

Spectral methods remain useful as analyses over an explicit matrix projection of a snapshot:

• eigenvector centrality to identify structurally influential nodes;
• the Fiedler vector to suggest partitions or fragile cuts;
• spectral radius as one signal of feedback amplification in a weighted projection;
• separate graph-coloring/constraint-solving passes for placement, compatibility, or scheduling constraints.

Every spectral result must name the projection, directionality, weights, normalization, and snapshot revision. It is an analysis artifact, not an intrinsic semantic truth about the runtime.

7. Graph compiler and deterministic wiring

Runtime auto-wiring should become a compiler pass.

7.1 Compiler pipeline

source declarations / manifests / imported GraphDocument
        ↓
parse and assign stable IDs
        ↓
normalize schemas, facets, effects, policies, and protocols
        ↓
validate local declarations
        ↓
solve candidate port bindings and adapter requirements
        ↓
validate static/global certification laws
        ↓
emit CertifiedGraph + findings + source map + certificate
        ↓
generate platform registries, serializers, monitors, and test cases

The compiler output is the only input accepted by a production runtime activator. Development mode may support an explicitly labeled unsafe or partial activation, but it must not be confused with a certified snapshot.

7.2 Wiring as constrained matching

Auto-wiring is a constrained bipartite matching problem, not a name lookup. A candidate edge is legal only if all declared constraints are satisfied:

role × schema/version × cardinality × interaction × effects × authority
× lifecycle region × process boundary × protocol role × user overrides

The solver must produce one of:

• a unique deterministic plan;
• a set of ambiguity findings requiring explicit selection;
• an unsatisfied-requirement finding;
• a plan containing explicit adapters whose own contracts can be validated.

The result is normalized and sorted by stable IDs. The same declarations in a different construction order must yield the same plan and digest.

7.3 Generated registries, not reflection names

KSP or another build-time generator should emit:

• stable component and port registries;
• schema descriptors and compatibility tables;
• lifecycle factories;
• protocol endpoint monitors;
• authority/effect manifests;
• source locations;
• platform capability offers;
• serializer and FFI bindings;
• test-case seeds for invalid configurations.

JVM reflection may remain a development adapter, but the published contract must not depend on reflection names. JS, native, and obfuscated Android builds must consume the same stable IDs.

8. Transactional mutation and GraphAuthority

No runtime, editor, AI tool, feature installer, or product component should mutate topology directly.

sealed interface GraphPatchOp {
    data class AddNode(val node: NodeSpec) : GraphPatchOp
    data class RemoveNode(val node: NodeId) : GraphPatchOp
    data class ReplaceNode(val expected: NodeSpec, val value: NodeSpec) : GraphPatchOp
    data class AddPort(val port: PortSpec) : GraphPatchOp
    data class RemovePort(val port: PortId) : GraphPatchOp
    data class ReplacePort(val expected: PortSpec, val value: PortSpec) : GraphPatchOp
    data class AddEdge(val edge: EdgeSpec) : GraphPatchOp
    data class RemoveEdge(val edge: EdgeId) : GraphPatchOp
    data class ReplaceEdge(val expected: EdgeSpec, val value: EdgeSpec) : GraphPatchOp
    data class AddContainment(val relation: Contains) : GraphPatchOp
    data class RemoveContainment(val relation: Contains) : GraphPatchOp
    data class PutProtocol(val expected: ProtocolSpec?, val value: ProtocolSpec) : GraphPatchOp
    data class RemoveProtocol(val protocol: ProtocolId) : GraphPatchOp
    data class PutPolicy(val expected: PolicySpec?, val value: PolicySpec) : GraphPatchOp
    data class RemovePolicy(val policy: PolicyId) : GraphPatchOp
    data class ReplaceFacet(
        val node: NodeId,
        val key: FacetKey,
        val expected: FacetValue?,
        val value: FacetValue?,
    ) : GraphPatchOp
    data class GrantAuthority(val grant: AuthorityGrant) : GraphPatchOp
    data class RevokeAuthority(val grant: PolicyId) : GraphPatchOp
}

data class GraphPatch(
    val patchSchemaVersion: UInt,
    val patchId: PatchId,
    val graphId: GraphId,
    val expectedRevision: Revision,
    val expectedBaseDigest: GraphDigest,
    val operations: PersistentList<GraphPatchOp>,
    val intent: String,
)

The closed algebra must cover every field of GraphState; adding a new state field is a schema change that either adds a patch operation or declares the field compiler-derived. The authenticated principal is supplied by the invocation/reference-monitor context and recorded in the plan—it is never trusted from a caller-authored patch.proposer field.

GraphAuthority follows a pure plan/validate/commit protocol:

1. Receive immutable AuthenticatedPlanInput: principal/context, patch, kernel/compiler/registry/policy versions, environment/evidence snapshot, clock/expiry, and target.
2. Read immutable snapshot revision r and verify graph ID, revision, and base digest.
3. Normalize the patch and apply it to an in-memory value using independent per-operation preconditions.
4. Run static, transition, contract, policy, lifecycle-plan, and migration validators.
5. Produce a PatchPlan containing the full diff, findings, effects, safety class, required approvals, test impact, and rollback/compensation plan.
6. Verify approvals against the exact complete-plan fingerprint and expiry.
7. Through a single topology writer, atomically persist a SnapshotRecord containing state r+1, digest, journal entry, authenticated proposer, approvals, and certificate. A backend that cannot provide this atomic record must use a durable write-ahead intent plus deterministic crash recovery before publishing the new snapshot.
8. Publish the committed immutable snapshot to readers.
9. Reconcile runtime activations from the committed snapshot.

The key laws are:

failed patch ⇒ state' = state
successful patch ⇒ revision' = revision + 1
successful patch ⇒ WFStatic(state') ∧ ValidTransition(state, planInput, patch, state')
readers observe either old snapshot or new snapshot, never a partial patch
same complete immutable PlanInput ⇒ same plan fingerprint
revision = ULong.MAX_VALUE ⇒ reject and require revision-schema migration

The existing GraphCommand, GraphEditorSession, and tooling plan/safety/event models should be reused rather than replaced. Today the commands are not a versioned serializable log and editor history is in-memory mementos; durable replay begins only when they become projections of the serialized patch algebra and journal. Rollback is a compensating patch that creates a new revision, never history rewind.

8.1 Runtime reconciliation is separate from topology commit

Committing a valid desired snapshot does not guarantee every external effect succeeds. The system therefore records:

• desired graph revision;
• observed runtime activation revision;
• reconciliation state and attempts;
• external side effects and idempotency keys;
• compensation or rollback eligibility;
• degradation findings.

This preserves the critical distinction between an atomic semantic commit and an eventually completed physical rollout.

9. Lifecycle and owned runtime scopes

A stable runtime returns an owned handle.

interface RuntimeHandle {
    val identity: RuntimeIdentity
    val state: StateFlow<ActivationState>
    suspend fun quiesce(deadline: Instant): QuiesceResult
    suspend fun closeAndJoin(deadline: Instant): CloseResult
    suspend fun awaitClosed(deadline: Instant): CloseResult
}

Every activation owns a RuntimeScope containing child coroutines, actor mailboxes, subscriptions, native allocations, database sessions, sockets, and adapters. Parent cancellation reaches all descendants. A child must not replace its parent's job with an unrelated SupervisorJob.

9.1 Lifecycle state machine

Use one explicit state machine, for example:

Declared → Prepared → Active → Quiescing → Inactive → Closed
                 ↘ Failed ────────────────↗

Rules:

• invalid transitions return a finding and invoke no success callback;
• close is idempotent and terminal;
• acyclic dependencies activate before dependents and close after dependents; an allowed strongly connected region uses an explicit prepare/barrier protocol;
• close continues after individual failures and reports an aggregate;
• every event includes definition ID, activation ID, epoch, graph revision, cause, and correlation ID;
• activation never publishes Active before required ports, policies, and protocol monitors are installed;
• new input is refused after quiescing begins, while in-flight work follows the declared drain/cancel policy.

9.2 Remove global correctness dependencies

Global conveniences such as Feature can remain as compatibility facades only during migration. Stable code resolves features through an explicitly injected ReaktorSession or RuntimeScope; the facade must fail on missing or ambiguous session context rather than infer one from a global under concurrent KMP coroutines. Parallel tests, previews, users, tenants, and workbench tabs must not share mutable capability state accidentally.

BestBuds should similarly stop using application-wide mutable objects as correctness boundaries. A product session owns its graph handle, auth principal, offline store namespace, socket set, workers, and close path.

10. Authority as a graph-wide reference monitor

Availability and permission are different concepts:

• a capability offer says an implementation can perform an operation;
• an authority grant says a principal may request that operation in a context;
• a policy decision says a specific invocation is allowed now;
• an effect records what the invocation may change.

These must not collapse into one Capability marker.

10.1 Enforcement points

Every effectful path passes through the same authorization evaluator, including:

• local port invocation;
• graph edge dispatch;
• actor command handling;
• service request handlers;
• HTTP routes and WebSocket frames;
• database commands;
• deployment and tooling operations;
• native/FFI calls that expose privileged effects;
• AI-proposed operations.

The evaluator receives a complete context:

data class DecisionInput(
    val principal: Principal,
    val tenant: TenantRef?,
    val action: ActionRef,
    val resource: ResourceRef,
    val graph: GraphId,
    val activation: ActivationId?,
    val environment: EnvironmentRef,
    val evidence: EvidenceSet,
    val time: Instant,
)

Resource matching uses both type and identifier under an explicit wildcard rule. Boolean policy combinators must have a denotational, preferably three-valued (allow/deny/indeterminate) semantics for missing context and negation. In the current LocalAuthorizer, a non-empty outer anyOf returns before evaluating outer allOf, permissions, roles, and delegation rules; either make the policy AST prevent mixed shapes or define and implement the complete conjunction explicitly.

10.2 Non-amplification law

For any patch or composition:

Authority(after) ⊆ Authority(before) ∪ ApprovedExplicitGrants

Adapters may attenuate authority. They may not create it. A composite component's outward effect ceiling is derived from its parts and policies.

10.3 BestBuds security gates

BestBuds should be the negative-test reference application. Required gates include:

• a chat principal cannot subscribe to, publish to, react in, or fetch a room without membership/room policy;
• unknown or malformed WebSocket frames are rejected, never broadcast as a fallback;
• external identity is derived from verified token claims rather than a client query parameter or arbitrary serialized-user header; the intentional internal delegated-user header remains allowed only behind the exact verified service-principal, method, and scope gate already implemented in BestBudsRequest.kt:301-317 and covered by negative auth-policy tests;
• notification debug routes are absent (404) in production and require service/admin auth in non-production; Pub/Sub push verifies issuer and audience, and publish/received endpoints are protected;
• offline data is partitioned by authenticated principal and tenant;
• worker retries cannot bypass auth by replaying a pre-authorized payload in a different context;
• resource type and ID mismatches deny;
• missing policy metadata denies for effectful edges;
• all denials are observable without logging credentials or message bodies.

Generated negative tests should accompany every declared authority requirement.

The first gates are responses to concrete current exposures, not hypothetical hardening:

• ChatService.kt:146-192 authenticates before minting a room-scoped realtime token but does not check chat_members; ChatService.kt:429-451 verifies token audience/context/scope at connect but also does not check membership. A non-member must be denied at both mint and connect. Revoking membership between mint and connect must deny, and revoking it for an active socket must disconnect or fence subsequent room effects. Every room-effect frame rechecks current room authority or a bounded, revocation-aware lease.
• Fetch and send already enforce membership through MessagingWorker.kt:126-160 and reusable social repository gates. Preserve that positive behavior.
• The reaction route at MessagingWorker.kt:217-233 parses chatId but does not bind membership or prove that messageId belongs to that chat. Commit requires member(principal, path.chatId) and message.chatId == path.chatId; a cross-room message ID denies.
• Unknown authenticated frames currently reach the fallback broadcast at ChatService.kt:426, and the smoke path uses __raw-do. Both require explicit protocol treatment as described in section 13.
• NotificationWorker.kt:7-12 currently uses the default auth-disabled worker construction, while debug/PubSub hello routes in NotificationRoutes.kt are exposed and an E2E expects unauthenticated debug state. The release gate must reverse that expectation and ensure denial/audit logs contain no notification title or body.

11. Persistence and effect protocol

Reaktor needs a portable semantic contract above individual databases, not an abstraction that pretends all databases have identical capabilities.

11.1 Minimum storage contract

Every authoritative mutation declares:

• aggregate/resource identity;
• expected revision or conflict policy;
• operation ID and idempotency key;
• principal/tenant context;
• schema version and migration path;
• transaction boundary;
• emitted events/outbox records;
• retry and duplicate semantics;
• consistency/read mode;
• retention and deletion policy.

data class OperationEnvelope<T>(
    val operationId: OperationId,
    val idempotencyKey: IdempotencyKey,
    val aggregate: AggregateRef,
    val expectedRevision: Revision?,
    val principal: PrincipalRef,
    val tenant: TenantRef?,
    val schema: SchemaId,
    val payload: T,
    val causationId: OperationId?,
    val correlationId: CorrelationId,
)

An operation result reports Applied, AlreadyApplied, Conflict, Rejected, or FailedUnknown. “Timed out” is not evidence that a mutation did not occur.

11.2 Inbox, outbox, and sagas

For service and worker delivery:

• an inbox deduplicates received operations before domain effects;
• an outbox records domain change and outbound message in one local transaction;
• the dispatcher retries idempotently and marks delivery separately;
• multi-resource workflows use an explicit saga or compensation protocol;
• irreversible effects are labeled and cannot claim automatic rollback.

BestBuds message send and reaction are the first envelope slice; media, moderation, notification, and timeline synchronization adopt the same identity in subsequent staffed slices. Current paths around MessagingService.kt:209-219,229-242,401-424,442-470, MessagingWorkerRepository.kt:45-129, MessagingWorker.kt:148-233, and ChatTimelineInteractor.kt:108-210 expose the concrete deduplication, revision, offline-reconciliation, and retry work.

The current send path commits the message row before moderation and notification dispatch, while dispatch failure may only be logged. The durable outbox acceptance test injects a crash after database commit and before each outbox insert, dispatch, and acknowledgement. Recovery must yield one logical message plus eventual one logical moderation job and one notification per intended recipient, each with durable delivery state. If media or notification adoption is deferred, the release notes must say which effects remain best-effort.

Reaction toggling currently performs a read followed by delete-or-insert and fetch without one transaction/CAS. Its contract must define concurrent duplicate and reordered requests. The reference implementation should be linearizable at the message/user/emoji observation boundary, and reuse of one idempotency key with a different payload must be rejected.

11.3 Desired state versus observed state

Optimistic UI state is a projection, not a second authority. A client command creates a pending operation with a stable ID. The timeline shows pending/accepted/rejected/reconciled state. Server acknowledgements and socket echoes carrying the same operation ID converge on one logical item.

Principal partitioning also applies to telemetry. Today analytics events do not capture a principal at enqueue, share a global analytics_pending_v1 queue, and are assigned to the bearer user at a later flush. The required regression is: user A enqueues → process dies or stays offline → A logs out → B logs in → flush. No A or anonymous event may be attributed to B. The envelope and store key capture principal/tenant at enqueue, and logout has an explicit drain, quarantine, anonymize, or delete policy.

The storage documentation should publish a matrix rather than promise universal transactions:

CRDTs should be introduced only for fields with a declared join-semilattice and product-correct merge meaning. “Offline first” is not permission to turn every record into last-writer-wins.

12. Actor semantics

Reaktor should specify actors locally before claiming distributed location transparency.

12.1 Honest current guarantee

The existing actor implementation provides a useful local mailbox/processing abstraction with coroutine execution and lifecycle integration. It does not yet, as one unified contract, guarantee durable exactly-once effects, replay-safe recovery, distributed identity, fencing, supervision trees, or transparent failover.

12.2 Target local actor contract

Use a pure reducer and explicit effects:

data class ActorStep<S>(
    val state: S,
    val effects: PersistentList<ActorEffect>,
    val disposition: MessageDisposition,
)

fun interface ActorReducer<S, M> {
    fun reduce(state: S, message: Envelope<M>): ActorStep<S>
}

sealed interface MessageDisposition {
    data object Ack : MessageDisposition
    data class Retry(val after: Duration) : MessageDisposition
    data class Reject(val reason: Finding) : MessageDisposition
    data class DeadLetter(val reason: Finding) : MessageDisposition
}

The runtime serializes reducer steps per actor identity. Effects execute outside the reducer and post completion messages back through the mailbox with actor epoch, sequence, causation ID, and idempotency key. Stale completions are rejected by fencing.

Required properties:

• reducer determinism for the same state/message/environment input;
• mailbox FIFO only within a documented sender/partition scope;
• one explicit disposition per delivery;
• no effect before durable state/inbox commit where durability is promised;
• restart increments epoch and rejects older completions;
• stop/quiesce behavior is specified for queued and in-flight messages;
• supervision decisions are values and are observable;
• dead letters preserve safe metadata and cause, not secret payloads by default.

12.3 Distributed actors come later

Remote actors require a real protocol: stable logical identity, placement revision, fencing token, durable inbox/outbox, retry budget, lease/ownership model, migration state, and split-brain behavior. Until those exist, Reaktor should describe remote actors as explicit service/gateway adapters—not location-transparent references.

13. Choreography and session protocols

An enum naming HTTP, WebSocket, worker, or another transport is not an end-to-end protocol. Reaktor should model multiparty interactions explicitly.

sealed interface GlobalProtocol {
    data class Send(
        val from: Role,
        val to: Role,
        val tag: MessageTag,
        val schema: SchemaId,
        val next: GlobalProtocol,
    ) : GlobalProtocol
    data class Choice(val at: Role, val branches: Map<BranchTag, GlobalProtocol>) : GlobalProtocol
    data class Recur(val variable: RecVar, val body: GlobalProtocol) : GlobalProtocol
    data class Continue(val variable: RecVar) : GlobalProtocol
    data object End : GlobalProtocol
}

For the supported finite protocol language, the compiler checks multiparty coherence, projectability, and branch mergeability, then projects the global protocol into local endpoint state machines. Asynchronous ordering, buffering bounds, delivery, and fairness assumptions are explicit. Runtime monitors enforce:

• allowed sender, receiver, tag, and schema at each state;
• branch ownership;
• recursion and termination;
• timeout, cancellation, reconnect, and retry transitions;
• authorization context and room/session membership;
• protocol and schema version negotiation;
• duplicate/replay behavior.

The target BestBuds chat protocol must cover connect/authenticate, membership, join, history, publish, acknowledge, reaction, presence, reconnect, timeout, and leave. The current Playwright socket test (tests/chatServer/playwright/socket.spec.mjs:26-62) proves only a signed-token connection path; it is not evidence for the complete protocol. Generated tests must cover legal and illegal orderings, malformed/unknown frames, token expiry, reconnect, duplicate acknowledgement/echo, backpressure, and close codes. Monitor soundness (every accepted trace is legal) and completeness for the supported bounded language (every legal trace is accepted) are both required; reject-all is not a conforming monitor.

Unknown frames must close or produce a typed error under the protocol. They must not fall through to the current generic broadcast path. The current __raw-do smoke-test frame must be removed from production parsing or restricted to an authenticated development/service-only protocol.

14. FFI, FlexBuffers, and code replacement

14.1 Validated payloads

The current FlexBuffer validator and hardening tests are a strong foundation. Validation should be encoded in the type boundary:

sealed interface IncomingFlexPayload
data class UntrustedFlexPayload(val bytes: ByteArray) : IncomingFlexPayload

class ValidatedFlexPayload<S : FlexSchema> internal constructor(
    private val ownedBytes: ImmutableBytes,
    val schema: SchemaId,
    val version: UInt,
    val rootType: FlexRootType,
    val digest: PayloadDigest,
) {
    internal fun readOnlyView(): FlexReadView = ownedBytes.readOnlyView()
}

Validation takes a defensive copy or exclusive immutable/native ownership so caller mutation cannot invalidate the result. Decoders and FFI calls accept ValidatedFlexPayload<S>, not arbitrary bytes. Validation includes total size, depth, table/vector bounds, offsets, strings, schema/version, resource limits, and expected root type. Today public decode paths in reaktor-flexbuffer/src/commonMain/kotlin/dev/shibasis/reaktor/flexbuffer/core/FlexBuffers.kt:120-126,174-180 still accept arbitrary bytes; closing or clearly marking those unsafe paths is part of the stable API gate.

14.2 Canonical call envelope

Cross-language calls need one portable versioned wire envelope containing:

• magic and envelope version;
• contract and schema IDs/versions;
• call ID, operation ID, correlation, and causation;
• request, response, stream item, end, error, cancel, and credit tags;
• status/error model;
• deadlines and cancellation semantics;
• maximum lengths and nesting;
• authority/effect context or a verifiable reference to it.

A separate process-local ABI descriptor carries address/handle, length, allocator, mutability, ownership-transfer mode, lifetime, and release callback. Pointer addresses and callbacks are never serialized as transport-independent wire metadata.

Generated bindings must run ABI compatibility tests across Kotlin/JVM, Kotlin/Native, JS/Wasm, C/C++, and any Swift or Java consumers. Sanitizers and boundary fuzzing belong in release gates for native adapters.

14.3 Signed bundle manifest

Code or logic replacement must operate on a signed, content-addressed manifest:

BundleManifest
  bundle digest
  publisher identity and signature
  compatible kernel/runtime/schema ranges
  exported component/contract IDs
  effect and authority ceiling
  state schema + forward/backward migrations
  resource limits
  provenance/SBOM
  test and verification attestations
  rollback compatibility

The signed bytes are the canonical manifest with the signature field excluded, bound to manifest schema, canonicalizer, publisher key ID, and bundle digest. Signature verification and content hashing occur before any payload or migration code is loaded.

14.4 Replacement protocol

Idle → Prepared → Quiescing → Migrating → Swapped → Probing → Committed
             ↘ Rejected      ↘ RolledBack ← Failed ←───────────┘

The first supported production scope should be stateless logic replacement with no authority expansion and a fully reversible swap. Stateful replacement is enabled only when:

• state schema migration is deterministic and tested;
• old code remains available until commit;
• in-flight work follows a defined drain/replay rule;
• fencing prevents old and new activations from writing concurrently;
• health probes are semantic, not just process liveness;
• irreversible external effects are excluded or handled by explicit compensation.

Automatic rollback cannot undo an email already sent, a payment captured, or a remote destructive API call. The plan must say so before approval.

15. Capabilities and graceful degradation

Platform branching should be a constraint-resolution problem.

data class Requirement(
    val capability: CapabilityId,
    val range: VersionRange,
    val requiredProperties: PropertySet,
    val fallbackPolicy: FallbackPolicy,
)

data class Offer(
    val capability: CapabilityId,
    val implementation: NodeId,
    val properties: PropertySet,
    val evidence: EvidenceSet,
)

sealed interface Resolution {
    data class Selected(val strategy: NodeId, val evidence: EvidenceSet) : Resolution
    data class Degraded(val strategy: NodeId, val missing: Set<Property>) : Resolution
    data class Unsatisfied(val findings: List<GraphFinding>) : Resolution
}

The compiler/runtime resolves requirements against observed offers. A fallback is a named strategy with known loss, not an if (platform == ...) string branch hidden inside business logic.

Example: BestBuds notification delivery may resolve to native push, web push, in-app-only, or unavailable. Each mode states persistence, latency, background, permission, and privacy properties. The UI can then explain the exact degradation.

16. Provenance and truth dimensions

A single ordinal such as “truth class” cannot faithfully rank source code, desired configuration, provider observation, inference, simulation, test evidence, and formal results. They are different dimensions.

data class SignalEnvelope<T>(
    val value: T,
    val subject: SubjectRef,
    val graphRevision: Revision?,
    val source: EvidenceSource,
    val observedAt: Instant,
    val validAt: Instant?,
    val expiresAt: Instant?,
    val confidence: Confidence?,
    val method: MethodRef,
    val assumptions: Set<AssumptionRef>,
    val signature: SignatureRef?,
)

The workbench should render at least:

• desired — declared by source, manifest, policy, or approved plan;
• observed — returned by a named provider/runtime at a timestamp;
• derived — computed from named inputs and method;
• simulated — produced by a model or replay, not the live system;
• checked — validated/tested/model-checked under stated bounds;
• attested — signed record of an executed process;
• unknown/stale/conflicted — insufficient, expired, or contradictory evidence.

No UI should turn “configuration says enabled” into a green live-health indicator.

17. Visitors, queries, rewrites, and analyses

Visitors should run over immutable snapshots and return explicit artifacts.

interface GraphQuery<R> {
    fun evaluate(graph: CertifiedGraph, controls: QueryControls): QueryResult<R>
}

data class QueryControls(
    val direction: Direction,
    val order: TraversalOrder,
    val boundary: BoundaryPolicy,
    val maxNodes: Int,
    val cancellation: CancellationProbe,
)

interface GraphRewrite {
    fun propose(graph: CertifiedGraph): RewriteResult // contains GraphPatch, never mutation
}

Traversal semantics must specify root inclusion, direction, ordering, duplicate handling, containment crossing, pruning, cancellation, and resource bounds. Breadth-first and depth-first implementations must not silently disagree about these basics.

Useful result types include:

• findings with precise node/port/edge/source locations;
• route and reachability proofs/counterexamples;
• impact and test-selection sets;
• authority/effect closure;
• deployment partitions and inserted gateways;
• lifecycle order;
• protocol conformance findings;
• normalized matrices for spectral analysis;
• proposed patches with preconditions.

Visitors are pure analyses. Effectful work belongs in a separately approved plan derived from their output.

18. Tooling, agents, and the control plane

The existing tooling model is one of the strongest design seeds in Reaktor. Preserve the separation between discovery, planning, safety classification, approval, fingerprinting, execution, and event evidence.

An agent or visual editor never receives a general “poke the runtime” primitive. It receives tools such as:

• read a snapshot or evidence graph;
• run a pure query;
• propose a typed patch;
• request compilation and validation;
• inspect the exact plan/diff/fingerprint;
• request approval for a classified effect;
• execute an approved plan through its owning adapter;
• observe reconciliation and rollback evidence.

The approved fingerprint covers:

• source and target graph revisions;
• normalized patch;
• compiler and policy versions;
• derived effects and authority change;
• target environment and resource identities;
• required tests/migrations;
• rollback/compensation classification.

Changing any of those invalidates approval. Agent identity, model/configuration, prompts or policy references, tool calls, input evidence, output patch, reviewer, and result belong in the audit record. This is not a demand to expose private chain-of-thought; it is a demand to record reproducible operational inputs and decisions.

19. Theory inventory: what the architecture actually uses

The framework should be explicit about which theoretical ideas are implemented, partial, or future.

This table is deliberately conservative. A concept appearing in a design document or enum does not make its semantics implemented.

20. Verification architecture

No single formal tool fits every Reaktor property. Use a portfolio with precise responsibility.

20.1 Lean 4: pure kernel theorems

Use Lean 4 for finite, pure semantic objects and algebraic theorems:

• per-operation preservation from independent primitive preconditions, for example WFStatic(g) ∧ preAddEdge(g,e) ⇒ WFStatic(addEdge(g,e));
• executable-certifier soundness: certify(raw) = ok(cg) → WFStatic(cg.state);
• failed-patch no-op at the semantic level;
• normalization idempotence and deterministic digest input;
• structural composition associativity and identity modulo the defined alpha-renaming/isomorphism relation and premises;
• authority non-amplification under composition and attenuation;
• coherence/projectability and local-monitor soundness for the supported finite protocol language;
• reducer determinism for generated pure reducer models;
• schema migration round-trip properties where reversibility is claimed.

The Lean model should be small and mathematical. valid must not be defined as “apply and then check WFStatic,” which would make the preservation theorem tautological. Define primitive preconditions independently, prove preservation per operation, and prove the executable certifier sound against the specification. Do not attempt to formalize Kotlin coroutines, databases, Compose, or cloud SDKs directly.

20.2 TLA+/PlusCal and TLC: temporal protocols

Use TLA+ for state machines and adversarial interleavings:

• graph authority compare-and-swap with concurrent proposers;
• activation/quiesce/close and failure cleanup;
• actor mailbox, retry, crash, recovery, epoch fencing, and duplicate delivery;
• inbox/outbox dispatcher and ambiguous timeout;
• BestBuds send/socket-echo/retry/offline reconciliation;
• chat join/publish/reconnect/leave authorization;
• code-replacement prepare/quiesce/migrate/swap/probe/rollback;
• deployment plan approval, expiry, execution, and reconciliation.

Safety properties answer “nothing bad happens.” Liveness properties require explicit fairness and environment assumptions. Model-check reports must publish bounds such as actors, messages, revisions, retries, failures, and queue sizes.

20.3 Apalache: bounded symbolic checking

Use Apalache where symbolic bounded checking complements explicit-state TLC, particularly for parameterized finite data and invariant counterexamples. Publish the exact command and pinned version, including invariant (--inv), path length (--length), solver/configuration, finite constants, and assumptions. Report “no invariant counterexample within the stated bound.” Use TLC for fairness/liveness properties; do not assume a TLC temporal PROPERTY is checked equivalently by Apalache outside its supported fragment.

20.4 Alloy: structural counterexamples

Use Alloy for finite structural models:

• containment cycles and ownership uniqueness;
• boundary closure and gateway insertion;
• port cardinality and compatibility relations;
• deployment partitions and forbidden cross-zone edges;
• authority/resource relations;
• protocol-role topology.

Alloy is especially valuable early because it finds small counterexamples to plausible but incorrect structural rules. As with temporal checking, scope is part of the result. Every gate records exact scope, bitwidth, solver, and command, and includes satisfiable run witnesses alongside check; an empty model is not evidence that an invariant is useful.

20.5 Lincheck and platform concurrency tests

Use Kotlin Lincheck only for Reaktor-owned JVM concurrent objects with explicit sequential specifications, such as a custom snapshot CAS store, registry, or queue. Record operations, sequential spec, threads, iterations, seeds, JVM, and tool version. It does not verify coroutine channels, actor lifecycle, or KMP semantics. Use TLA+ trace conformance plus deterministic coroutine, stress, and fault tests for those; add JCStress where JVM memory-model behavior warrants it. Native and JS targets need platform-appropriate stress and race tooling.

20.6 Property, model, differential, fuzz, and fault testing

Every semantic subsystem gets executable tests derived from the same model:

• property generators for graphs, patches, contracts, schemas, and policies;
• model-based command sequences compared with the implementation;
• differential runs across JVM, JS/Wasm, and native interpreters;
• construction-order and serialization round-trip metamorphic tests;
• wire/ABI fuzzing with hostile lengths, offsets, versions, and cancellations;
• fault injection at every persistence and rollout transition;
• crash/restart and duplicate/reorder tests for actors and workers;
• authorization negative tests for every route, edge, frame, and resource pattern;
• deterministic replay from recorded operation envelopes.

20.7 Differential conformance and translation validation

The formal model and Kotlin implementation will not be identical artifacts. Finite sampled fixture/trace agreement is differential or model-based conformance testing. Reserve translation validation for an independent checker run on every generated artifact against the exact certified source. Both use an explicit observation relation:

1. Serialize a canonical input snapshot/patch/trace.
2. Evaluate it in the reference semantic model.
3. Evaluate it in each platform implementation.
4. Normalize observations.
5. Compare results, findings, next revision, and emitted abstract effects.
6. Store the counterexample or signed attestation.

Generated registries, platform manifests, and endpoint monitors are translation-validated only when every emitted artifact is independently checked against its exact certified graph/source map. Sampled platform execution remains differential evidence and publishes corpus/coverage.

20.8 Non-vacuity and coverage controls

Every formal gate proves that the model can do intended work as well as reject bad work:

• Lean builds with a pinned toolchain, no sorry, and a recorded #print axioms result for release theorems.
• Alloy includes satisfiable witnesses, mutated counterexamples, scope, bitwidth, and solver.
• TLA+ records reachable milestones, enabled/action coverage, deadlock result, state counts, fairness, seed/configuration, and replayable counterexamples.
• Validators accept a valid generated corpus and reject targeted law-breaking mutations; reject-all cannot pass.
• Auth evaluators include allowed witnesses as well as denials; deny-all cannot pass.
• Protocol monitors accept every supported generated legal trace and reject illegal mutations; reject-all cannot pass.
• Property/fuzz jobs publish generators, seeds, case counts, coverage where available, and sanitizer configuration.

20.9 Trusted computing base

Every proof package lists what remains trusted, including as applicable:

• Lean kernel and definitions;
• model-to-code mapping and serializers;
• Kotlin compiler/runtime and target backend;
• cryptographic implementation and key custody;
• generated bindings and native toolchain;
• database guarantees actually relied upon;
• cloud/provider behavior outside the model;
• build provenance and artifact-signing infrastructure.

The trusted base should shrink over time, but it can never be replaced by marketing language.

21. Verification obligations by subsystem

21.1 Graph kernel

• WFStatic is decidable for finite snapshots under finite total kernel/registry DSLs.
• Normalization is idempotent.
• Digest input is canonical.
• Each primitive patch operation's independent preconditions preserve WFStatic; executable certification is sound against the specification.
• Rejected patches are semantic no-ops.
• Structural composition is associative and has identity modulo the defined canonical-isomorphism relation and premises.
• Compiler output is independent of declaration iteration order.

21.2 Graph authority and runtime reconciliation

• At most one patch commits from a given expected revision.
• Readers never observe partial topology.
• Snapshot, revision, digest, journal, proposer/approval evidence, and certificate commit atomically or recover from a durable intent before publication.
• Approval binds to the exact complete PlanInput fingerprint and expiry.
• Runtime failure cannot rewrite desired state without another patch.
• Reconciliation is idempotent under repeated events.
• A closed activation cannot regain authority or publish current-epoch output.

21.3 Lifecycle

• No success callback occurs for an invalid transition.
• repeated closeAndJoin(x) is observationally equivalent to one completed close.
• Every acquired resource is released by closeAndJoin within the stated deadline; a leak finding is diagnosability and fails the stability gate.
• Acyclic dependencies close after dependents; permitted SCCs follow their barrier protocol.
• Cancellation reaches every owned coroutine/mailbox/subscription within the declared bound; a timeout/finding fails the stability gate.

21.4 Actors

• One reducer step per dequeued message.
• Exactly one disposition is recorded per delivery attempt.
• Effects cannot precede a required durable commit.
• Retry plus crash does not create more than one logical application for an idempotent operation.
• Older epochs cannot commit after fencing.
• Recovery preserves the documented ordering and dedupe contract.

21.5 Choreography

• Global roles are coherent/projectable and local branch projections are mergeable under the stated asynchronous semantics.
• A runtime monitor accepts only legal local traces and accepts every legal trace in the supported bounded language.
• Unknown tags, wrong roles, and incompatible schema versions fail closed.
• Reconnect cannot reuse expired authority or revive a terminal session.
• Liveness claims name fairness, availability, and retry assumptions.

21.6 Persistence

• Revision checks prevent lost updates where promised.
• Idempotency keys make repeated same-payload operations observationally equivalent to one logical operation at a named boundary; reusing a key with different payload rejects.
• Inbox/outbox atomicity holds within the stated backend transaction scope.
• Ambiguous failure is exposed as FailedUnknown, not incorrectly mapped to rejection.
• Offline reconciliation cannot cross principal or tenant partitions.

21.7 Authority

• Default deny for effectful operations without a matching grant.
• anyOf, allOf, and negation obey their Boolean specifications.
• Resource type and ID are both enforced under explicit wildcard rules.
• Composition and adapters do not amplify authority.
• Cached decisions are invalidated by policy, principal, resource, graph revision, and expiry changes.

21.8 FFI and bundles

• Unvalidated bytes cannot reach typed accessors through the stable API.
• Bounds, ownership, cancellation, and version mismatches fail without memory unsafety.
• Generated bindings agree on envelope vectors across supported languages.
• Bundle signatures, digests, compatibility, authority ceilings, and migrations are checked before activation.
• Rollback is only claimed for effects covered by the rollback model.

22. Verification claim policy

Every published assurance claim should use this template:

Subject: graph patch preservation, kernel schema v1
Claim: AddEdge with independent preconditions preserves WFStatic
Evidence: Lean theorem Kernel.Patch.addEdgePreservesWFStatic
Assumptions: finite maps; independent primitive preconditions; listed primitive operations only
Implementation link: translation suite kernel-patch-v1
Artifact: source digest, toolchain digest, proof/check report digest
Limitations: says nothing about external reconciliation effects

Bounded checks add:

Bounds: 3 actors, 5 messages, 2 crashes, 2 retries, 4 revisions
Fairness: weak fairness for enabled dispatcher action
Result: invariant holds / counterexample

Forbidden statements unless literally justified:

• “Reaktor is formally verified.”
• “Exactly once” without defining the observation boundary and idempotency assumptions.
• “Automatic rollback” for irreversible external effects.
• “Location transparent” without failure, fencing, and delivery semantics.
• “Secure by construction” when enforcement depends on callers choosing a wrapper.
• “All interleavings checked” without finite bounds or an unbounded proof.

23. Migration without a big bang

The existing runtime and BestBuds integration should remain usable while the foundation is introduced.

23.1 Strangler sequence

1. Define typed stable IDs, GraphState, GraphPatch, findings, and the certification predicates in a new kernel module.
2. Write adapters from GraphDocument and the current runtime graph into untrusted snapshots.
3. Compile/certify snapshots in shadow mode and compare them with current runtime wiring.
4. Generate manifests and source maps without changing execution.
5. Route editor and tooling changes through GraphAuthority, while adapting accepted patches back to the old runtime.
6. Introduce owned runtime handles and session-scoped features.
7. Move port matching into the compiler and compare binding plans with current autoWire results.
8. Turn mismatches into blocking errors in development, then CI, then production activation.
9. Move product mutations one vertical slice at a time: BestBuds chat first, then messaging/offline timeline, then notifications, then broader app state.
10. Delete direct topology mutation and global correctness paths only after usage telemetry and repository search show no remaining callers.

23.2 Compatibility policy

For every migration boundary, publish:

• source schema version;
• runtime compatibility range;
• generated artifact version;
• migration/alias table;
• fallback behavior;
• deprecation date and removal gate;
• test fixtures containing at least the oldest supported and next planned version.

Adapters are temporary and observable. An adapter without an owner and removal criterion becomes a second semantic system.

23.3 Executable module and data migration matrix

The target dependency arrows are explicit:

This reverses current dependency pressure gradually: reaktor-graph presently exports service/UI/DB surfaces, and server portions of core pull large concrete frameworks. Compatibility modules remain at the outside until callers move; none of those dependencies enter the kernel.

Every phase publishes KMP support separately for JVM, Android, iOS/native, JS, and Wasm: compile, serialization golden corpus, lifecycle/ownership, concurrency/fault facilities, FFI where applicable, and known unsupported behavior. Performance budgets cover normalized compile time, snapshot size, activation overhead, steady-state dispatch overhead, and close latency. Each adapter has an owner, staffing estimate, telemetry, removal gate, and recovery procedure.

24. Ninety-day execution program

Ninety days is a credible P0 foundation slice, not a promise to complete universal authorization, durable actors, session-type code generation, cross-target FFI, live code replacement, and a verification UI at once. The sequence assumes a small dedicated team; owners and capacity must be assigned before dates become commitments.

Days 1–20: freeze, characterize, and fix immediate contradictions

Deliverables

• Foundation ADR, target dependency matrix, stable-ID rules, evidence vocabulary, toolchain lock, and performance baselines.
• Inventory of direct topology mutation, global features, unowned coroutine/resource paths, edge construction/disconnect/attach paths, container closure, auth boundaries, worker retries, and raw binary decoders.
• Failing characterization tests for lifecycle invalid callbacks, parent-job replacement, partial bulk connect, public invalid Edge construction, stale disconnect entries, cross-graph attach, and child-graph closure.
• Auth fixes/tests for mixed anyOf semantics, resource type/ID, BestBuds room membership at token mint/connect, reaction room binding, unknown frames, and notification debug/PubSub routes.
• Product isolation regressions: two simultaneous runtime scopes; repeated Android Activity/iOS controller create-dispose; login→logout during hydration; chat A close→chat B while A work completes; analytics A enqueue→B login→flush.

Exit criteria

• Existing targeted suites remain green and every named defect has a failing-before/passing-after test or a documented deferral owner.
• Non-members fail both room-token mint and socket connect; membership revoked between stages fails; active revocation prevents further effects.
• Cross-room reaction IDs deny, notification production debug routes return 404, and queued A/anonymous analytics cannot be attributed to B.
• Recreate/dispose tests finish with zero owned jobs, listeners, sockets, observers, or stale UI commits—not merely a leak report.

Days 21–45: static kernel v0 and lossless shadow adapters

Deliverables

• reaktor-kernel with typed IDs, immutable GraphState, finite facet/contract registry, canonicalization, digest wrapper, findings, complete patch schema, and WFStatic certifier.
• Lossless adapters from GraphDocument and current runtime export, including explicit current edge orientation and ID aliases.
• Property/metamorphic generators and serialization corpus across declaration permutations, invalid mutations, oldest/current/next formats, and one BestBuds slice.
• One Alloy model for identity, ownership, containment, endpoints, cardinality, and boundary closure, with run witnesses and mutated counterexamples.
• Pinned Lean project scaffolding with named definitions and release commands.

Exit criteria

• Permuting declaration order over a published generated corpus yields byte-identical normalized snapshots/digests; repeating one input alone does not satisfy this criterion.
• Each single-law invalid mutation produces at least one finding naming the exact subject ID and source; results cap cascades explicitly and never substitute a stack trace.
• Shadow export preserves all current nodes, ports, endpoints, containment, registered facets, and source mappings, or reports a blocking unsupported field.
• Alloy report records exact scope, bitwidth, solver, witnesses, checks, and replayable counterexamples.

Days 46–70: single-process authority prototype and owned lifecycle

Deliverables

• Pure per-operation patch planning with independent preconditions and complete PlanInput fingerprint.
• Single-process GraphAuthority with atomic snapshot+journal commit (or tested write-ahead recovery), checked revision overflow, and compensating rollback patches.
• Session-owned RuntimeHandle.closeAndJoin, durable epoch/fence abstraction, explicit SCC activation barriers, and compatibility facade that fails on ambiguous session.
• Fixes for current lifecycle/ownership blockers plus deterministic close/failure aggregation tests.
• One small TLA+ model for concurrent same-revision proposals and crash around durable publish/journal.
• Lean theorems for normalization idempotence and certifier soundness or one primitive patch preservation theorem; pinned lake build, no sorry, recorded #print axioms, theorem/source/toolchain digests.

Exit criteria

• Failed patches are observational no-ops; same-revision concurrency yields one committed record; crash injection cannot publish state without recoverable journal/certificate.
• closeAndJoin releases every owned resource under success and injected acquisition/close failures within a stated deadline.
• TLA+ report includes reachable commit/recovery milestones, action coverage, deadlock/state counts, finite bounds, and a replayable counterexample harness.
• Lean CI fails on sorry/unexpected axioms and produces reproducible artifacts; if the named theorems are not complete, the release claim is “proof scaffolding,” not “proved kernel.”

Days 71–90: one BestBuds vertical proof and P0 decision

Deliverables

• Compile and certify the selected BestBuds chat/messaging graph slice in shadow mode while the existing runtime still executes it.
• Introduce stable operation/idempotency identity through one send-message path and bind pending/REST/database/socket observations to it.
• Transactional, room-bound reaction mutation or an explicit deferral that removes it from the P0 claim.
• Durable message outbox pilot for moderation and notification, with crash points around commit/insert/dispatch/ack.
• Exact report joining kernel snapshot, product tests, Alloy, Lean, TLA+, tool versions, bounds, limitations, and source/artifact digests. A CLI file/report is enough; no workbench badge system is required in P0.

Exit criteria

• Reuse of one idempotency key and same payload is one logical send at the documented UI/database/socket observation boundary; reuse with a different payload rejects.
• Crash after message commit cannot lose the declared durable moderation/notification work or create duplicate logical effects; any still-best-effort effect is excluded from the claim.
• Socket membership/revocation, unknown/malformed frames, reaction cross-room checks, analytics principal isolation, and real product lifecycle race tests pass.
• The P0 review either accepts the static kernel + authority/lifecycle + product slice or publishes concrete blockers. Protocol codegen, distributed actors, generalized reference monitoring, cross-target FFI, and code replacement remain later tracks.

25. Longer roadmap after the foundation

Treat these as staffed six-to-twelve-month tracks with independent gates, not as the tail of P0:

1. Deterministic wiring/compiler track: generated stable registries, constraint solver, ambiguity UX, current-autoWire shadow diff, translation-validated target manifests, and performance budgets.
2. Universal authority track: reference monitor at every effect boundary, finite policy semantics, decision-cache invalidation, non-vacuity tests, and product migrations beyond chat.
3. Durable effects/actors/workflows track: operation protocol adoption, inbox/outbox, pure reducers, durable epochs/fencing, supervision, timers, compensation, and only then remote placement.
4. Choreography track: finite global protocol DSL, multiparty coherence/projectability/mergeability, generated monitors, async trace model, chat rollout, then other services.
5. FFI/polyglot track: immutable validated payload API, portable envelope and local ABI split, cross-language golden corpus, fuzz/sanitizers, TypeScript/C++ hardening, then Python research.
6. Code-replacement track: signed stateless bundles first; stateful replacement only for carefully bounded state machines with reversible migrations and effect exclusions.
7. Evidence/control-plane track: proof/check attestations, desired/observed provenance, IDE/MCP/A2A query and patch interfaces, deploy reconciliation, and human-readable evidence UI.
8. Data/distribution track: selective CRDT fields, deployment graph compilation, broader providers, and platform compatibility only after differential and ownership suites pass per target.

The ordering matters. CRDTs before canonical identity/revision, distributed actors before fencing/durability, or arbitrary hot patching before effect accounting would add complexity while weakening the foundation.

26. Acceptance gates

26.1 A module may be labeled “stable” only when

• its semantic contract is versioned and testable;
• public IDs and wire/schema compatibility rules are documented;
• ownership and close semantics are explicit;
• authority/effect boundaries fail closed;
• invalid and failure paths have tests;
• platform support is stated per target rather than inferred from commonMain;
• generated artifacts have reproducible inputs and source maps;
• claims link to evidence and limitations;
• migration and deprecation policy exists;
• there are no known critical contradictions between documentation and code.

26.2 P0 foundation release gate

• canonical snapshot and patch formats are frozen as version v1;
• WFStatic is used by compiler/editor/import paths, while activation, transition, runtime, protocol, and reconciliation use their named predicates;
• topology mutation is single-authority and revisioned;
• canonical graph export/adapters pass declaration-permutation and invalid-mutation tests;
• runtime activation is owned and leak-checked;
• auth fixes and mandatory monitor are active for the reference slice;
• operation IDs survive client, service, worker, database, and socket observations for the selected send path;
• proof/model/property/concurrency reports are reproducible in CI;
• BestBuds reference scenarios pass with injected duplicates, delays, crashes, reconnects, and denials.

26.3 Production code-replacement gate

• signature and content digest verified;
• compatibility and authority ceilings checked;
• exact state migration and rollback scope stated;
• quiesce and fencing bounded-model-checked and fault-tested for the stated subset and bounds;
• semantic health probes pass;
• old artifact retained through commit window;
• irreversible effects either excluded or explicitly approved with compensation;
• audit evidence complete and recoverable without the workbench UI.

27. Risks and non-goals

Risks

• Two graph truths during migration. Mitigate with adapters, shadow comparison, digests, and a dated removal gate.
• Formal model drifts from Kotlin. Mitigate with shared fixtures, trace comparison, translation validation, and model-to-source mapping in review.
• Kernel grows into another framework. Enforce dependency rules and require every type to participate in a law or compatibility boundary.
• Generated metadata becomes stale. Make generation incremental but fail CI on source/manifest digest mismatch.
• Security monitor becomes optional for performance. Compile it into effectful invocation paths and benchmark/cache decisions safely; never offer a bypass mode in production.
• BestBuds-specific policy contaminates the kernel. Keep room membership, message policy, and notification behavior in product schemas/policies interpreted by generic mechanisms.
• Tooling polish outruns correctness. Render desired, observed, and checked evidence separately and block unsupported actions regardless of UI affordance.
• Build/toolchain drift invalidates evidence. Record toolchain digests and rerun compatibility/proof suites when compilers or generators change.

Non-goals

• Proving the whole Kotlin Multiplatform application stack correct.
• Inventing custom cryptography instead of using audited standards and libraries. For group encryption, use the semantics of Messaging Layer Security, RFC 9420 rather than a home-grown group-key protocol.
• Treating all state as CRDT-compatible.
• Providing arbitrary production hot patching.
• Promising exactly-once physical delivery across independent systems.
• Treating eigenvectors as runtime component primitives.
• Using a visual graph file as the only source of truth without stable IDs, schemas, source maps, and code generation.
• Hiding provider-specific consistency or failure semantics behind a deceptively uniform API.

28. Value created by this foundation

For developers

• deterministic wiring errors at build time instead of runtime surprises;
• reproducible graph snapshots and source-located findings;
• one mutation and approval protocol across code, CLI, desktop, and agents;
• explicit lifecycle ownership that makes tests and previews isolated;
• generated compatibility and negative tests;
• fewer platform conditionals in business code;
• confidence that “stable” has a concrete gate.

For BestBuds users

• fewer duplicate, missing, or cross-account messages;
• clearer offline/pending/retry behavior;
• chat membership and frame authorization enforced consistently;
• graceful explanation when a platform capability is unavailable;
• safer application updates and rollback;
• more trustworthy privacy and audit behavior.

For operators and investors

• architecture claims backed by reproducible artifacts rather than prose alone;
• reduced blast radius from typed plans, authority ceilings, and staged reconciliation;
• evidence-linked operational views;
• a credible route from product proof to reusable platform;
• a moat in deterministic cross-runtime semantics and verification, not simply in the number of modules.

Technical essay: an executable architecture for heterogeneous systems

Software products are no longer single programs. A consumer application may include Android and iOS clients, a web application, an edge worker, a JVM service, an actor that owns realtime state, a transactional database, an analytics store, object storage, notification providers, deployment scripts, dashboards, and background jobs. Each part can be well engineered while the whole remains difficult to understand. The system's real architecture is scattered across source code, dependency injection, routes, infrastructure manifests, database schemas, queue configuration, cloud consoles, and tribal knowledge.

Reaktor is an attempt to make that architecture executable.

Its central abstraction is a nested heterogeneous port graph. Nodes represent components at different scales: a UI screen, interactor, repository, service, actor, database projection, worker, native routine, or deployment resource. Ports expose typed contracts. Edges make flows and dependencies explicit. Containment gives the system hierarchy, so a developer can inspect an entire product and then enter one feature or request path. Visitors and compiler passes can traverse that structure to validate wiring, derive routes, install telemetry, analyze authority, select tests, propose deployment partitions, or explain the impact of a change.

This resembles Unreal Engine's Blueprint model in one important respect. Unreal combines a highly optimized runtime with a composition surface that allows different specialists to understand and build a complex system. Reaktor extends that idea from games to heterogeneous applications and distributed infrastructure. It does not require every algorithm to become a visual node. Source code remains the natural place for local logic. The graph captures the relationships that source files and independent cloud dashboards fail to show clearly.

Keeping a runtime graph creates opportunities that a build-only dependency graph cannot. A running system can identify which graph definition and revision produced an activation, which capabilities were selected on the device, which policy guarded an edge, which deployment owns a service, and which traces or failures belong to a component. A workbench or agent can ask questions against the actual revision instead of guessing from source. Explicitly replaceable regions can be quiesced and swapped. Telemetry and profiling can be correlated with the same identities used by the compiler and editor.

That runtime power also creates danger. If the runtime graph is a mutable collection of objects and global registries, then the visual editor, agent, application, and deployment layer can each invent a different truth. A failed wiring operation can leave half an update applied. A coroutine or actor can outlive the graph that created it. A hot update can expand authority or migrate state irreversibly. An authorization wrapper can be omitted by one caller. Reaktor becomes reliable only when those behaviors stop being conventions.

The stable foundation proposed here is therefore intentionally small. It consists of canonical identities, an immutable and versioned graph state, explicit port and protocol contracts, static/transition/runtime certification predicates, an effect and authority vocabulary, and a transactional patch algebra. Every graph change is first a value. It is applied to an immutable snapshot, validated, classified, fingerprinted, and approved before an atomic snapshot-plus-journal commit. Readers see the old or new revision, never a partial topology. Runtime resources reconcile to committed desired state through owned handles and observable lifecycle transitions.

This foundation changes the role of Reaktor's many modules. Actors, services, UI, databases, FFI, cloud adapters, tools, and product features are interpreters or extensions of the kernel; they do not independently redefine graph semantics. A module can add a node kind, schema, capability, visitor, or protocol, but it cannot bypass stable identity, topology authority, lifecycle ownership, or effect policy. This makes the system more extensible precisely because the base becomes harder to reinterpret.

Kotlin is a compelling language for this architecture. Kotlin Multiplatform reaches Android, JVM servers and desktop applications, iOS and other native targets, JavaScript, and Wasm while preserving a shared typed model. Sealed interfaces can encode closed patch and protocol languages. Value classes can distinguish identifiers and revisions that would otherwise be interchangeable strings. Coroutines and Flow offer a common implementation vocabulary for asynchronous calls and streams. KSP and compiler tooling can generate registries, schemas, source maps, endpoint monitors, and language bindings. Java interoperability opens a large production ecosystem, while native and JavaScript interop reach performance and dynamic environments.

Kotlin's reach is an enabler, not a proof. A coroutine does not define retry semantics. Flow does not establish backpressure across a process boundary. A generic type does not provide schema evolution. commonMain code does not guarantee that native, JVM, and JavaScript implementations have identical lifecycle or memory behavior. Reaktor must state those contracts above the language and test their interpretations on every supported target.

Polyglot execution is equally important. Kotlin can remain the semantic center, TypeScript and JavaScript can power browser, Worker, and Hermes-hosted logic, and C++ can provide native and high-performance kernels. Python can later connect scientific and machine-learning ecosystems. Reaktor FFI should not promise that these boundaries disappear. It should make them explicit through a canonical envelope: contract and schema versions, call and operation identities, request/response or stream tags, cancellation, credit, errors, authority, resource bounds, and buffer ownership. FlexBuffers may provide compact, directly accessible data, but untrusted bytes must still be validated and interpreted under a named semantic schema.

The same discipline applies across processes. Naming a transport “WebSocket” or “HTTP” says little about the legal conversation. A chat flow includes authentication, room membership, history, publish, acknowledgement, reaction, reconnect, timeout, and leave. A global protocol can describe those roles and branches. The compiler projects it into local client and server state machines; runtime monitors reject illegal frames. Choreographic programming then becomes a concrete way to prevent distributed endpoints from drifting, rather than a label attached to diagrams.

Actors benefit from similar honesty. The actor model is powerful because it combines identity, isolated state, serialized message handling, and supervision. A local coroutine mailbox is a useful start, but it is not yet a durable distributed actor. Reaktor should first define a pure reducer, explicit effects, one disposition per delivery, stable message identity, crash/retry behavior, and activation epochs that fence stale completions. Durable inboxes, outboxes, placement, leases, and split-brain policy can then support remote actors without relying on vague location transparency.

BestBuds is a strong forcing function for these ideas. Chat and messaging cross UI state, optimistic local updates, authentication, realtime sockets, workers, actors, PostgreSQL, notifications, retries, and offline behavior. A message can be locally pending, committed remotely, echoed by a socket, retried after an ambiguous timeout, and delivered as a notification. Stable operation identity and revisioned reconciliation let those observations converge on one logical event. Protocol monitors and a universal authority evaluator can ensure that only room members connect or publish. Session-owned runtime scopes can prevent one user's data, jobs, or sockets from surviving into another session.

For a developer, this architecture promises earlier and better errors. Ambiguous wiring fails during compilation with source-located findings. A graph patch shows its exact impact, required authority, affected tests, and rollback limits before it runs. Generated registries replace reflection-sensitive names. A component's lifecycle and platform requirements are visible. Debugging can follow one identity from source through runtime activation, service call, database operation, and deployment evidence.

For an end user, the benefits appear as product behavior rather than graph terminology: fewer duplicate messages, safer account switching, more reliable offline recovery, secure realtime rooms, clearer degraded modes when a device lacks a capability, and updates that fail safely. The user does not need to know that a session type or idempotency envelope produced the result.

For an operator, the graph can join desired configuration, observed provider state, telemetry, incidents, and approved changes without pretending those facts are identical. A deployment action is not just a button; it is a typed plan bound to a graph revision, artifact digest, environment, test set, authority grant, and rollback classification. An agent can propose the same kind of patch as a human editor but cannot bypass the validator or reference monitor.

For an investor or platform adopter, the defensible value is not a long list of modules. Breadth can be copied and can become maintenance debt. The deeper asset is a coherent semantic contract spanning code, runtime, polyglot boundaries, operations, and evidence. If Reaktor can make heterogeneous application architecture deterministic, queryable, safely mutable, and progressively verified, it offers leverage beyond a conventional app framework or AI code generator.

Formal verification should reinforce that value without exaggeration. Lean can prove algebraic laws of the small pure kernel, such as per-operation preservation under independent preconditions and certifier soundness. Alloy can find small structural counterexamples. TLA+ and Apalache can explore temporal protocols such as concurrent commit, actor recovery, inbox/outbox delivery, chat reconnect, and code replacement under bounded failures. Lincheck, property tests, platform differential tests, fuzzing, sanitizers, and fault injection connect those models to real implementations. Independent checking of every generated artifact can qualify as translation validation; sampled cross-platform agreement remains differential evidence.

This does not prove every line of a multiplatform product or every behavior of a cloud provider. The honest claim names the subject, theorem or invariant, assumptions, bounds, tool versions, and implementation evidence. That honesty is a strength: users can distinguish a mechanically proved kernel law from a bounded temporal check, a runtime validation, a test result, and a signed operational attestation.

Reaktor can increase the space of systems it expresses by adding powerful primitives, but the sequence is decisive. Canonical graph semantics come before distributed actors. Transactional patches and effect accounting come before arbitrary graph code push. Stable operation identity comes before offline merge strategies. Capability contracts come before adding more platform branches. Protocols come before claiming choreography. Evidence provenance comes before an AI workbench presents inferred state as truth.

The long-term vision remains ambitious: an executable architecture where Kotlin, TypeScript, C++, and later Python components participate in one typed graph; where UI, services, actors, data, workers, cloud resources, debugging, benchmarks, deployments, IDEs, and agents share stable identities and contracts; and where safe graph operations can reconfigure selected parts without full redeployment. The path to that vision is not more magic. It is a small verified core, explicit boundaries, controlled effects, and product evidence accumulated one vertical slice at a time.

That is why the base-layer program matters. If Reaktor makes BestBuds chat, messaging, lifecycle, auth, persistence, FFI, and updates predictable under retries, crashes, platform variation, and hostile input, it demonstrates more than an architecture diagram. It demonstrates a general method for building complex heterogeneous systems without losing the ability to reason about them.

29. Decision log

30. Immediate repository actions

The next implementer should begin with these concrete changes:

1. Add reaktor-kernel and move no runtime classes into it.
2. Write the GraphState/GraphPatch/GraphFinding schemas and version them before adding compiler behavior.
3. Convert current GraphDocument to/from the new state and property-test round trips.
4. Export the current runtime graph and compare it in shadow mode.
5. Add failing tests for the lifecycle callback, parent-job ownership, invalid public edge construction, partial bulk connect, stale disconnect, cross-graph attach, child-graph close, auth anyOf, resource type/id matching, non-member chat connection, cross-room reaction, notification debug routes, and unknown chat frames.
6. Introduce session-owned feature resolution behind the existing Feature facade.
7. Add operation/idempotency IDs end to end for one BestBuds send-message path.
8. Create the first Alloy model and TLA+ specs in a top-level verification/ directory with reproducible scripts and published bounds.
9. Add a CI job that produces a machine-readable VerificationAttestation and a human-readable report.
10. Refuse new distributed-actor, arbitrary code-push, or broad CRDT claims until the relevant acceptance gates in this document pass.

31. Source map

The line references below identify the audited code neighborhood as of 2026-08-27. Line numbers will move; stable follow-up documentation should migrate toward generated source anchors or symbol references.

Reaktor

BestBuds

32. Related Reaktor documents

• Graph Kernel Analysis — the broader universal graph vocabulary and module model.
• Reaktor Graph Refinement Plan — graph types, ports, controllers, actors, routing, and supervision refinements.
• Reaktor Component Lifecycle — lifecycle vocabulary across supported targets.
• Reaktor Actor Model — current actor design and roadmap.
• Auth Architecture — authentication and authorization surface.
• FlexBuffer Implementation — binary format and validator.
• Reaktor FFI — foreign-function boundary implementation.
• BestBuds Schema Hardening — product persistence and schema risk.
• Security Plan — broader security work.

33. Glossary

Activation — one running instance of a graph definition in a session and epoch.
Attestation — a signed record that named checks ran against named inputs; not automatically a proof.
Authority — permission for a principal to request an effect in a context.
Capability — an implementation's ability to provide behavior with stated properties.
Certified graph — a canonical snapshot accepted by the versioned WFStatic certifier under a named kernel and registry snapshot.
Contract — stable machine-readable interaction, schema, delivery, error, effect, and authority requirements.
Definition — a stable program-level component or graph identity.
Effect — an observable change outside a pure computation.
Epoch — a monotonically changing activation generation used to fence stale work.
Finding — a structured validation, policy, compatibility, or operational result with source location.
GraphAuthority — the sole topology mutation boundary that plans, validates, fingerprints, approves, and commits patches.
GraphPatch — a closed, versioned set of graph operations with an expected revision.
Open graph — a graph whose declared boundary permits typed composition with another graph.
Operation ID — stable logical mutation identity preserved across retries and transports.
Projection — a derived view or interpreter output from a canonical snapshot/evidence set.
Protocol monitor — a generated runtime state machine that accepts only legal local session traces.
Reconciliation — the process of making observed runtime/external state match committed desired state.
Revision — monotonically advancing semantic state version used for compare-and-swap and conflict detection.
Translation validation — independent checking of every generated artifact against the exact certified source; sampled behavior comparison is differential/model-based evidence.
Well-formedness (WFStatic) — the finite static snapshot predicate; transition, activation, runtime, protocol, normalization, and reconciliation have separate named invariants.

Closing position

Reaktor's most valuable idea is not that everything can be represented as a graph. Many systems can draw or traverse graphs. Its opportunity is to make one graph definition carry stable identity, contracts, authority, lifecycle, protocol, persistence intent, provenance, and operational evidence across Kotlin/JVM, Android, iOS, web, native, services, workers, databases, and tooling.

That opportunity depends on restraint. The stable base must be much smaller than the framework around it. It must be immutable before it is live, certified before it is activated, transactional before it is mutable, owned before it is concurrent, authorized before it is effectful, versioned before it crosses a boundary, and honestly evidenced before it is called verified.

BestBuds should remain the forcing function. If the kernel can make chat membership, message retries, offline reconciliation, actor recovery, cross-runtime envelopes, session cleanup, and safe updates precise under real product pressure, then Reaktor has earned a durable foundation. If it cannot, another layer of abstractions will not compensate.