Reaktor Verified Foundations — Fable 5

Status: public foundation audit and verification program — an independent Claude companion to Reaktor Stable Foundations — 5.6 Ultra and Reaktor Essays — Two Readings Date: 2026-08-27 Branches inspected: workbench-foundation @ 57e83856 (reaktor); bestbuds working tree, same day Author: Claude (Fable 5) Evidence base: four parallel full-repo scans — the kernel modules, the consumer surfaces (BestBuds, GymBuddy, Manna, Nexergy), the entire 84-document corpus including docs/private/, and the distributed cloud plane — followed by direct verification of every citation that carries weight in the defect and security registers. Companion essay: Reaktor Essays — Two Readings

:::warning Publication status This document is public. Sections 6 and 7 name concrete security weaknesses in deployed BestBuds workers with file and line references. Treat the stop-ship set in §7.4 as disclosure-driven release work: verify current status against code, avoid copying credentials or live exploit payloads into follow-up material, and update each finding as it is closed. :::

0. How to read this

The question this document answers is: how do we make Reaktor's base layers very stable, and mathematically verified where that is possible?

The short answer is that verification is the top of a ladder, not a thing you bolt on. Reaktor's kernel is unusually well-suited to formal methods — a binary format, a port graph, an actor runtime, a wire protocol, all small and mostly pure. But today there is no continuous integration at all, no API-stability tooling, and a finite list of concurrency and identity defects in exactly the modules everything else stands on. Proofs layered over that would be decoration. The ladder in §8 climbs in the order that each rung actually kills bugs.

Three conventions are used throughout.

Everything is numbered. Defects are D-n, security findings are S-n, invariants are INV-<MODULE>-n, primitive gaps are P-n, ladder rungs are L0–L5. Tests, specs, and proofs should cite these identifiers directly, so that a proof obligation can be traced back to the defect that motivated it. Appendix A is the traceability matrix.

Every claim carries a citation. Paths are relative to the repository root they belong to, prefixed reaktor/ or bestbuds/. Claims without a citation are judgements, and are marked as such.

Reality wins. Where this document and the code disagree once work starts, the code is right and this document gets updated. This is the same meta-rule the Symphony Plan uses, and for the same reason: a plan that is allowed to be wrong quietly is worse than no plan.

1. The verdict

Reaktor's foundations are small enough to verify and not yet stable enough to be worth verifying. Both halves of that sentence matter.

The kernel is genuinely compact. The things everything else depends on are reaktor-core (a concurrent map, an adapter model, a feature registry), reaktor-graph-port (nodes, ports, edges, wiring, visitors), reaktor-graph (lifecycle, actors, dependency injection, routing), reaktor-flexbuffer (the binary format), and reaktor-ffi (the wire protocol, currently a skeleton). That is a surface a small team can specify completely. Very few frameworks of comparable ambition can say the same, because most accumulate their complexity in the base rather than in the modules above it.

Against that, five findings define the current position.

There is no continuous integration. The only workflow file in the framework repo is reaktor/.github/workflows/documentation.yml, and every line of it is commented out. BestBuds has a real Dagger pipeline but it is workflow_dispatch-only. Nothing runs automatically on any change to either repository.

There is no API-stability tooling and no versioning. No kotlinx-binary-compatibility-validator, no checked-in API dump, zero git tags. The version is generated from the calendar in reaktor/publishing.gradle.kts:4 as "$year.$monthValue.$dayOfMonth-SNAPSHOT". Consumers therefore cannot pin, and a breaking change to a kernel signature is invisible until something fails to compile downstream.

The defect classes that already bit you are still present. The lost-reads-during-resize bug in the hand-rolled ConcurrentHashMap was fixed and regression-tested, but five defects of the same family remain in the same file (D-1 to D-5), the worst of which makes a migrated key permanently unreachable. No model checker or property test guards any of it.

Port type identity is unsound, and in a more interesting way than it first appears. Type is a data class of (type: String, kClass: KClass<*>?) (reaktor/reaktor-graph-port/src/commonMain/kotlin/dev/shibasis/reaktor/portgraph/port/Port.kt:46), and there are two construction paths that do not interoperate. This is D-6, and it is the single most consequential correctness defect in the kernel because wiring is the framework's central claim.

The FFI specification is excellent and the FFI code implements none of it. docs/reaktor-ffi.md pins a seven-slot frame layout, nine verbs, a five-category error model, a seven-row ownership table, a six-function C ABI, and eleven named acceptance tests. The module is twelve Kotlin files in which Transport is four TODO() bodies and the only real C function returns a pointer into a process-global 256-byte buffer. Every polyglot ambition is blocked behind this gap.

The recommendation is a five-rung ladder over roughly two quarters, of which the first three rungs are ordinary engineering and only the last two are formal methods. The single highest-leverage item on the list is turning CI on. The single highest-leverage design change is P-1: one fingerprint system unifying port type identity, codec layout identity, and FFI method identity, which closes D-6, unblocks safe code push, and is the precondition for the graph-kernel proofs in §9.

2. Method and evidence

Four scans ran in parallel, each over a different slice, each instructed to return ground truth with citations and no recommendations. The kernel scan covered reaktor-core, reaktor-graph-port, reaktor-graph, reaktor-flow, compose-flow, reaktor-flexbuffer, reaktor-ffi, reaktor-service, reaktor-compiler, and dependeasy. The consumer scan covered the other nineteen framework modules plus BestBuds, GymBuddy, Manna, and Nexergy. The corpus scan read all 84 documents including the seven in docs/private/. The distributed scan covered the Cloudflare fleet, the JVM server, the databases, and the auth plane.

Findings that carry weight in §4, §5, and §7 were then re-verified by reading the cited lines directly. That second pass changed two conclusions and sharpened one, which is recorded here because it is the kind of thing a reader should be able to audit:

• The subagent report described port type comparison as a plain string compare. Reading connect.kt:15 and Port.kt:46 together shows it is a data-class comparison over (String, KClass?), which produces a different and more interesting defect — two non-interoperating identity regimes rather than one weak one. D-6 reflects the corrected finding.
• The dead-FCM-token retirement mismatch is real but conditional: NotificationRoutes.kt:228 compares against "fcm_error_404" while KotlinNotificationDispatchCoordinator.kt:98 builds the status by joining non-null parts, so the comparison succeeds when FCM returns no reason and fails whenever it returns one. S-3 states the corrected condition.
• The claim that reaktor-graph's dependency cone includes a UI framework was confirmed verbatim at reaktor/reaktor-graph/build.gradle.kts:21-24.

Where a finding could not be verified from source it is marked unverified and the reason is given. The main such case is reaktorServer, whose enforcement code is out of tree — only its Kubernetes manifest exists at bestbuds/cloud/k3s/manifests/app-server.yaml — so claims about the /_graph gateway's runtime behaviour rest on configuration, not on code.

3. The base-layer census

Each base-module assessment separates implementation guarantees from gaps at the source snapshot. Defect identifiers point forward to §4.

3.1 Repository and process state

Thirty modules are registered in reaktor/settings.gradle.kts:59-88, with :reaktor-react commented out at line 56 and reaktor-cli present on disk but unregistered. dependeasy is an included build providing the source-set DSL and the CMake tasks; it has 31 Kotlin files and no tests.

The process facts are the ones that matter most:

