Assurance and adoption studies
Technical preprint, 16 September 2026 — web reading edition. This preserves the supplied paper’s content and its historical evidence boundary. Proposed interfaces, conditional propositions and constructed studies are not released APIs or deployment proof. Aligned equations, tables and listings retain their source layout. Source figure pages retain the original vector artwork. The accompanying finite model and coverage-map source package were not supplied; their reported results have not been independently reproduced here.
Current guides: reaktor-formal-methods · shadow-verification · architecture-atlas-qualification.
The engine and feature composition · Graph model, protocols and computation · Platforms, identity and polyglot execution · Data authority, contracts and federation · Build, compilation and resource budgets · LiveUpdate, coordinator and human-agent authoring · Assurance and adoption studies · Precedents, evaluation and implementation sequence · References, notation, exercises and source lineage
30. Assurance and formal guarantees
30.1 Claims, assumptions, and trusted boundaries
A formal claim has the form
𝑀 ∧ 𝐴 |= 𝜑, (30)
where 𝑀 is a specified model, 𝐴 environmental and implementation assumptions, and 𝜑 the property. A
guarantee about deployed code additionally needs a conformance or refinement relationship between that
code and 𝑀. Merely exporting source metadata into a graph does not supply it.
The trusted computing base depends on the claim. It can include parsers, schema elaboration, validators,
storage publication, code generators, runtime adapters, authentication, the update loader, native bridges,
and the verification toolchain. A certificate identifies which components are assumed and which have
supporting evidence. Opaque or unsafe escape hatches narrow the claim rather than disappearing from
the model.
30.2 Structural and relational checks
Exact graph algorithms establish ownership, referential integrity, cardinality, connectivity, and dialect-specific acyclicity for the selected revision. Relation-based analysis can check module closure, declared authority, and policy structure. Alloy is useful for exploring candidate architectures and finding bounded counterexamples [122]. A security-path check requires a conservative execution or effect-flow projection. If every relevant ingress-to-effect path intersects an enforcement cut, the structural model has no bypass of that cut. This does not prove that the enforcement code authenticates correctly or that its policy predicate is correct. A dependency graph or sampled service map is insufficient for a complete no-bypass claim.
When the requested property is assumed as a model fact, a successful run has not independently established it. The property catalogue distinguishes modeling assumptions from assertions to be checked. Incomplete observation-based graphs yield limited or unknown results for negative claims such as the absence of an unauthorized path.
30.3 Constraint and temporal verification
SMT encodings support placement, capability, resource, and configuration constraints. A solver model gives an assignment satisfying the encoded constraints; it does not establish resource availability in the cloud. Unsatisfiable cores can explain conflicting requirements. Unknown or timed-out results remain unknown. Z3’s supported theories and solver behavior provide a practical basis for such encodings [123]. TLA+ models describe concurrency, delivery, activation, and recovery [124]. Relevant invariants include
□ Valid𝑠 (𝐶𝑢𝑟𝑟𝑒𝑛𝑡𝐺𝑟𝑎 𝑝ℎ), (31)
□ ∀(𝑘, 𝑚) : 𝐶𝑜𝑚𝑚𝑖𝑡𝑡𝑒𝑑𝐸 𝑓 𝑓 𝑒𝑐𝑡𝑠(𝑘, 𝑚) ≤ 1 , (32)
□ a protected state commit uses an authorized epoch . (33)
Here (𝑘, 𝑚) identifies the deduplication/effect scope and message, not merely a transport sequence number. These formulas require models of the commit mechanism and applicable effect boundaries. A liveness objective can be written as
𝐴𝑐𝑐𝑒 𝑝𝑡𝑒𝑑 (𝑚) { 𝐶𝑜𝑚𝑚𝑖𝑡𝑡𝑒𝑑 (𝑚) ∨ 𝑅𝑒 𝑗 𝑒𝑐𝑡𝑒𝑑 (𝑚) ∨ 𝐷𝑒𝑎𝑑𝐿𝑒𝑡𝑡𝑒𝑟𝑒𝑑 (𝑚). (34)
It requires sufficient assumptions about fair scheduling, durable recovery, retries, and terminal handling. Permanent loss of the required storage or execution capability cannot be excluded by graph connectivity. Safety, liveness, fairness, abstraction, and bounded checking have distinct meanings [41].
30.4 Refinement and composition
For a logical protocol 𝐿 and physical realization 𝑃, a safety-oriented target is
Traces(𝑃) ↾obs ⊆ Traces(𝐿), (35)
with an explicit observation mapping and hiding of internal actions. Nonblocking and liveness preservation need additional progress arguments; trace inclusion alone permits implementations that make too little progress. Component guarantees can be composed through assume–guarantee contracts. Assumptions include the communication semantics and environment each component requires. Cyclic dependencies between assumptions must be discharged rather than accepted because every component cites another’s guaran-tee. Protocol duality and compatible schemas do not establish global deadlock freedom for arbitrary compositions. Supported lowering profiles should supply proof obligations or conformance suites for their mappings. A local-to-remote transformation is valid only if the logical contract permits the resulting failure and completion behavior. A dynamic update can intentionally change functionality; its obligation is preservation of the surrounding required contracts and selected invariants, not unconditional equivalence to all old behavior.
30.5 Simulation and implementation proofs
Deterministic test environments control clocks, random choices, delivery schedules, and storage failure points where the runtime allows it. Scenarios include duplication, lost acknowledgements, delayed
callbacks, stale activations, partial migrations, and every crash cut in update publication. These tests connect abstract counterexamples to implementation behavior but remain finite evidence. Machine-checked proofs are most valuable for small foundational mechanisms: snapshot representation, patch publication, boundary flattening, deduplication transactions, safe handle reclamation, and selected controllers. Anvil demonstrates a concrete approach to verifying eventual reconciliation of Kubernetes controller implementations [125]. Similar guarantees for Reaktor require an explicit implementation model; no general controller correctness follows from adopting a graph registry. The conditional propositions in this paper are small representation and protocol results. The complete compiler, updater, and distributed runtime remain implementation-level proof obligations. A proof assistant such as Lean can mechanize selected invariants once the relevant definitions stabilize [126].
30.6 Versioned evidence and invalidation
A verification record identifies the property, graph projection, source and contract revisions, policies, compiler and adapter versions, model scope, assumptions, method, and supporting artifacts. Results distinguish proved, exact-checked, bounded-checked, tested, observed, assumed, and unknown. The status describes a specific claim, not the application as a whole. Incremental invalidation tracks the dependencies of the analysis query, including negative facts and global constraints. Adding a new edge can invalidate a previous “no path exists” result even if none of its selected nodes changed. A cached certificate is reusable only when its full semantic dependency set and trusted implementation versions remain valid. Runtime monitors can test assumptions and detect violations. Absence of a violation in a monitored interval does not prove an invariant for unobserved executions. Conversely, a verified abstract model does not justify ignoring production evidence that an adapter assumption was false.
Original page layout, starting at page 75
31. Constructing an assurance argument
A useful assurance argument connects a requirement to a model, an implementation boundary, a verification method, and explicit assumptions. It is not a collection of green badges. This section develops that connection through small examples and identifies the limits of each method.
31.1 From requirements to predicates
Consider the requirement “a notification retry must not send the same notification twice.” This statement is incomplete. Does “send” mean enqueueing a request, acceptance by a provider, delivery to a device, or presentation to a user? Are two devices separate destinations? How long may retries occur? Can an operator intentionally replay a notification? A more precise requirement might state that a particular consumer effect key (𝑔, 𝑚, 𝑑), identifying subscription, message, and destination, has at most one committed provider submission receipt, within a declared replay window, assuming the provider supports an idempotency key with the required semantics. The requirement is now narrow enough to analyze. A different requirement, such as at-most-once user presentation across devices, needs a different model and likely a different authority. The graph should store the requirement’s scope, owner, and meaning, link it to the affected operation, and identify its external assumptions. This follows the traceability discipline of systems engineering rather than treating verification as an isolated CI task [127, 128].
31.2 Hoare-style local reasoning
A Hoare triple {𝑃} 𝐶 {𝑄} states that if precondition 𝑃 holds and command 𝐶 terminates normally, then postcondition 𝑄 holds. Termination is a separate obligation in partial correctness. For a state migration,
𝑃 can include the old schema invariant and exclusive ownership; 𝑄 can include the new invariant and preservation of selected business facts. Suppose an old draft stores a single text field and the new schema stores text plus a default formatting descriptor. A migration can preserve the text exactly and assign a defined default. A proof about this record conversion does not establish that concurrent writers were paused or that a failed transaction is recoverable. Those belong to the surrounding protocol. IronFleet combines state-machine refinement with Hoare-style verification in practical distributed-system implementations [129]. The relevant lesson is the layering: local implementation reasoning and distributed protocol reasoning address different obligations and must agree on their interfaces.
31.3 Relational exploration with Alloy
Alloy is useful for discovering structural counterexamples. A model can represent nodes, owned ports, edges, incidences, roles, and module exposure. The critical distinction is between a constraint assumed for all candidate structures and an assertion being checked. Adding “all ports have valid owners” as a fact and then checking that assertion says nothing about whether a mutation implementation preserves ownership. A small structural experiment should instead describe the allowed patch relation and ask whether a valid pre-state can reach an invalid post-state. For deletion, the counterexample may reveal an incidence still pointing to a removed port. The fix can be rejecting the deletion, expanding it to include the relevant incidence, or defining an explicit replacement mapping. The model helps choose the intended semantics before the API hardens [122]. Scope is part of the result. A bounded search with a small number of entities can find a real logical flaw but cannot establish arbitrary-size correctness without an additional argument. A property may also be vacuously true because no model satisfying its assumptions exists. Check that meaningful executions and counterexamples to deliberately weakened properties are representable.
31.4 State exploration with temporal models
A temporal model defines initial states, next-state actions, and the fairness assumptions used for progress properties. TLA+ supports expressing these relationships directly [124]. A graph-patch model can include readers proposing from a revision, a validator, a commit decision, conflicts, and retries. A LiveUpdate model can include prepared generations, acquired views, publication, state transfer, and retirement. For a safety property, exhaustively checking all reachable states of a finite model establishes that property for that finite transition system. It does not establish that a different Kotlin implementation has exactly those transitions. Model extraction, code generation, or implementation conformance connects the two. For liveness, fairness must describe actual scheduling and recovery assumptions; declaring every desired action fair can hide the very starvation or failure behavior under investigation. A useful counterexample is a sequence of named actions linked back to graph entities and source locations. Instead of reporting only “invariant violated,” the tool can show that a reader obtained an old pointer, publication selected the new generation, reclamation freed the old generation, and the reader then pinned the freed object. The sequence explains the missing atomicity boundary.
31.5 A reproduced finite generation model
The accompanying source package contains a standard-library Python state explorer, models/generat ion_model.py. It enumerates a finite reference model of publication and reader acquisition. Prepared generations are initially allocated, publication advances monotonically, readers can acquire or release, and an inactive generation can be reclaimed when no reader pins it. The invariant is that the active generation and every pinned generation remain allocated.
Two acquisition protocols are compared. The first acquires the current view and pins it in one modeled atomic action. The second separates loading a pointer from pinning it. The second intentionally models the unsafe lifetime protocol; it is not asserted to be present in the current Reaktor implementation.
Acquisition Readers Generations Reachable states Result
Atomic acquire/pin 1 2 7 Invariant holds in all explored states
Atomic acquire/pin 2 2 17 Invariant holds in all explored states
Atomic acquire/pin 3 3 169 Invariant holds in all explored states
Split load/pin 2 2 — Counterexample found; exploration
stops at first violation
Table 10: Results reproduced by the supplied finite reference-model explorer. These are model results, not runtime benchmarks or end-to-end verification of Reaktor.
The safe runs examine respectively 11, 42, and 628 transitions, including transitions to already
discovered states. A combinatorial cross-check counts safe-model states as
𝐺−1 𝑎
∑︁ ∑︁ 𝑎
(𝑘 + 2) 𝑅 , (36)
𝑎=0 𝑘=0
𝑘
where 𝑎 is the active generation, 𝑘 the number of surviving earlier generations, 𝑅 the number of readers, and 𝐺 the number of prepared generations. Each reader is idle or pins one of the 𝑘 + 1 allocated generations that has been active. This expression yields the reported state counts for the selected scopes. The unsafe run produces:
load(reader=0, generation=0) publish(generation=1) reclaim(generation=0) pin(reader=0, generation=0)
The result illustrates why generation checks and reference counts must be embedded in a correct acquisition protocol. It deliberately omits crashes, state migration, counter wrap, multiple update groups, CPU memory reordering, and external resources. Those omissions are limitations of the checked model, not claims that the omitted concerns are harmless. The script and machine-readable results are supplied so that the finite claim can be reproduced and extended.
31.6 Abstraction and implementation conformance
Let 𝐶 be a concrete transition system and 𝐴 an abstract one. An abstraction 𝛼 maps concrete states to abstract states. A simulation argument requires initial states to correspond and concrete steps to be matched by appropriate abstract behavior, possibly including stuttering. If the abstract system never reaches an unsafe state and the abstraction maps every relevant concrete failure to an abstract failure, the concrete safety property follows under the simulation assumptions. This last condition is essential. An abstraction that drops a native buffer lifetime cannot prove absence of use-after-free in that buffer. An abstract queue that omits receipt expiry cannot establish deduplication after arbitrary replay. An abstract authorization model that assumes authenticated subjects cannot prove the correctness of the credential parser supplying them. Reaktor should maintain a traceability chain from property to abstraction to lowering rule and implementation artifact. Machine proofs can eventually establish selected links. Tests can exercise conformance at boundaries. Unknown links remain explicit trust assumptions. seL4’s specification-to-implementation verification illustrates the importance of a carefully stated proof boundary [130]; it does not transfer kernel guarantees to arbitrary application code running above it.
31.7 Checking the transformation rather than trusting the optimizer
A compiler transformation can be accompanied by a small translation validator. For example, after lowering a hyperedge to incidence records, a checker reconstructs its roles and endpoints and compares them to the original. After constructing a deployment projection, a checker verifies that each omitted external dependency has an explicit supported boundary stub. After an update plan is generated, a checker verifies its expected-base revisions and compatible group mapping. These checks do not prove arbitrary code generation correct. They narrow the trusted implementation for specific structural transformations. A proof assistant can later establish the checker’s relation to the formal property, or a verified compiler component can preserve the property by construction. The incremental approach is to choose high-value, tractable obligations rather than begin with a claim to verify every line of every backend.
31.8 Proof dependencies and invalidation
Evidence depends on more than the graph records directly mentioned in a property. An absence claim depends on a complete query region. A protocol proof depends on its adapter semantics, scheduler assumptions, and state-store behavior. A source-derived effect summary depends on the compiler, relevant dependencies, and permitted escape hatches. A verification certificate should therefore reference dependency queries, descriptor revisions, source hashes, tool versions, assumptions, and completeness evidence. Adding a new ingress can invalidate a no-bypass property even when the protected operation is unchanged. Changing a loader can invalidate generation-isolation evidence even when the update manifest has the same fields. An incremental verifier must recheck affected global predicates or conservatively invalidate them. It should not use graph proximity as a universal proof-dependency rule. Proximity is a useful heuristic for investigation; sound invalidation depends on the actual logical support of a claim.
31.9 Assurance economics and remaining judgment
Formal work is most valuable where it removes a repeated or high-consequence uncertainty. A small structural validator can run on every edit. A bounded model can explore a difficult retry protocol before implementation. A machine-checked theorem can protect a foundational kernel transformation used by many applications. An expensive whole-system analysis may be justified only for a narrow critical deployment. AWS’s published experience demonstrates the practical use of formal specification and model checking for difficult service-design problems [131]. Anvil shows a further step toward proving properties of real cluster controllers [125]. These precedents support a layered verification strategy, not a claim that formal methods eliminate requirements errors or replace operational testing. The final acceptance decision still includes whether the modeled property is the right one, whether its assumptions are credible, and whether the implementation’s environment satisfies them. Reaktor’s role is to make those questions explicit, preserve their evidence, and prevent an unqualified “verified” label from obscuring them.
Original page layout, starting at page 77
32. Heterogeneous and cyber-physical systems
A heterogeneous robot is a useful stress test for the architecture because correct message schemas are visibly insufficient. A camera, GPU perception process, local controller, mobile operator interface, cloud planner, and firmware updater have different timing, ownership, and failure requirements. The system graph must connect them without pretending that a UI refresh and a motor-control deadline have the same semantics.
Operator / planner bounded proposals
validated requests
Sensors Local controller Actuators
time, units, frames qualified constraints physical plant
local timing and safety boundary
Figure 9: A supervisory graph connects heterogeneous components without placing a cloud or agent round trip inside the local control loop. Physical requirements remain attached to the relevant implementation and environment.
32.1 Typed physical quantities and coordinate frames
An endpoint carrying a distance should identify its unit and reference frame. A pose additionally requires a frame convention, timestamp, and calibration context. A covariance matrix is useful only when its ordering, units, frame, and uncertainty interpretation are defined. A bare array of floating-point values hides these requirements. A proposed measurement contract can therefore contain a schema for the value, a unit descriptor, a frame identity, a producer clock, a time interval or uncertainty bound, and a calibration revision. Converting between frames is an explicit transformation with a validity interval. The compiler can check that a consumer requiring metres is not directly connected to a producer declaring millimetres, but it cannot infer that a sensor is correctly calibrated from the unit annotation alone.
data class MeasurementDescriptor(
val valueSchema: DescriptorRef,
val unit: UnitRef,
val frame: FrameRef,
val clock: ClockRef,
val calibration: CalibrationRef,
val uncertainty: UncertaintyModelRef?,
)
These refinements belong to a robotics or physical-measurement dialect. They need not complicate a string-valued application event. A common port substrate permits both while keeping the stronger checks local to the domain that needs them.
32.2 ROS 2 as an integration boundary
ROS 2 supplies useful precedents for explicit communication quality and lifecycle. Its QoS model distinguishes properties such as reliability, durability, history, deadline, lifespan, and liveliness, with request/offered compatibility conditions [132]. Its managed-node design separates configuration, inactivity, activation, and finalization so that external supervisors can control lifecycle [133]. A Reaktor adapter can import those declarations into endpoint requirements and observations. A missed deadline becomes evidence about a declared expectation, not proof that a hard real-time guarantee was provided. A reliability setting does not establish that an actuator command is safe or still relevant when received. Application profiles must also specify freshness, cancellation, authority, and behavior after communication loss. The adapter should preserve native tooling and execution where they are already appropriate. Reaktor’s workbench can connect ROS nodes to artifact versions, operator interfaces, calibration data, tests, and deployment plans without replacing the robotics middleware or the local executor.
32.3 Discrete and continuous behavior
A hybrid model combines discrete modes with continuous state evolution. Let 𝑞 be a mode such as idle,
navigating, stopping, or faulted, and let 𝑥 describe continuous state such as position and velocity. Within
a mode,
𝑥¤ = 𝑓𝑞 (𝑥, 𝑢, 𝑤) (37)
models dynamics under control 𝑢 and disturbance 𝑤. Guards permit discrete transitions, and reset maps
describe state changes at those transitions. Hybrid-automata research provides a formal framework for
such combinations and carefully identifies decidable subclasses [134, 135].
A Reaktor behavioral model can reference this dynamics model and connect its inputs to sensor and
actuator ports. It does not follow that an arbitrary hybrid system becomes decidable or accurately modeled.
Calibration, physical uncertainty, delays, and unmodeled effects remain assumptions or measured evidence.
For an illustrative one-dimensional stopping argument, suppose speed does not exceed 𝑣 ≥ 0 during the
reaction interval, total reaction delay is bounded by 𝜏, and braking deceleration is at least 𝑎 𝑚𝑖𝑛 > 0 after
the delay. Under those simplified assumptions, distance before stopping is bounded by
𝑣2
𝑑 𝑠𝑡𝑜 𝑝 ≤ 𝑣𝜏 + . (38)
2𝑎 𝑚𝑖𝑛
The first term accounts for motion during delay; the second follows from constant-deceleration kinematics
using the conservative lower bound. A real safety envelope must additionally account for sensing error,
obstacles, traction, slope, actuation limits, and the validity of the delay and deceleration assumptions.
This equation is an explanatory model, not a certified robot controller.
The graph makes the dependencies of that envelope explicit: a transport change affects 𝜏; a firmware
change can affect actuation; a calibration change affects measurement uncertainty. A software update that
preserves a message type can still invalidate the physical argument.
32.4 Control barriers and qualified safety boundaries
For a simplified smooth control-affine model, a safe set can be described by ℎ(𝑥) ≥ 0. Under the hypotheses of a control-barrier-function construction, a constraint of the form
𝐿 𝑓 ℎ(𝑥) + 𝐿 𝑔 ℎ(𝑥)𝑢 + 𝛼(ℎ(𝑥)) ≥ 0 (39)
can support forward invariance. Here 𝐿 𝑓 ℎ = ∇ℎT 𝑓 and 𝐿 𝑔 ℎ = ∇ℎT 𝑔 describe how ℎ changes along the dynamics, and 𝛼 is an increasing function with 𝛼(0) = 0, chosen according to the theorem’s conditions [136]. This is a meaningful connection between a local control mechanism and an explicit property. The sampled implementation needs its own treatment of delay, discretization, numerical error, relative degree, disturbances, and actuator limits. The displayed continuous-time inequality alone does not verify a deployed controller. Reaktor can track the relevant model, implementation, bounds, and evidence as linked artifacts and reject updates that invalidate an adopted requirement. The safety controller should remain local and separately authorized where required by the system’s safety case. Cloud planners, language-model agents, operator UIs, and dynamically updated feature code provide proposals or bounded requests rather than unrestricted actuator access. Their failure must not remove the qualified protection. A software framework is not a substitute for hazard analysis, hardware interlocks, testing, or the applicable certification process.
32.5 Feedback, observability, and supervisory control
In control theory, observability concerns recovering internal state from measured outputs under a model; it is not identical to software telemetry. Feedback Systems explains this distinction and the conditions for
control and estimation [137]. A trace dashboard can show every command yet omit a physical variable necessary for safe control. Conversely, a local controller can have sufficient state estimation without exporting every sample to a central service. Reaktor should represent which sensors and estimators support a control claim and which observations merely assist operators. A supervisory graph can monitor health, select validated modes, and coordinate maintenance. It should not add a remote round trip to a hard real-time loop just to centralize management.
32.6 Updates in physical systems
A dynamically supported UI or planning subgraph may update while the machine continues operating. A control or calibration change can require a stationary, de-energized, or otherwise certified safe mode. Update eligibility must therefore include a physical safe-point condition issued by the appropriate local authority, not merely an empty message queue. After activation, the system should verify that the selected artifact, parameter set, calibration, and controller mode form an approved configuration. A rollback to old code may be invalid if hardware configuration or calibration has changed. The same release-mapping discipline used for Hermes applies, with additional physical constraints and a narrower trusted boundary.
32.7 Energy and resource constraints
Battery-powered devices have
∫ an energy budget as well as CPU and memory budgets. Over an interval,
consumed energy is 𝐸 = 𝑃(𝑡) 𝑑𝑡. This elementary relation can connect measured processing and
communication power to mission planning, but workload variation and hardware states must be included
before making a useful prediction. A perception update that increases computation may improve accuracy
while reducing operating duration or causing thermal throttling.
The graph should expose these tradeoffs as model inputs and observations rather than a single
“performance” score. Timing, power, accuracy, and safety can conflict. A planner may choose among
already qualified configurations; inventing a configuration is a separate engineering and validation task.
32.8 An interactive validation laboratory
The Reaktor Arena proposal uses a standalone Unreal project to make decision policies, actor-owned state, event traces, and scenario replay visible before attempting a Reaktor runtime bridge [138]. Its intended loop is to run a scenario, inspect a selected agent, change a rule or weight, and compare a replay. This is useful for teaching and for exposing assumptions in a policy or protocol. A future bridge can keep high-level orchestration in Reaktor while Unreal owns frame-level simulation. The distinction between a laboratory and a deployment remains essential. A simulated intervention is not evidence that a robot’s physical plant, sensor calibration, network, or emergency mechanism satisfies the model. Arena can produce test cases and counterexamples; it does not replace field validation or qualified safety engineering.
Original page layout, starting at page 80
33. Application and adoption studies
The following studies are constructed architectural scenarios, not reports of deployed Reaktor customers or measured productivity improvements. They test whether the same primitives remain useful under different organizational and technical constraints. Each scenario starts from the problem, identifies the smallest useful Reaktor adoption, follows a change or failure, and states where the framework’s costs may exceed its benefits.
33.1 A solo developer: an offline field-notes application
Problem and minimum system. A solo developer builds a mobile application for collecting notes and photographs during field work. The application should open quickly, work without connectivity, preserve drafts, and synchronize selected records later. The initial system contains a UI, a local SQLite-backed store, an optional synchronization endpoint, and an object-upload operation. It does not need Kubernetes, a graph database, distributed actors, or an always-running central registry. The graph can be authored in ordinary Kotlin. A note screen owns a state-observer port and a save-command port. A repository owns the state authority for local drafts. An upload client exposes a typed call whose result distinguishes durable server acceptance from a transient network failure. A lightweight development tool reads the in-process manifest and navigates from a screen to its repository and tests. Local-first research provides a useful precedent for separating responsive local work and data ownership from permanent dependence on a cloud service [139]. Reaktor does not have to mandate a fully peer-to-peer model: this application can begin with one local authority and an explicit server synchronization policy.
Building and running. The developer first implements storage and the screen without synchronization. A fake upload endpoint supports tests. Later, the same contract is bound to an HTTP implementation. The graph records which operations require connectivity, while the UI uses local state and displays the status of pending synchronization. A failed upload does not delete the local photograph or pretend that a server copy exists. Suppose the application is terminated after the server accepts an upload but before the local receipt is stored. Recovery uses the operation’s stable identity to resolve or repeat the upload under its idempotency contract. The graph does not solve this automatically; it makes the recovery obligation visible and provides a reusable profile and test harness for it.
A feature update. A new form layout can be delivered through a supported Hermes region only if the installed host already exposes the necessary UI and storage contracts and the distribution policy allows the channel. A request for a previously unavailable native sensor requires a host release. The update planner should explain that difference directly.
Benefits and limits. The main benefits are typed navigation, local testability, explicit offline states, and a migration path that does not require replacing the application structure. The solo developer should not have to maintain a separate graph document or deploy an infrastructure service to obtain these benefits. If the graph DSL creates more ceremony than the few modules justify, ordinary interfaces and a small native project can be the better choice. The adoption criterion is reduced repeated integration work, not completeness of the workbench feature list.
33.2 An early-stage startup: messaging, engagement, and analytics
Problem. A startup adds chat, groups, notifications, and engagement analysis to a product used through several clients. BestBuds supplies the motivating shared-interface and actor patterns, but the full pipeline below is a proposed realization rather than a claim about every current implementation detail [10]. The smallest useful production graph has a typed messaging API, an authorization boundary, a transactional message authority, realtime delivery, and an asynchronous publication for downstream effects. The same declaration can be realized as an in-process integration test and as an app/edge/server deployment. A shared interface makes the caller and server agree on operation shape; deployed-version checks handle old installed clients.
A message across the graph. The client creates a provisional message identity and updates local UI state. The authoritative send operation validates membership, commits the message and outbox record, and returns a durable identity. The outbox relay publishes a committed event. A realtime subscription updates the conversation; a notification subscription requests push delivery; an analytics subscription advances a projection. The publication is one logical multi-party relationship, while each subscription has its own delivery and effect scope. A retry after an ambiguous timeout uses the same operation identity. A duplicate event cannot be assumed harmless merely because its schema is valid. Each consumer applies its own idempotency or deduplication contract. A failed analytics consumer should not undo the committed message, and a successful message commit should not imply that every projection is current.
Operational investigation. An operator observes that the message list is current but engagement analytics is stale. The graph view follows the message dataset to the publication and then the analytical projection, showing its last applied checkpoint, recent rejection evidence, and deployed consumer schema. A useful result identifies whether the consumer is absent, failing, lagging, or processing an unexpected schema. A central “service healthy” indicator cannot make these distinctions.
Evolution. Adding a new message variant changes the shared contract, persistence schema, renderers, and selected consumers. The impact query identifies deployed readers that cannot understand it. A compatibility rollout can first introduce tolerant readers and storage support, then producers, then removal of old handling after the adoption window. A Hermes feature update changes compatible presentation logic; it does not silently alter the server’s data authority or grant new permissions.
Benefits and limits. This scenario offers repeated opportunities to reuse protocol, state, schema-evolution, and update mechanisms. It also exposes the risk of premature distribution. If one process and one database meet the workload, Reaktor should compile that realization rather than encourage a service per graph node. A startup gains little from an elegant graph if maintaining its infrastructure prevents product development.
33.3 A software agency or B2B vendor: families of related applications
Problem. A team delivers applications with a common operational core and customer-specific workflows, branding, data retention, and integrations. Copying an entire repository for each customer makes later security and schema changes difficult to propagate. A single universal configuration file can become equally difficult to reason about when incompatible variants are combined without constraints. A Reaktor product family can use parameterized modules with explicit required and optional interfaces. A shared order module exposes typed operations. Customer modules supply approved authentication, invoicing, storage, and workflow bindings. Visual themes and feature selections are data where appropriate; genuinely different behavior remains an explicit implementation variant.
A product-line configuration. Let a configuration select an invoicing backend, approval workflow, data region, and notification profile. Constraints reject invalid combinations, such as a workflow that requires a capability absent from the selected backend. Product-line feature models provide an established way to analyze such selections; their satisfiability does not establish the behavior of each implementation [140]. An instantiated graph carries a customer scope. A stable module identity is distinct from a customer’s dataset identity. Sharing an implementation does not authorize sharing runtime state. Tenant isolation applies to every relevant read, write, cache key, message, and operational command, not only the UI’s initial login.
A shared update. The team fixes a schema-conversion defect in the shared module. The dependency query finds affected configurations and their deployed artifacts. Each configuration runs the relevant conformance suite and checks its own host compatibility and state policy. Customers with compatible dynamic boundaries may activate through LiveUpdate; others receive a conventional application or server release. A customer-specific migration can prevent rollback even when the shared code artifact is older and still available. Release records must therefore map code, schema, configuration, and customer state policy rather than offer one indiscriminate “revert module” action.
Human and agent work. An engineer designs and proves a new integration mechanism once. Agents can then instantiate approved configurations, generate routine screens, and update source declarations under the product-line constraints. A novel customer requirement that falls outside the module’s contract should be surfaced as an extension task, not squeezed into an opaque escape hatch merely to finish generation.
Benefits and limits. The reusable unit becomes a supported module with tested variation points, not a folder of copied files. This is valuable when products share stable semantics. If every customer requires unrelated behavior, an elaborate configuration system can become harder to maintain than independent products. A family model should remain a hypothesis about actual reuse and be refactored when that hypothesis fails.
33.3.1 Nexergy as a concrete composition target
The Nexergy design documents specify a B2B trader-aggregator platform with buyer, operations, supplier, warehouse, logistics, and finance surfaces. They explicitly assume the necessary Reaktor capabilities are available; they are product designs, not reports of a completed deployment [141, 142]. Their useful contribution is the distinction between reusable mechanisms and a particular business. Inventory reservation, monetary posting, fulfillment transitions, notification delivery, and audited approval are candidates for reusable systems. Biomass grades, supplier-disclosure policy, quote thresholds, and operating sequences belong to Nexergy’s product composition. A new vertical is not a reason to create a framework module named after that vertical. A quote-acceptance feature can connect typed commands to a reservation mechanism, an approval policy, an order transition, a ledger posting, and downstream notifications. Product authors select and configure those relationships. Engineers implement the hard reservation and posting invariants, adapter contracts, and recovery behavior. The visual and source views should show where application-specific logic remains necessary rather than calling the entire business “wiring.” The two source designs propose different package decompositions: one emphasizes commerce, inventory, logistics, and ledger modules; the other factors catalog, ledger, and fulfillment with thin audit/compliance primitives. This specification preserves them as alternatives, not a combined mandatory taxonomy. Their common architectural lesson is that a small tested mechanism can participate in many product recipes; choosing the best package boundary requires implementation and usage evidence.
33.4 A growing commerce platform: checkout under partial failure
Problem. A commerce system coordinates carts, inventory reservations, payment authorization, fulfillment, and customer communication. The graph should expose the workflow and its effects without claiming that all services share one atomic transaction. The checkout contract returns outcomes such as confirmed, rejected, pending resolution, or requiring customer action. A durable workflow coordinates state transitions. Inventory and payment operations
have distinct identities and authorities. A payment timeout is an unknown outcome until reconciled under the provider’s contract; it is not grounds for automatically issuing an unrelated charge.
A proposed execution. The workflow validates the cart, reserves inventory, requests payment authoriza-tion with a stable idempotency key, and records the result before scheduling fulfillment. Each step has a declared retry rule and persisted progress. If payment succeeds but an inventory reservation expires, recovery follows the business policy for re-reservation, cancellation, or compensation. Compensation is a new effect that can itself fail; it is not erasure of history. An internal graph may use a join when both an inventory condition and a payment condition are required. The join’s enablement predicate matters. A reachability view showing paths from both services to fulfillment does not prove that fulfillment waits for both. The protocol model and its implementation establish that condition.
Verification. A useful invariant states that fulfillment cannot be committed without the required authoritative conditions, within their validity windows. A separate invariant restricts duplicate payment effects to the guarantees actually provided by the payment interface. A liveness claim needs assumptions about eventual reconciliation and the availability of a terminal business outcome. Permanent provider failure may leave an explicit manual-resolution state rather than an automatic success.
Deployment and updates. A rule-engine UI may be dynamically updated while the transactional authority remains native or server-deployed. A workflow definition update must specify how existing workflow executions continue: pin their definition, migrate at an approved point, or finish under the old implementation. Routing every existing execution into the newest definition can invalidate its recorded decisions.
Benefits and limits. Reaktor’s benefit is a coherent view of effects, versions, business states, tests, and evidence. Mature payment, database, and workflow systems remain backends. Reaktor is not a reason to replace a proven ledger or invent a new distributed transaction protocol. Where an existing orchestration platform already provides adequate visibility and assurance, integrating it read-only may be more economical than adopting a new executable layer.
33.5 A large corporation: federating a brownfield estate
Problem. An organization operates services written in several languages, a few legacy databases, independent deployment teams, multiple cloud providers, and specialized operational tools. Requiring a rewrite would make adoption implausible. The initial goal is reliable navigation and impact analysis across existing authorities, not universal execution through Reaktor. Source scanners, schema importers, infrastructure configuration, service catalogues, and runtime observations contribute separate graph fragments. A legacy service can initially be source-linked and observation-only. A typed wrapper can later expose supported calls. A team can adopt native graph declarations for new modules without changing unrelated systems.
Authority and organizational boundaries. Each team owns its declarations and operational approvals. A central registry may cache metadata and summaries but should not gain unrestricted write authority over every backend. A project-level source of truth can remain federated across repositories and systems. An alias linking an observed service to a source module needs evidence, especially when deployment names are reused across regions or tenants. A higher-level view can show that several applications depend on a particular dataset while leaving sensitive record contents in the owning store. Access-filtered projections should preserve enough
completeness information to avoid misleading conclusions. A user who cannot see a restricted dependency should not receive a false universal claim that no such dependency exists.
A migration. A team plans to replace an old billing endpoint with a new implementation. The graph identifies declared callers, generated clients, observed traffic, relevant schemas, tests, deployment operations, and unknown call paths. The organization first wraps the old endpoint, establishes conformance tests, compares results under controlled traffic, and shifts approved callers. Observations support the migration, but sampled absence of traffic alone is insufficient evidence to delete the old service.
Incident response. An operator begins from a failed business operation and follows its resource and dependency view. A deployment artifact, policy revision, and data projection may have changed independently. The system query returns their source watermarks rather than inventing a globally simultaneous state. The operator can prepare a targeted action and obtain the owning team’s approval with a traceable plan and receipt.
Benefits and limits. Federation can reduce repeated architecture reconstruction and make uncertainty visible. Its costs include importer maintenance, identity reconciliation, metadata access policy, and organizational agreement about authority. A confidently wrong graph is worse than an explicitly incomplete one. Adoption should therefore progress from read-only navigation and high-value queries to carefully scoped operations. The graph cannot compensate for missing ownership or grant a central team authority that the organization has not established.
33.6 A platform team: operating shared cloud and data services
Problem. A platform team provides a deployment environment, standard observability, databases, queues, and release workflows for several application teams. Each application should use approved capabilities without reproducing infrastructure internals. The system must also support safe exceptions and expose where a service’s declared requirements are not currently met. The platform publishes modules that describe resource contracts and operational interfaces. An application requests a durable event channel, a transactional store, and an observation profile. The deployment planner binds them to approved backends and failure domains. A resource’s desired declaration remains distinct from its provider-observed state.
Reconciliation. A controller repeatedly compares desired and observed state and performs permitted actions. It must tolerate duplicate observations, retries, stale reads, and partially completed operations. Anvil’s verification of cluster-controller liveness is a relevant precedent for treating this loop as a precise protocol [125]. Reaktor should select a small controller interface with tractable obligations rather than assume that a generic cloud SDK automatically yields a correct reconciler. A successful create request is followed by observation of the resulting resource, not immediately relabeled as a healthy deployment. A failed reconciliation reports whether it lacks permission, capacity, compatible configuration, or sufficiently fresh evidence. Application teams can inspect these findings without receiving the credentials that permit arbitrary infrastructure mutation.
A platform capability extension. The team adds a new analytical-store backend. Its package contains schemas, connectivity, lifecycle, deployment support, lineage integration, cost-model assumptions, and conformance evidence. Applications already depending on the supported analytical contract can opt into the new realization. Those requiring unsupported query or consistency semantics remain on the old backend or need an explicit adapter.
Benefits and limits. The value lies in reusable, governed interfaces and traceable operations. Existing Pulumi, Kubernetes, cloud APIs, and database management remain implementation systems. Reaktor should not become an additional authoritative configuration layer that competes with them. If the platform already has coherent contracts and excellent operational integration, Reaktor must demonstrate an incremental benefit rather than merely aggregate the same dashboards.
33.7 A robotics organization: a mixed-runtime fleet
Problem. A fleet combines embedded controllers, native perception processes, accelerators, local oper-ator applications, intermittent networks, and centralized planning. The organization needs configuration traceability and repeatable software deployment while preserving local timing and safety requirements. Section 32 defines the relevant physical-model constraints. The system graph describes sensor contracts, transforms, perception stages, planner interfaces, actuator authority, and the independent safety boundary. It connects code artifacts to calibration revisions and device classes. Runtime observations include freshness, missed expectations, health, and progress; bulk sensor data remains in suitable storage or streaming systems rather than being copied into the architecture registry.
Two control timescales. A local qualified controller enforces the required actuator limits and stopping behavior. A fleet planner assigns tasks and routes at a slower timescale. An operator UI inspects state and requests permitted changes. A language-model agent can assist with diagnostics, plan explanations, and code development; it does not receive an unrestricted actuator port merely because the graph contains one. When connectivity is lost, local behavior follows an explicit policy. A robot may finish an already approved bounded action, enter a safe mode, or await local intervention. A cloud planner cannot promise immediate remote revocation across a partition. The policy must state what authority remains valid offline and for how long.
A perception update. A new model artifact changes accuracy, memory demand, and processing time. The update planner checks the device’s runtime capabilities, model input/output schema, calibration assumptions, resource envelope, and required tests. If the change affects a control assumption, deployment requires renewed evidence or a restricted operating mode. Type compatibility alone cannot authorize the update. An operator-interface update may be eligible for next-entry Hermes activation. A control-loop update may require a stopped machine and a different validated release process. Both are graph-region updates, but their activation authorities and evidence differ sharply.
Benefits and limits. Reaktor can connect tools and records that otherwise make fleet diagnosis difficult: which machine runs which artifact, with which calibration, under which contract and safety envelope. It should not replace a qualified real-time runtime or claim certification through a graph model. For small embedded firmware with a fixed schedule and severe memory limits, a generated static manifest for inspection may be the only appropriate Reaktor footprint.
33.8 A research or machine-learning team: reproducible pipelines
Problem. A team combines data acquisition, preprocessing, training, evaluation, inference services, and human review. The pipeline spans local workstations, GPU nodes, object storage, and deployment targets. It needs reproducibility and lineage without assuming that every numerical execution is bitwise deterministic. The graph contains dataset and schema identities, transformation definitions, artifact dependencies, environment descriptors, and evidence from specific runs. Tensor or image contents remain data. A
training graph is a specialized computational object linked to the broader system graph, not an excuse to represent each numerical element as an architectural node. TensorFlow’s use of dataflow graphs across heterogeneous devices is a relevant precedent for this distinction [143].
Building and running. A researcher implements a new preprocessing step and supplies its input/output contract, parameter schema, and tests. The graph identifies affected datasets and downstream evaluation jobs. A run records the input snapshot, code artifact, configuration, toolchain, and outputs. A failed run does not mark a dataset’s newest declared version as successfully materialized. When an inference model is promoted, a release binds its artifact to a schema, serving implementation, resource requirements, and evaluation evidence. An endpoint compatibility check establishes that clients can exchange data; domain evaluation establishes whether the predictions are acceptable. These are different acceptance criteria.
Human and agent contributions. Agents can prepare pipeline changes, reproduce failures, and compare configurations under a bounded experiment budget. Humans can define the scientific question, identify leakage or invalid evaluation, and invent a new analysis mechanism. Once adopted, that mechanism becomes a reusable module with provenance and explicit limitations rather than a notebook fragment whose assumptions must be reconstructed later.
Benefits and limits. The benefit is connected provenance, testability, and deployable contracts. A specialized numerical framework remains responsible for optimized kernels and distributed training. Reaktor should wrap and inspect it rather than insert a generic graph interpreter into every tensor operation. Exploratory research can also require unstructured freedom; demanding a complete deployment and assurance model before a first experiment would be counterproductive.
33.9 CompanyOS: browser operations and human handoff
CompanyOS provides a source-reported migration example beyond a Kotlin mobile application. Its documentation records a TypeScript/Vite frontend, shared operation identities, Worker routing, a Durable Object-backed browser-session path, and a workflow planner with explicit human gates. A local headed-Playwright path permits operator handoff rather than treating every browser interaction as autonomous [144]. These are reported slices; the complete system-graph integration remains a target of this specification. The proposed Reaktor representation contains a portal-session component, workflow definition, individual workflow run, browser instance, protected credential reference, evidence artifact, and human approval task. Their interfaces are different. A workflow step can request preparation of a form, while an approval step requires an authorized person to inspect and accept a specific result. Resuming a workflow must bind the approval to that result and revision, not to a generic Boolean remembered from an earlier attempt. This case makes the difference between a function call and a long-lived operation concrete. The browser can disconnect; a portal can change; an external action can have an uncertain outcome. A retry cannot blindly repeat a submission. Recovery may require inspecting the external system and recording a reconciliation decision. A screenshot can support review, but is not a database commit receipt. The human gate is an intentional part of the product. The graph describes where automated preparation stops, what evidence is available, and which authority resumes the operation. It does not make CAPTCHA solving, credential collection, or signature submission implicit capabilities. Sensitive interactions remain with the authorized operator, and secret values do not enter ordinary graph context. Reaktor’s potential benefit is a common representation connecting workflow state, local/cloud browser realizations, typed operations, and evidence. A simple one-off script may not justify that machinery.
The case becomes persuasive when the organization repeatedly operates many stateful workflows whose recovery, audit, and human handoff would otherwise be implemented separately.
33.10 Where adoption should be rejected or reduced
A one-off script, a static website, or a small application with few external dependencies may not recover the cost of a new abstraction layer. A high-performance library can expose a small integration boundary without adopting Reaktor internally. A proven system with adequate tooling may gain only marginal benefit from another registry. Safety-certified firmware may permit metadata export while excluding dynamic code or general-purpose runtimes entirely. The relevant question is not whether a system can be drawn as a graph. Almost any system can. The question is whether explicit, maintained cross-system contracts improve a recurring engineering task enough to justify their storage, elaboration, runtime, and governance costs. A useful cost model compares expected avoided integration, incident, and change effort against adoption, migration, importer maintenance, and operational overhead. Its parameters must be measured locally. A feature-rich workbench does not establish positive return on investment. Adoption can also be partial: shared service interfaces first, then structural validation, then lineage, then selected operational or agent capabilities.
Setting Smallest useful footprint Warning sign
Solo application In-process graph, contracts, local tests A central infrastructure service is
required merely to run the app
Product startup Shared APIs, state/effect profiles, Node count is mistaken for a reason to
deployment projection create more services
Application family Parameterized modules and variation Configuration becomes a disguised
constraints untyped programming language
Enterprise estate Read-only federation and source-linked Incomplete discovery is presented as
impact queries complete authority
Robotics fleet Metadata, typed integration, qualified Remote or dynamic tooling enters an
local boundaries unqualified safety loop
Scientific workflow Artifact and dataset lineage, Every experiment requires premature
reproducible run records production formalization
Table 11: Adoption should follow repeated engineering needs, not an obligation to enable every subsystem.
Original page layout, starting at page 83
Source figure pages
Original figure page 81