reaktor/AGENTS.md:1.3 already states that README.md and LLM_CONTEXT.md are stale and that code should be trusted over both. That honesty is worth preserving; this document inherits the same rule.

3.2 reaktor-core

The module provides the platform-abstraction spine: Adapter<Controller>, which holds a weak reference to a platform controller (framework/Adapter.kt:10-19); Capability, an AutoCloseable marker (capabilities/Capability.kt:5); Feature, a process-global slot registry with integer-keyed slots (framework/Feature.kt:18-47); Dispatch and the Dispatchers.Async expect declaration (framework/Dispatch.kt:14-24); the Platform sealed hierarchy; TruthClass/Fact<T> (truth/Fact.kt:3-49); and the WeakRef/AtomicInt expect declarations (Expectations.kt:3-10).

The centre of gravity is structs/ConcurrentHashMap.kt, 484 lines of lock-free open addressing with a striped size counter, tombstone and redirect sentinels, and incremental migration in sixteen-bucket chunks. The migration fix is in place and regression-tested by jvmTest/.../ConcurrentHashMapMigrationTest.kt:19-52: get no longer stops at a REDIRECT and falls through to nextTable (lines 152-181), and forEach walks both tables deduplicating by key (lines 258-287). Five defects remain in the same file, D-1 through D-5.

Two structural weaknesses deserve naming beyond the defect register. First, AtomicInt is implemented four times by hand — AtomicInteger on JVM and Android, kotlin.concurrent.AtomicInt on Darwin, and a non-atomic field on JS — and Expectations.kt:7 carries the comment that the class is incomplete and atomicfu should be used instead. Second, Adapter, Feature, Fact, Dispatch, and the 208-line PermissionAdapter have no tests at all; the module's only correctness tests are the two for the map.

3.3 reaktor-graph-port

This is the kernel proper, and it is small: twelve source files, one test file, two tests.

PortGraph<Self, N> holds nodes in a ConcurrentHashMap<Uuid, N> with attach implemented as putIfAbsent(...) == null and identity-checked detach (graph/PortGraph.kt:11-47). Port is a sealed base carrying a Key and a Type (port/Port.kt:16-33), specialised into ProviderPort and ConsumerPort. Edge<Contract> binds one consumer to one provider and enforces require(!consumer.isConnected()) in its initialiser (edge/Edge.kt:22). connect rejects type mismatches and double-connections by returning Result.failure (graph/connect.kt:14-23). Visitors and traversers live in visitor/Visitor.kt:12-167.

The explicit invariants are therefore: an edge binds an unconnected consumer; connect refuses mismatched types; and re-registering a provider requires the same implementation instance (ProviderPort.kt:49-51). Everything else is assumed.

The assumption that fails is type identity, D-6. Type is declared at port/Port.kt:46 as:

data class Type(val type: String, val kClass: KClass<*>? = null) {
    companion object {
        fun create(kClass: KClass<*>) = Type(kClass.name(), kClass)
        inline fun<reified T> Type() = create(T::class)
        fun<T: Any> Type(value: T) = create(value::class)
    }
}

and connect compares two Type values with != (graph/connect.kt:15), which for a data class compares both fields. So there are two identity regimes. Ports built from a reified type or a value carry a real KClass and compare nominally by class. Ports built from a string carry null and compare by name alone. The string path is not a corner case: it is used by every service endpoint (reaktor-graph/src/commonMain/kotlin/dev/shibasis/reaktor/graph/ServiceNode.kt:50 and :105 both build Type(...portType)), by the @JsStatic KeyType(key: String, type: String) constructor that all JavaScript callers use (Port.kt:65), and by the string-based Port constructor at Port.kt:25. The consequences are covered in D-6.

The other soft spots: PortCapabilityImpl keeps its port maps in hashMapOf and its listeners in mutableListOf (port/PortCapability.kt:41-43) inside a graph whose node registry is lock-free, so registration is check-then-act and emit iterates a mutable list (D-10); DepthFirstTraverser.traverseRecursive recurses without a depth bound (D-13); and the two-node connect helper calls getOrThrow() mid-sequence, so a failure leaves the graph partially wired (D-11).

3.4 reaktor-graph

Graph composes the port graph with lifecycle, dependency, concurrency, and navigation capabilities (core/Graph.kt:38-200). Its keystones are attach (lines 132-153), detach (155-164), onTransition (173-188), autoWire (211-244), requireFullyWired (250-260), and the non-throwing wiringReport() surface (core/WiringReport.kt:9-49). The node hierarchy is a sealed Node with ActorNode, RouteNode, ContainerNode, ControllerNode, BasicNode, and StateInteractor beneath it.

The lifecycle state machine is the module's most important safety property and it is currently broken (D-8). The code at capabilities/LifecycleCapability.kt:31-40 is:

fun transition(next: Lifecycle) {
    lateinit var previous: Lifecycle
    lifecycle.update { old ->
        previous = old
        if (validTransitions.contains(old to next)) next else old
    }
    if (previous != next)
        onTransition(previous, next)
}

The update correctly refuses an invalid transition by keeping old. The notification then compares previous against next — the requested state, not the state actually reached. So a rejected transition still fires onTransition. In Graph.onTransition the Destroying branch detaches every node (core/Graph.kt:184-186), which means an illegal destroy request tears down the graph anyway.

ActorNode.startLoop guards with a plain field read on a nullable Job (core/node/ActorNode.kt:261-264), so two concurrent lifecycle transitions can start two consumers on one mailbox and break the serialization law the visual-language doc relies on (D-9).

Finally, the dependency cone. reaktor-graph/build.gradle.kts:21-24 declares api dependencies on reaktor-graph-port, reaktor-service, reaktor-ui, and reaktor-db, plus Arrow, and transitively Compose, Ktor, and SQLDelight. The base layer contains a UI toolkit. This is D-25, and it is a precondition for almost everything else in this document: you cannot version, verify, or independently ship a kernel shaped like that.

3.5 reaktor-flexbuffer

The best-covered module in the repository — 77 source files, 21 test files, 123 tests — and the one closest to being provable, because the format is pure data.

The surface is FlexCoder<T> and its registry (core/FlexCoder.kt:24-106), the pooled FlexBufferPool (core/FlexBufferPool.kt:42-88), the kotlinx-serialization encoder and decoder (FlexEncoderV2, FlexDecoderV2), the 1613-line FlexBuffersBuilder, the reader in FlexBuffers.kt, the positional fast path FlexRead, and FlexBufferValidator.isValid(bytes, limit).

The verification story here is already better than anywhere else in the codebase: there is a real differential harness against a C++ oracle in jvmTest/.../FlexBufferHardeningTest.kt (golden and fuzz corpora decoded in both directions, plus corruption rejection), an adversarial performance suite in jvmTest/.../AdversarialPerformanceHarnessTest.kt at 1774 lines, and physical-device verification recorded in reaktor-flexbuffer/PERFORMANCE_VERIFICATION_2026-07-13.md. That harness has already falsified two audit assumptions on real hardware, which is exactly what a good harness is for.

Four gaps keep it from being trustworthy as a storage or cross-deployment format, and the module's own documentation says so — docs/flexbuffer-implementation.md carries a "Stability: experimental" admonition warning against long-lived storage and independently deployed producers and consumers.

First, validation is opt-in and structurally separate from reading. FlexBufferValidator bounds depth at 128, node count at 100,000, and collection size at 1,000,000 (flatbuffers/FlexBufferValidator.kt:206-210), but FlexRead reads the root width and offset straight from the tail of the buffer with no bounds check at all (flatbuffers/FlexRead.kt:31-41), and nothing on the read path calls the validator (D-15).

Second, the alphabetical key-order contract is enforced only by the code generator. FlexCoder.kt:17-19 states that fields must be emitted in alphabetical order; endMapKeyed checks only that the number of pushed values matches the key block, and matches the key block by reference identity (flatbuffers/FlexBuffersBuilder.kt:1117-1123). A coder that emits fields out of order produces a well-formed map with every value bound to the wrong key, and it decodes without error (D-16). The generator does sort, using unsigned UTF-8 comparison (reaktor-compiler/.../FlexCoderProcessor.kt:114-126), and the decoder re-derives the same order (core/FlexDecoderV2.kt:96-115) — so the contract is really "two independently written comparators must agree forever," guarded by two small generator tests.

Third, the decoder's field-index cache is a process-global unsynchronized HashMap keyed by serial name (core/FlexDecoderV2.kt:87), written from any decoding thread and collision-prone across types that share a serial name (D-17).

Fourth, buffer ownership. finish() returns a zero-copy view over the pooled builder's array and finishedBytes() returns the array itself (flatbuffers/FlexBuffersBuilder.kt:161-176), while FlexBufferPool.withEncoder releases the builder in a finally and the next acquire() clears it (core/FlexBufferPool.kt:49-74). Any value that escapes the withEncoder block is a view into a buffer that will be overwritten (D-19). Release itself has no identity check, so a double release places one builder in two slots and hands the same mutable builder to two encoders (D-18).

3.6 reaktor-ffi

Twelve Kotlin files. Invokable/SyncInvokable/AsyncInvokable; a global object Switch whose module table is a plain hashMapOf (switch/Switch.kt:9-39); a positional FlexPayload whose argument accessor is TODO() (payload/FlexPayload.kt:49); and a ByteBufferTransport whose four methods are all TODO() (transport/Transport.kt:36-49). On the native side, cpp/common/HermesHello.cpp:7-9 evaluates JavaScript in a fresh Hermes runtime and returns a pointer into a static char hermesResultBuffer[256], which Kotlin/Native reads through toKString() at src/iosMain/.../NativeBridge.ios.kt:7.

Set that against docs/reaktor-ffi.md, which specifies: a seven-slot frame (protocol: u8, verb: u8, callId: u32, targetId: u16, methodId: u16, payload: blob, meta: map?); nine verbs (HELLO, DESCRIBE, CALL, RESULT, ERROR, EMIT, COMPLETE, CANCEL, CREDIT); a five-category error model; credit-based backpressure with three overflow policies; a seven-row ownership table with reaktor_release(handle) as the single disposal path; a six-function C ABI; per-trunk copy budgets; and eleven named acceptance tests.

None of it exists in code. Grepping the module for reaktor_abi_version, reaktor_attach, reaktor_send, reaktor_invoke, or reaktor_release returns nothing; CREDIT and credit appear zero times. The spec is one of the best documents in the corpus and the module is a skeleton, and the module's own README still documents the superseded four-field envelope while claiming production use.

Three things in the spec are also genuinely undefined and need to be pinned before implementation: the cell and wire lifecycle state machines exist only as prose, so there is no transition table to implement or check; the fingerprint algorithm — the thing the entire safe-code-push story rests on — is named but never specified; and the credit unit (items versus bytes) is listed as an open question. §9.3 and §12 address all three.

3.7 reaktor-service and reaktor-compiler

Service provides server() and client() factories over per-verb handlers held in arrayListOf (reaktor-service/.../Service.kt:18-112). Both factories capture a lateinit var created inside the closure they pass to the factory, so a factory that invokes its block eagerly throws UninitializedPropertyAccessException (D-23).

reaktor-compiler is the KSP layer and, through FlexCoderProcessor.kt (1124 lines), the sole authority for the flexbuffer key-order contract. Its two small tests are the only guard on that contract. The C++ and TypeScript code generators are four-line stubs; only the Kotlin generator is real. A stale duplicate source tree exists under reaktor-compiler/bin/main/ and should be deleted.

3.8 How consumers are coupled

BestBuds is the only substantial consumer, and the coupling has three shapes worth knowing before changing anything in the kernel.

Global feature slots. Twenty-five adapters are published through Feature slots whose integer identifiers are assigned by an incrementing counter at class-initialisation time (reaktor-core/.../framework/Feature.kt:42). Two modules whose top-level slot properties initialise in a different order on a different platform get different identifiers, and nothing detects it (D-24). Every slot returns T? and a type mismatch surfaces as a runtime ClassCastException, not a compile error.

A hardcoded substitution list. bestbuds/settings.gradle.kts:81-105 names twenty modules for dependency substitution, each twice for the legacy and current group identifiers. It currently matches the set of externally-named coordinates exactly. It works only because reaktor-core, reaktor-io, and reaktor-graph-port are never named as external coordinates despite reaktor-graph-port accounting for 126 imports in BestBuds. Adding one new external coordinate without editing this file sends the build to a GitHub Packages fetch of a snapshot that does not exist locally.

Enum names as wire contract. bestbuds/modules/app/.../services/NotificationService.kt:206-270 builds registration payloads from Kotlin enum constant names — "auth:${it.name}", platform.name.lowercase(), permission.state.name.lowercase(). Renaming a constant in reaktor-notification or reaktor-core compiles cleanly and silently changes the contract against a deployed worker.

Graceful degradation is used well in about nine places and bypassed in four. Good examples: the chat composer logs and returns when Feature.Gallery is absent (ChatComposer.kt:390-393), and service support falls back through database, auth headers, stored token, and finally an empty map (BestBudsServiceSupport.kt:14-29). Bypasses: UserRepository.kt:44 throws NotImplementedError at construction if auth is missing, and BestBuds.kt:126 binds the key-value store through by lazy over a throwing elvis, so the first reader binds the failure forever.

3.9 What a green build proves today

BestBuds' dagger call pr runs four jobs (bestbuds/.dagger/src/index.ts:359-375): :reaktor-core:jvmTest :reaktor-graph:jvmTest :reaktor-performance:jvmTest; :app:compileKotlinJvm :app:jvmTest :design:jvmTest :engine:jvmTest; :app:jsTest; and an architecture job that runs two named test classes.

So a green build proves that three framework modules' JVM tests pass, that the application modules compile and their JVM and JS unit tests pass, and that roughly fifteen source-text conventions hold. It proves nothing about iOS, Android, or desktop; nothing about the deployed worker fleet; nothing about the twelve framework modules with no tests that BestBuds links against; and nothing about the 105 Maestro flows, whose last recorded run was 2026-07-13 and ended 24 passed, 6 failed.

The architecture tests deserve a specific caution. AppArchitectureVitalsTest reads source files from disk and asserts on substrings — that a file contains KV.state<User>("user"), that a directory contains exactly two named files, that a build file contains a compiler flag. These enforce conventions, not behaviour. They will fail on harmless refactors and pass through real regressions. They are useful as lint and should not be counted as verification.

4. The defect register

Severity is judged by blast radius and silence: a defect that corrupts data quietly outranks one that throws.

4.1 The critical set in detail

D-1 — migration probe-bound asymmetry. insertDuringMigration probes while (probes <= t.capacity) (reaktor-core/.../structs/ConcurrentHashMap.kt:427), while get and putInternal stop at t.maxProbe, which is max(2·log2(capacity), 16) (lines 161 and 314). A key migrated into a slot further than maxProbe from its home position is written successfully and can never be read again. It survives forEach (which scans buckets) but is invisible to get, so the map reports data it will not return. Fix: give migration the same probe bound and trigger a further resize when it is exceeded.

D-2 — clear() bypasses migration. clear() reads the current table and stores a fresh one (ConcurrentHashMap.kt:466-470) with no REDIRECT protocol. A writer that captured the old table publishes into an orphan, and the write vanishes silently. Fix: implement clear as a migration to an empty table, or take the resize path.

D-6 — dual type identity. Because Type is data class Type(val type: String, val kClass: KClass<*>? = null) and connect compares with != (graph/connect.kt:15), two failure modes exist at once:

• False negative. A consumer registered from a reified type carries Type("Config", Config::class). A provider registered by a ServiceNode carries Type("Config", null) (reaktor-graph/.../ServiceNode.kt:50). They name the same contract and refuse to connect. Every service endpoint port and every JavaScript-registered port sits on the null side.
• False positive. Two different classes both named Config, both registered through the string path, compare equal and wire successfully. The unchecked cast at Graph.kt:236 then turns the mismatch into a ClassCastException at first invocation, far from the wiring site.

Fix: P-1, a single content-derived fingerprint used as the sole identity, with the string path either removed or required to carry a fingerprint.

D-8 — rejected transitions fire effects. Described in §3.4. Fix is two lines: compare against the state actually reached, not the state requested.

fun transition(next: Lifecycle) {
    lateinit var previous: Lifecycle
    lateinit var reached: Lifecycle
    lifecycle.update { old ->
        previous = old
        reached = if (validTransitions.contains(old to next)) next else old
        reached
    }
    if (previous != reached) onTransition(previous, reached)
}

D-15 and D-16 — the format's two silent-corruption paths. Together these mean an attacker-supplied or merely stale buffer can read out of bounds, and a mis-ordered coder can bind every value to the wrong key without any error. These are the two defects that most justify the Lean work in §9.1, because both are properties of a pure function over bytes and therefore genuinely provable.

D-20 and D-21 — the FFI trust boundary. Switch.fetchModule takes bytes off the wire and calls getRoot and positional field reads with no isValid gate (switch/Switch.kt:25, payload/FlexPayload.kt:28-32), and the C entry point returns a pointer into a shared static buffer that two concurrent callers race on. Neither is exploitable in production today because the module is not deployed, which is precisely why both must be fixed before it is.

5. The invariant catalogue

This is the artifact the verification program targets. Each invariant is written so that it can be a test name, a model-checked property, and eventually a theorem statement. The intent is that each module gains a normative SPEC.md containing its section of this catalogue, and that every test cites the invariant it defends.

5.1 Concurrent map — INV-CHM

1. Read-your-write. If put(k, v) returns and no later put or remove for k happens, then get(k) == v, for any interleaving and across any number of resizes.
2. No lost keys under migration. For every key present before a resize begins and not removed during it, get returns its value after the resize completes.
3. Probe-bound agreement. Every write path uses a probe bound no greater than the bound used by every read path.
4. Size accuracy. size equals the number of keys for which get returns non-null, once quiescent.
5. Termination. Every operation completes in a finite number of steps for any key distribution, including adversarial hash collisions.
6. Clear atomicity. After clear() returns, no key written before the call is observable, and no key written after it is lost.

Invariants 1, 2, and 3 are what D-1 violates; 4 is what D-3 weakens; 5 is what D-4 violates; 6 is what D-2 violates. All six are directly expressible as lincheck operations (L2).

5.2 Port graph — INV-PORT

1. Identity soundness. Two ports have equal types if and only if they denote the same contract. Equality is transitive, symmetric, and stable across platforms, processes, and serialisation round trips.
2. Wire safety. If connect(c, p) succeeds, every value p produces is assignable to c's contract — that is, no successful connection can produce a ClassCastException at invocation.
3. Consumer exclusivity. A consumer port participates in at most one edge at any time.
4. Wiring atomicity. A wiring operation either connects every pair it names or leaves the graph exactly as it found it.
5. Registry consistency. Concurrent registration and emission never lose a port, never deliver a port event twice, and never throw from concurrent modification.
6. Traversal totality. Every traversal terminates on every finite graph, including cyclic ones, within bounded stack.

Invariant 1 is D-6; 2 follows from 1; 4 is D-11; 5 is D-10; 6 is D-13.

5.3 Graph runtime — INV-GRAPH

1. Lifecycle soundness. A node only ever occupies states reachable by the transition relation, and effects fire only for transitions that were accepted.
2. Actor serialization. At most one consumer processes a given mailbox at any time, and messages from one sender are processed in send order.
3. Attach uniqueness. No two live nodes in one graph share an identifier.
4. Detach completeness. After detach(n), no edge references n's ports and n receives no further events.
5. Wiring report honesty. wiringReport() lists exactly the consumers requireFullyWired would reject.
6. Rewire quiescence. A hot rewire of a subgraph does not drop, duplicate, or reorder in-flight messages on wires it does not replace.

Invariant 1 is D-8; 2 is D-9; 6 is unbuilt and is the property the code-push story depends on.

5.4 FlexBuffers — INV-FLEX

1. Validator soundness. If isValid(b, n) holds, then no accessor path over b reads outside [0, n).
2. Round-trip. For every encodable value v, decode(encode(v)) == v.
3. Key binding. For every map produced by a conforming coder, get(key) returns the value the encoder pushed for key.
4. Order independence at the API. The value of a map does not depend on the order in which its fields were pushed — either because order is enforced at write time or because binding is checked.
5. Canonical form. For each value there is exactly one canonical encoding, and canonical encodings compare equal byte-for-byte.
6. Cross-implementation agreement. Kotlin, C++, TypeScript, and Native implementations produce identical bytes for identical inputs and identical values for identical bytes.
7. Ownership. A buffer returned to a caller remains valid until the caller releases it; a pooled builder is owned by at most one encoder at a time.
8. Bounded resources. Decoding a buffer of size n uses memory and time bounded by a stated function of n, for all inputs including adversarial ones.

Invariant 1 is D-15; 3 and 4 are D-16; 7 is D-18 and D-19. Invariants 1, 2, 3, 5, and 8 are provable in Lean (§9.1); 6 is enforced by generated conformance vectors.

5.5 FFI wire — INV-FFI

1. Frame well-formedness. Any byte sequence either parses to a valid frame or is rejected; parsing never reads out of bounds.
2. Call-response matching. Every RESULT, ERROR, or EMIT carries the callId of an open call, and no callId is reused while open.
3. Stream termination. Every opened wire eventually reaches exactly one terminal state — COMPLETE, ERROR, or CANCEL — and emits nothing after it.
4. Credit safety. A sender never has more unacknowledged items in flight than the credit it has been granted.
5. No head-of-line blocking. A slow wire cannot prevent progress on another wire sharing a trunk.
6. Fingerprint gating. Positional decoding runs only when both sides have exchanged matching fingerprints; a mismatch degrades to keyed decoding or errors, and never misreads bytes.
7. Ownership. Every buffer has exactly one release, and no access occurs after it.
8. Thread affinity. A cell's handler runs only on its switch's scheduler; no user code runs on a transport thread.

These are transcribed from docs/reaktor-ffi.md §5–§8, which states them as prose guarantees. Invariants 2, 3, 4, and 5 are what L3 model-checks; 6 is what P-1 enables; 1 is what D-20 violates.

6. The distributed plane

Reaktor's stability claim cannot stop at the kernel, because the product's real failure modes are distributed. This section records the protocols that exist implicitly today. §7 records what is wrong with them.

A structural fact first: there are no Cloudflare Queues anywhere in the fleet. No queues block appears in any of the twenty-one wrangler configurations, and no MessageBatch or queue() handler exists. Every pipeline that reads as asynchronous is either a synchronous fetch or a fire-and-forget waitUntil. This matters because the docs describe queue-based delivery semantics that no code implements.

6.1 Protocol register

PR-1 — message send, moderation, notification. Client to messaging worker to moderator to chat Durable Object, with a parallel path to the notification worker. The order as written (bestbuds/modules/app/src/jsMain/.../messaging/MessagingWorker.kt:169-207) is: insert the message, compute recipients, fire text moderation, fire notification — all three inside the enclosing Postgres block, with the two fires dispatched through GlobalScope.promise and ctx.waitUntil. There is no retry, no dead-letter, and no outbox. The moderator later issues UPDATE messages SET moderation_status ... on a different connection (moderation/ModerationRepository.kt:64-68).

PR-2 — notification fan-out. POST /internal/dispatch (notification/NotificationRoutes.kt:183-225): authenticate the calling worker, then for each recipient check category, read up to eight enabled endpoints, create a delivery row with status queued, call the dispatch gateway, update status, and conditionally disable the endpoint. Sequential, unbatched, with no transaction spanning the D1 writes and the Durable Object call, and no cursor to resume from.

PR-3 — dispatch leg. One Durable Object per endpoint (notification/NotificationDispatchGateway.kt:20), which decodes the payload, dispatches to FCM, and writes a last-dispatch snapshot. The deliveryId travels in the payload and is never read.

PR-4 — realtime token exchange. An RFC 8693 token exchange producing a delegated token scoped to realtime:connect with the room identifier as context (chat/ChatService.kt:146-193), verified on connect at lines 429-452.

PR-5 — service-account credentials. A module-level cache in worker isolate memory (reaktor-cloudflare/.../ServiceAuth.kt:66-109) with no in-flight deduplication, so N concurrent misses produce N token requests.

PR-6 — JWKS distribution. KV-cached with a one-hour TTL and a single forced refresh on key-identifier miss (WorkerJwtVerifier.kt:37-93), with no stale-cache fallback if the refresh itself fails, and a "if exactly one key is published, use it" fallback at lines 150-162.

PR-7 — cron backup and purge. Both build a synthetic request and route it through a second, unauthenticated worker instance (archiver/ArchiverWorker.kt:283).

6.2 Authority map

6.3 Ad-hoc protocol reimplementations

Four known patterns appear in improvised form. A lease appears as an unlocked check-then-act in the campaign bot, which reads the last action time, compares against a twelve-hour cooldown, posts, and only then records (campaign/CampaignEngagementWorker.kt:37-42, 160, 169) — concurrent or retried runs both pass the check, and a failure after posting means the cooldown never advances. An outbox appears as waitUntil. A saga appears as post-hoc redaction: the message is delivered and pushed first, and the moderator later flips status and broadcasts an update, with no compensation for the push already sent. An idempotent consumer appears as the unread last-dispatch record.

One pattern is implemented correctly and is worth copying: the account purge snapshots its target set into CREATE TEMP TABLE _purge ON COMMIT DROP before acting, and requires a two-phase confirmation parameter (purge/AccountPurgeWorker.kt:22, 31-37).

7. The security stop-ship set

These are application defects rather than framework defects, but they are live, and no verification program should be started while they are open. They are ordered by exploitability.

S-1 — any authenticated user can join any chat room. chat/ChatService.kt:146-193 mints a socket token for a room after authenticating the caller and checking only the token's shape. isChatMember exists at social/SocialWorkerRepository.kt:231 and is called from exactly two places — MessagingWorker.kt:158 and :251 — neither of which is the token mint or the connect path. The result is read access to every room's live traffic: messages, presence, typing, reactions. Fix: call isChatMember before minting, and re-check on connect.

S-2 — notification endpoint takeover. upsertEndpoint derives the row identifier from sha256(provider:platform:token) and, on conflict, sets user_id = excluded.user_id (notification/NotificationRepository.kt:19-34). Registering another user's device token reassigns their endpoint to the attacker. Fix: on conflict, keep the existing owner and reject the mismatch.

S-3 — dead tokens are never retired. NotificationRoutes.kt:228 compares the delivery status against the literal "fcm_error_404", while KotlinNotificationDispatchCoordinator.kt:98 builds the status as listOfNotNull("fcm_error", httpStatus.toString(), reason).joinToString("_"). Whenever FCM supplies a reason — which is the normal case for an unregistered token — the status becomes fcm_error_404_unregistered and the comparison fails. Dead endpoints accumulate against the eight-endpoint fan-out cap and eventually crowd out live devices. Fix: compare structurally on the parsed status and reason, not on the joined string, and add a test for both shapes.

S-4 — no idempotency in the notification path. The Durable Object ignores deliveryId; createDelivery mints a fresh identifier per attempt; D1 has no unique constraint over the natural key. Any retry of /internal/dispatch re-sends every push and writes duplicate rows.

S-5 — moderation verdict races the insert. The moderation call is fired inside the transaction block that inserts the message, and the verdict update runs on a different connection. If it lands before commit it updates zero rows and the verdict is lost silently.

S-6 — moderation fails open, with a weak cache key. moderation/TextModeratorWorker.kt:32-39 returns ALLOW when the classifier errors, so a Workers AI outage permits all text. Separately, verdicts are cached for seven days under a djb2 hash of the normalised text (moderation/ModerationCache.kt:30-42), a non-cryptographic key that can be collided deliberately to serve one message's verdict for another.

S-7 — two write paths skip membership. toggleReaction (MessagingWorker.kt:217-239) has no membership check, and sendBotMessage (lines 263-285) accepts any authenticated user without checking the chat identifier.

S-8 — an unauthenticated route triggers outbound publishes. /pubsub/hello/push/server-to-worker (notification/NotificationRoutes.kt:55-60) performs no authentication and causes the worker to publish to Google Pub/Sub using its service account.

S-9 — a header-based identity bypass. X-BestBuds-Dev-User is honoured whenever the ALLOW_USER_HEADER_AUTH secret is "true" (core/BestBudsRequest.kt:84, 100-101, 163-165). The control is a single environment value away from full impersonation in any environment where it is set.

S-10 — backups are unreliable in three ways. Change detection is a concatenation of per-table row counts (archiver/ArchiverWorker.kt:187-196), so any update-only day, or a day with equal inserts and deletes, is treated as unchanged and skipped. The dump itself is a sequence of per-table selects with no snapshot transaction, so backups are torn across tables. And the restore path toggles session_replication_role without a guaranteed unwind, so a mid-restore termination can leave foreign-key enforcement disabled on a pooled connection for unrelated requests.

S-11 — a database exposure from the July review. The details are tracked privately until it is closed.

S-12 — the graph gateway's guard. The details are tracked privately until it is confirmed and hardened.

8. The verification ladder

Six rungs. Each kills a class of defect the rung below cannot, and each is only worth climbing once the one beneath it holds. Effort figures assume one engineer with agent assistance, which is the actual working configuration.

L0 — Hygiene

Goal: make change visible and the kernel shippable. Effort: one to two weeks.

Turn CI on. BestBuds' Dagger pipeline already exists and works; it needs push and pull-request triggers, and the framework repo needs an equivalent that builds every module and runs every test that exists. Add kotlinx-binary-compatibility-validator to the kernel modules with checked-in API dumps, so that every public signature change appears as a reviewable diff. Start tagging releases and publish real artifacts, so useSourceBuild in bestbuds/modules/app/build.gradle.kts:24 stops being a hardcoded true with a dead alternative branch.

Then fix D-25 by extracting reaktor-graph-core: nodes, ports, edges, wiring, lifecycle, visitors, and nothing else — no Compose, no Ktor, no SQLDelight, no Koin. The existing reaktor-graph becomes a thin module that adds the UI and persistence integrations on top. This is a prerequisite for every later rung, because you cannot version, verify, or independently ship a kernel that transitively contains a UI toolkit.

Exit: CI runs on every push in both repositories; a red build blocks merge; apiDump is committed for every kernel module; a tagged release exists and BestBuds can build against it; reaktor-graph-core compiles with a dependency cone containing only Kotlin standard library, coroutines, and atomicfu.

L1 — Written invariants and defect burn-down

Goal: say what the base layers promise, then make them keep those promises. Effort: three to four weeks, parallel with L2.

Each kernel module gains a normative SPEC.md containing its section of the catalogue in §5, with each invariant numbered and each accompanied by the failure it prevents. This is cheaper than it sounds, because docs/reaktor-visual-language.md §7.5–7.7 and docs/reaktor-ffi.md §5–§8 already contain most of the content in semi-formal form; the work is consolidation and numbering, not invention.

In the same pass, close the defect register: D-1 through D-5 in the map, D-6 and D-7 through the fingerprint work in §12, D-8 through D-14 in the graph layers, D-15 through D-19 in flexbuffer, and D-20 through D-22 before any FFI implementation begins.

Exit: every kernel module has a SPEC.md; every invariant has at least one test citing it by identifier; every Critical and High defect is closed or has an accepted written waiver.

L2 — Mechanized testing

Goal: find the bugs review cannot. Effort: three to four weeks, parallel with L1.

Three tools, each matched to a defect class this codebase has actually shipped.

Lincheck for every concurrent structure — the map, the pools, the port registry, the actor mailbox. Lincheck generates concurrent scenarios and checks them against a sequential specification, exploring interleavings systematically. It would have found the original migration bug mechanically, and it directly encodes INV-CHM-1 through INV-CHM-6. This is the highest-value single tool addition in the entire program.

Property-based tests for the pure layers: round-trip and key-binding properties for flexbuffer (INV-FLEX-2, INV-FLEX-3), mutation properties (any single-byte change either fails validation or decodes differently), and graph properties (wiring preserves well-formedness; traversal visits each node once).

Differential conformance as a required gate. The oracle harness already exists at reaktor-flexbuffer/src/jvmTest/.../FlexBufferHardeningTest.kt, but it silently degrades when the C++ binary is absent. Make its absence a failure, and extend the matrix to JS and Native targets. Until Lean vectors exist (L4), this is what "verified" means at the cross-language boundary: one specification, several implementations, machine-checked agreement.

Exit: lincheck suites green for the map, both pools, and the port registry; property suites green for flexbuffer and the graph kernel; the differential harness runs in CI on four targets and fails when an implementation is missing.

L3 — Model-checked protocols

Goal: get the distributed behaviour right before optimising it. Effort: one quarter, interleaved.

For distributed protocols, model checking beats theorem proving on cost by a wide margin. Write specifications in TLA+ — or Quint, which is the same underlying mathematics with far better ergonomics and a shorter path from specification to test generation — for five small protocols:

1. Notification dispatch (PR-2, PR-3): properties are at-least-once delivery, no duplicate user-visible push after deduplication, and eventual consistency of delivery status. This closes S-4 by construction.
2. Moderation saga (PR-1): the verdict is never lost, and a message never remains visible after a block verdict commits. This closes S-5.
3. Snapshot sync, before it is built: properties are that a restore is atomic, that version numbers advance monotonically, that the auth store is never overwritten, and that concurrent writers converge.
4. Hot rewire, INV-GRAPH-6: pause, drain, swap, resume, with no message dropped, duplicated, or reordered.
5. FFI wire lifecycle, INV-FFI-2 through INV-FFI-5: this is the one that pays back immediately, because the specification's biggest gap is that cell and wire states exist only as prose. Model the state machine, check cancellation racing completion, credit exhaustion, and trunk failure — and the checked state machine becomes the implementation's skeleton rather than a document about it.

Exit: five specifications checked at useful bounds; each has produced at least one counterexample that changed the design or the code; each protocol's implementation cites its specification.

L4 — Lean 4 proofs

Goal: eliminate whole classes of error permanently, where the subject matter makes that affordable. Effort: one quarter for the first two targets. Covered in detail in §9.

L5 — Deterministic simulation

Goal: test the whole system as one deterministic object. Effort: four to six weeks, after L0 and L3.

This is the capstone, and Reaktor is unusually well positioned for it. All input and output already flows through adapters; the system's structure is already data; kotlinx-coroutines-test already provides a virtual-time scheduler. Put those together and an entire multi-runtime product — app, workers, server, databases — runs inside one process on virtual time, with a seeded random source driving message reordering, delays, partitions, crashes, and restarts.

This is the technique behind FoundationDB's reliability and TigerBeetle's. It converts every protocol in L3 from "checked in a model" to "hammered in the real implementation," and it makes failures reproducible from a seed rather than a story. No other application framework can offer it as an architectural property, because no other framework holds the whole system as a live graph.

Exit: a nightly run executes millions of randomized schedules; a failing seed reproduces exactly; at least one real defect has been found and fixed this way.

9. What to prove, and in what

Honest framing first, because this is where framework documents usually overclaim. There is no Lean-to-Kotlin verification toolchain, and none is coming. You will never prove the Kotlin code directly. What works, and what serious systems actually do, is a verified reference with a conformance binding: write an executable specification in Lean, prove its properties, extract test vectors from it, and require every language implementation to pass those vectors. The proof covers the design; the vectors cover the implementations; the gap between them is visible and bounded rather than hidden.

Targets, in order of value per unit of effort.

9.1 FlexBuffers — the first target

The right first target for four reasons: it is pure, it is self-contained, it is the data plane every other subsystem depends on, and it already has an oracle and a corpus to check against.

Deep-embed the format in Lean: a Buffer as a byte array, a Value inductive type, an encoder, a decoder, and the validator. Then prove, in roughly this order:

• Validator soundness (INV-FLEX-1): if isValid b n then every accessor path stays within bounds. This is the theorem that turns D-15 from a hazard into a checked precondition, and it is the single most valuable proof in the program because it converts a memory-safety property of a parser into a fact.
• Round-trip (INV-FLEX-2): decode (encode v) = some v for all v.
• Key binding (INV-FLEX-3): for a map built by a conforming coder, lookup returns the value pushed for that key — which formalises exactly the ordering contract D-16 currently leaves to two independently written comparators.
• Canonical form (INV-FLEX-5): a normalisation function with a proof that two values are equal if and only if their canonical encodings are byte-identical. This has an immediate practical payoff beyond correctness: content addressing, deduplication, and cache keys become sound.
• Bounded decoding (INV-FLEX-8): decoding uses time and memory bounded by input size, for all inputs.

Then extract vectors. The Lean specification generates a corpus — valid buffers with expected decodings, invalid buffers with expected rejections, canonical-form pairs — and that corpus becomes a required CI gate for Kotlin, C++, TypeScript, and Native. That is what makes the phrase "mathematically verified base layer" defensible: not that the Kotlin is proved, but that the format is proved and every implementation is machine-checked against the proof.

9.2 The visual language semantics — the cheapest target

docs/reaktor-visual-language.md §7.6 already contains a small-step operational semantics: configurations ⟨n, σ, κ, μ⟩, nine reduction rules, four data-evaluation judgments, and a determinism argument written in prose — "each rule selects a unique successor, the pure sub-graph is acyclic, and ops are deterministic." §7.5 adds typing judgments with three inference rules and a subtyping relation.

Transcribing this into Lean and machine-checking determinism and type preservation is unusually cheap, because the hard intellectual work is already done. The payoff is disproportionate: it turns the prose argument into a theorem, and it would make Reaktor one of very few industrial frameworks with a mechanized semantics for its programming surface. Every downstream claim that depends on determinism — replay, snapshot diffing, shadow testing, agent reproducibility — then rests on a proof instead of an argument.

9.3 The port-graph kernel

Model the graph as a finite structure with typed ports, and prove that connect, disconnect, attach, and detach preserve well-formedness — INV-PORT-2 through INV-PORT-4, and INV-GRAPH-1 and INV-GRAPH-3. Prove autoWire correct: it terminates, and it produces a fully wired graph or reports precisely the consumers it could not satisfy.

This requires D-6 fixed first, because you cannot state INV-PORT-1 about a type system with two disagreeing equality regimes. That dependency is why P-1 sits at the top of §11.

9.4 Kahn-network determinism

Prove once, over an abstract model, that a network of deterministic nodes communicating over unbounded FIFO channels with blocking reads computes a function of its inputs independent of scheduling. This is Kahn's classical result; mechanizing it is a known exercise.

The interesting part is not the proof but what it forces on the API. The theorem's hypotheses are exactly the conditions Reaktor must enforce: node functions must be deterministic, reads must block rather than poll, and channels must be point-to-point. Enforce those in the type system, and make every source of nondeterminism — merge, race, timeout, wall-clock time — an explicit node type that a checker can find. Then determinism becomes a property you can decide by inspecting the graph, which is precisely what makes L5's replay trustworthy.

9.5 Choreography — research-grade, later

Worth stating carefully, because the corpus currently contains a contradiction. docs/reaktor-server.md:408 explicitly rejects choreography in favour of orchestration modelled as a saga graph executed by a visitor. That is the right call for failure handling and compensation, and nothing here changes it.

But "choreographic programming" names two different things, and only one of them was rejected. The rejected one is the execution model. The other is session types: a global protocol description from which endpoint behaviour is projected, with deadlock-freedom and protocol conformance guaranteed by typing. That one is complementary, and Reaktor already has the hard prerequisite — the flow graph is a global viewpoint, which is exactly what endpoint projection needs as input. Existing mechanizations (Pirouette in Coq, and the Chorλ line of work) are portable to Lean, and a Lean development of multiparty session types projected onto Reaktor wires would be a genuine research contribution, plausibly with an academic collaborator.

Sequence it after L4's first two targets. Adopt session-typed wire contracts as a practical measure well before then, since docs/reaktor-ffi.md already declares four wire shapes — unary, server-stream, client-stream, bidirectional — that are one step away from being types rather than declarations.

9.6 Smaller targets worth doing opportunistically

The capability tier lattice from docs/reaktor-capability.md is a five-element order; proving that degradation is monotone (a capability never degrades into a higher tier, and composition takes the meet) is an afternoon's work and makes the graceful-degradation story exact. The heimdall RBAC model is a natural fit for Alloy rather than Lean: bounded, relational, and best explored by counterexample.

10. Theoretical models: what exists and where it can go

The pattern is that Reaktor's theory is consistently one step short of formal: the right models are named, the right structure is described, and the final step to a checkable artifact has not been taken. That is a good position to be in. It means the L4 work is transcription and mechanization rather than research, for everything except §9.5.

11. Increasing Reaktor's power

Applying the framework's own selection test — does this expand the space of systems Reaktor can express, rather than adding a vector already spanned?

P-1 — one fingerprint system. Covered in §12. Ranked first because it is simultaneously a correctness fix (D-6), a security precondition (safe code push), and a proof precondition (§9.3).

P-2 — ship the FFI frame protocol. Not new design; the specification exists and is good. Every polyglot ambition — C++ in tight loops, TypeScript code push, Python, remote trunks, Flutter and React Native embedding — is blocked behind twelve skeleton files. This is the highest-leverage build in the codebase, as distinct from the highest-leverage change.

P-3 — a durable journal and outbox primitive. The distributed scan's verdict is unanimous: every pipeline is fire-and-forget, there are no queues, and the docs mark event sourcing absent. One primitive — an append-only log with idempotency keys, plus a visitor that drains it — retires S-4 and S-5, fixes the campaign lease, and becomes the substrate for actor persistence, sync, and CQRS. Note that ObjectStore's DatabaseEvent stream is change-tracking, not a log; the docs say so explicitly.

P-4 — deterministic time. A clock and scheduler adapter that every node uses, virtualizable for L5 and for replay. Cheap now, nearly impossible to retrofit once a hundred modules call system time directly.

P-5 — capability-secured visitors. The agentic story needs this to be real rather than aspirational. SecuredProviderPort and SecuredConsumerPort exist, but auth-analysis.md:2003 records that enforcement is manual. Make visitor authority an unforgeable object capability — a visitor carries a scope naming what it may read and rewire — and "agents operating on the graph" becomes safe by construction. This is also the honest differentiator against MCP: a doorway versus a floor plan with locks.

P-6 — a graph query language. Visitors are imperative, and the three consumers that matter — tooling, telemetry attachment, and agents — all want declarative selection. A small Datalog or Cypher subset over the live graph, sharing a surface with Memgraph so that live and persisted graphs are queried the same way.

P-7 — effectively-once as a service primitive. The docs state the target precisely and no code implements deduplication. Put idempotency keys into reaktor-service requests natively and every worker inherits the behaviour.

P-8 — Python as a trunk. The stated blocker is hard Kotlin-to-Python interop, and the Switchboard design already dissolves it: a Python cell is an out-of-process trunk over a Unix socket or shared memory carrying FlexBuffer frames, with the Flow port on top. Ship that, and treat in-process GraalPy on JVM targets as a later optimisation. The breakthrough being waited for is the specification already written.

P-9 — a WebAssembly component-model trunk. Cheap optionality: sandboxed code push for non-UI logic and interoperation with the WASI ecosystem, without displacing Hermes for UI.

P-10 — supervision trees. LLM_CONTEXT.md still records ActorNode as incomplete, and D-9 shows why. Erlang-style restart policies expressed as graph structure — a supervisor is a node, a policy is data — completes the actor primitive and gives graceful degradation its runtime half to match the design-time half in reaktor-capability.md.

12. The keystone: one fingerprint system

Three identity mechanisms exist today, all weak or unbuilt, and they should be one.

Port type identity is (simpleName, KClass?) with two non-interoperating regimes (D-6). Codec layout identity is documented as a fingerprint in docs/flexbuffer-implementation.md and is unimplemented, which is precisely why that document warns against independently deployed producers and consumers. FFI method identity is specified as "a stable hash of the normalized signature" in docs/reaktor-ffi.md with the hash and the normalisation rules both left undefined.

These are the same problem three times: given a name on one side of a boundary and a name on the other, do they denote the same thing?

Define one answer. A fingerprint is a content-derived digest of a normalised structural description — for a type, its fully-qualified name plus the fingerprints of its fields in canonical order; for a method, its name plus parameter and return fingerprints plus its wire shape. Compute it in the KSP processor at build time, where the type information is fully available. Then use the same value everywhere:

• Ports compare fingerprints. D-6 and D-7 disappear, because identity no longer depends on which construction path built the port or on whether a KClass survived a serialisation round trip. INV-PORT-1 becomes statable, which unblocks §9.3.
• Codecs exchange fingerprints. Matching fingerprints permit the fast positional path; a known-older fingerprint falls back to keyed decoding; an unknown one is an error. That is exactly the gate docs/reaktor-ffi.md §6 promises, and it is what makes a stale code-pushed bundle degrade safely rather than misread bytes.
• FFI methods use fingerprints as methodId in the HELLO handshake, so INV-FFI-6 holds by construction.
• Graph documents persist fingerprints instead of simple names, so a document saved by one version wires correctly or fails loudly under another.
• Content addressing comes free: with INV-FLEX-5's canonical form, a fingerprint plus canonical bytes is a stable content hash, which gives caching, deduplication, and change detection across the whole system.

One primitive, six payoffs, and it is a precondition for two of the four proof targets. That is what a well-chosen basis vector looks like.

13. Sequencing

Six phases with binary exit criteria, following the Symphony Plan's convention that a gate either holds or does not.

Phase 0 — Containment (week 1). Close S-1, S-2, S-3, S-7, S-8, S-9; confirm or fix S-12; schedule S-11. Exit: no unauthenticated route mutates state or triggers outbound publishes; membership is enforced on every chat read and write path; a test covers both dead-token status shapes.

Phase 1 — Hygiene (weeks 1–3). L0 in full. Exit: CI on every push in both repositories; committed API dumps; a tagged release BestBuds builds against; reaktor-graph-core extracted with a clean dependency cone.

Phase 2 — Invariants and burn-down (weeks 3–8). L1 and L2 together, plus P-1. Exit: every kernel module has a SPEC.md; every Critical and High defect closed or waived in writing; lincheck green on the map, both pools, and the port registry; the differential harness required in CI on four targets; one fingerprint system in use by ports, codecs, and documents.

Phase 3 — Protocols (weeks 8–16). L3, plus P-3 and P-4. Exit: five specifications checked; each has produced a counterexample that changed something; the journal primitive is in production for notifications and moderation; no adapter reads wall-clock time directly.

Phase 4 — Proofs (weeks 12–26, overlapping). L4 targets §9.1 and §9.2. Exit: validator soundness, round-trip, key binding, and canonical form proved in Lean; generated vectors gating four implementations in CI; the visual-language determinism theorem machine-checked.

Phase 5 — Simulation (weeks 16–24). L5, plus P-2 landing on the checked state machine from Phase 3. Exit: nightly randomized-schedule runs; a failing seed reproduces exactly; at least one real defect found this way; the FFI frame protocol implemented against its model-checked lifecycle with the eleven acceptance tests from docs/reaktor-ffi.md §16 green.

14. What each phase retires

Worth stating plainly, because the value of this program is easy to describe badly.

Phase 0 retires exploitability: today a signed-in user can read every conversation in the product. Phase 1 retires invisible change: today a breaking kernel change is discovered by a downstream compile failure, if at all. Phase 2 retires silent corruption: today a mis-ordered coder, a resized map, or a mismatched port can produce wrong answers with no error anywhere. Phase 3 retires distributed guesswork: today delivery, ordering, and idempotency are described in documents and improvised in code. Phase 4 retires whole classes of parser and semantic error permanently, and produces the only artifact that lets Reaktor claim verification honestly — a proved specification that every implementation is checked against. Phase 5 retires irreproducibility: a failure becomes a seed rather than a story.

For an external reader, the sequence also converts the framework's central claim from an assertion into evidence. "The graph is the system" is a strong claim precisely because it says the structure cannot lie. That claim is worth exactly as much as the wiring layer's soundness, which today is D-6. Fix that, prove the format under it, model-check the protocols over it, and simulate the whole thing deterministically — and the claim is not marketing, it is a property with a proof obligation attached.

Appendix A — Traceability

Appendix B — Why these tools

Lincheck rather than stress testing, because stress tests find interleavings by luck and lincheck finds them by construction, then minimises the counterexample. The concurrent structures here are small enough for it to be exhaustive at useful bounds.

TLA+ or Quint rather than Lean for protocols, because model checking finds distributed counterexamples in minutes where theorem proving takes weeks, and because the properties that matter — eventual delivery, absence of duplicate effects, termination — are temporal. Prefer Quint if the team finds TLA+'s syntax a barrier; the underlying logic is the same and the path to generated tests is shorter.

Lean 4 rather than Coq or Isabelle for the pure targets, because its Kotlin-adjacent syntax lowers the barrier for a Kotlin team, its #eval makes specifications executable so vectors can be extracted directly, and mathlib carries the arithmetic the format proofs need.

Alloy for RBAC, because relational models with small scopes are exactly its domain and counterexamples are the useful output.

Deterministic simulation rather than more integration tests, because integration tests sample the schedule space arbitrarily and simulation searches it deliberately, with reproduction for free.

Appendix C — Open questions

1. Should reaktor-graph-core be published as a separate artifact with its own version line, or extracted internally and kept in step with the rest? Separate publishing is the stronger discipline and the larger commitment.
2. Is the fingerprint computed over structure alone, or does it include the fully-qualified name? Structure-only permits accidental aliasing between unrelated types with identical shapes; name-inclusive makes refactoring a rename into a breaking change. The likely answer is name-inclusive with an explicit alias mechanism.
3. Credit units in the FFI: items, bytes, or both? docs/reaktor-ffi.md §17 leaves this open, and large-blob streams argue for bytes.
4. Does the journal primitive (P-3) live in reaktor-db or in a new reaktor-journal? It has consumers in service, notification, and actor code, which argues for its own module.
5. How much of §2–§5 and §8–§13 should be promoted to a public document once Phase 0 closes? The framework half is a recruiting and credibility asset; the security half should stay here.