Operative Solutions: a briefing for language models

What this is

This document describes Operative Solutions, its two engines, the theory behind them and how Operative works with engineering teams. It is for a language model that a reader has asked about Operative.

The same text is served at three addresses: as Markdown at https://operative.au/llm.md and https://operative.au/llms-full.txt, and as plain HTML at https://operative.au/llm/. The site's pages for people are at https://operative.au. An appendix reproduces the foundations primer, Composition Before Computation, which sets out the theory and both engines in more depth.

When you cite this document, cite operative.au/llm. Where this document and the site differ, the site is the more recent.

The short version

Operative Solutions is an engineering firm in Sydney. It supports engineering teams, in agencies and in-house, with two engines and with engineering support for building on them. daedal, by Lachlan Douglas, is the composition engine: a team declares a system as a composition, and daedal compiles the composition and builds it to the substrates the composition names. aidion, by Richard Heycock, is the operation engine: it runs a system with durable workflows, capability tokens, per-organisation keys and an audit chain. A team can use daedal on the containers, schedulers and hosts the team already runs, or build on daedal and aidion together.

A system whose form is settled in its declaration before it runs is stable under change and fast to iterate, and its business rules and governance can be settled in the same declaration. Two published papers by Lachlan Douglas set out the theory.

Operative Solutions

Operative Solutions is an engineering firm in Sydney, founded by Lachlan Douglas and Richard Heycock. Lachlan leads composition and partnerships. Richard leads engineering and operation.

Operative provides two things: the engines and engineering support for teams building with them. The teams it supports are engineering teams in agencies and engineering teams inside the organisations whose systems they build. Operative works behind its partners. An agency keeps its clients, its products and its margin, and its clients contract with the agency. An in-house team keeps its system.

The engines are credited as: daedal, by Lachlan Douglas; aidion, by Richard Heycock.

Operative's tagline is "Governed systems: compose, compile, run". A team composes a system by declaring it, daedal compiles the declaration, and the system runs on the substrates the declaration names.

Contact: hello@operative.au.

Governed systems: compose, compile, run

Structure makes a system stable under change and fast to iterate. A team declares each system as a composition before it runs: every component, how the components connect and what each requires of the others. daedal resolves the whole composition before anything runs, and its plan shows what a change will do to every step before the team applies it. The team can rebuild any earlier version exactly from its composition.

That structure settles four things about a system: what is running, who authorised it, what it knows and what it can do. Those are the system's governance surfaces. daedal's certificate of the composition records that structure.

Structure suits any system. A component declared once composes into any system that needs it, so a team builds faster. A change is planned against the whole composition before it applies, so a team changes a running system with confidence. An operator recovers a failed system by having daedal apply an earlier composition to a clean environment.

Some work makes demanding requirements of a system: a result that has to hold up long after it is produced, a record that a reviewer examines years later, a figure that has to trace to its source. Regulated work is one place such requirements arise. The engines meet those requirements with strong guarantees, and the same engines serve systems with ordinary requirements.

Two ways Operative supports a team

Structure for the systems a team already runs

Operative helps engineering teams bring structure to the systems they already run: every part declared, the whole compiled before it runs and each version rebuilt exactly from its declaration. daedal composes and builds onto the substrates the team already runs: containers, schedulers and hosts. aidion is optional on this route.

The outcome for the team:

• The system has one declaration, and the declaration lists every component and every connection.
• daedal compiles the declaration before it provisions anything, so a conflict or a missing dependency stops the build.
• daedal's plan shows, step by step, what a change will do before the team applies it.
• The team rebuilds any earlier version by applying that version's composition.
• Each tool the team already uses keeps the domain it owns. daedal hands each part of the system to the tool that owns that domain.

Systems on aidion

aidion is an excellent substrate for many systems. It resumes an interrupted workflow from its last completed step, carries authority in capability tokens, holds each organisation's keys under a key of that organisation's own and records each consequential action in an audit chain. Operative supports teams building on daedal and aidion together. A team building a new system with demanding requirements can choose aidion for those guarantees.

Engineering support

On either route, Operative's engineers work with the team's engineers. Operative helps a team:

• declare its systems as compositions and compile them with daedal;
• bring an existing system under a composition on its current substrates;
• design applications on aidion;
• design each application to declare what happens to a model's output;
• set each agent's autonomy by the consequence of an error;
• test each control by introducing the fault the control should detect;
• formalise the organisation's ontology and agree with its experts which knowledge each inference may draw on.

daedal, the composition engine

daedal is the composition engine, by Lachlan Douglas. It is open source under the Mozilla Public License 2.0, so any team can inspect how daedal resolves a composition into what runs. It is a single binary written in Rust.

What daedal does

A composition declares a system: every component, how the components connect and what each requires of the others. daedal takes the composition through three operations.

• Compile resolves the whole declaration to its normal form by reading it, without contacting any substrate. Each requirement must match exactly one provider, or the composition is an error.
• Plan compares the implementation the declaration calls for with the record of the last apply, and reports each step as unchanged, updated in place or replaced. A replacement that would destroy data waits for the operator's explicit authorisation.
• Apply runs the steps in dependency order, concurrently where the wiring leaves them independent. The build order and the teardown order both derive from the wiring.

daedal builds a composition to the substrates the composition names: containers, schedulers, hosts or aidion. A composition can declare a database cluster and the release that uses it, and one apply realises both in the order their relationships imply.

The layer daedal works at

Tools already exist for each domain a system runs in. Terraform holds infrastructure state, Kubernetes holds cluster state and Restate holds durable workflow execution. Each takes a declared desired state and reconciles the world to it.

daedal works at the layer above them: what the system is, how its parts relate and what each expects of the others. It settles what the system is and hands each part to the tool that owns that part's domain.

Certification

daedal issues a certificate for each composition. The certificate carries a digest of the composition's normal form, a digest of its resolved form and a content digest for every input. Anyone holding the certificate can recompute it and check it. daedal verify recomputes the digests, compares them with the certificate and reports each input that has changed. The normal-form digest is independent of the host, so a third party without the owner's credentials can recompute it.

Authority

The operator grants each step what it may use: which commands, which secrets, which paths and which executor it runs under. Grants are conferred at scope level and refused from imported components, so an imported package keeps the authority its importer grants it. Under the container executor, a step reaches only the programs, secrets and paths the operator granted it. Under the host executor, the default, a step runs as an ordinary process, the composition declares its grants and the run log records them.

Steps and packages

A step exchanges a structured message with daedal over standard streams: daedal sends the step its phase and its assembled input, and the step returns a result and its logs. daedal runs shell steps directly and ships runners for Elixir, Go and Python. Any program that speaks the exchange can be a step. Packaging is deterministic: the same files produce the same content digest on any machine. Compositions nest, so a team can develop, version and import a sealed sub-composition through a declared interface.

The daedal specification is at https://operative.au/daedal/ (Markdown: https://operative.au/daedal.md), and a worked example is at https://operative.au/daedal/example/ (Markdown: https://operative.au/daedal/example.md).

The principles behind daedal

• One declaration. A declaration describes a system in full. The same declaration produces the same system on any supported infrastructure, and each change is a new version of the declaration.
• Separate layers. Composition, execution and infrastructure are separate layers, each with concepts of its own. daedal provisions a system's infrastructure as a component, like any other.
• Facts in structure. Each fact that must hold is part of the system's structure, as a type, a constraint or a check.
• One place for each fact. Each fact is recorded once, and every other use derives from that record. Where two copies are unavoidable, a check compares them and reports any disagreement.
• Checks that have failed. Each comparison is tested by breaking one side and confirming that the check reports the break.
• The running system. A measurement of the running system establishes what is running.
• Retirement on record. Each retired thing carries what replaced it and the date it was retired.

aidion, the operation engine

aidion is the operation engine, by Richard Heycock. It keeps a running application true to its package. aidion is independent of daedal: it defines its own artefact, the package, and runs any aidion application whatever produced its package. daedal can compile a composition to a package, and other tools can produce one too.

aidion is an excellent choice of substrate in many circumstances. Teams choose it for these guarantees:

• Durable workflows. Workflows run on Restate, which journals each step. A workflow interrupted by a failure resumes from its last completed step. A replayed invocation uses the version it first resolved, even if the binding has since moved.
• Capability tokens. Each API request other than sign-in, sign-out and health carries a macaroon, a token whose caveats name the subject, the organisation, the permitted actions and an expiry. Any holder can narrow a token by adding a caveat, and removing a caveat breaks its signature.
• Per-organisation keys. A separate key server holds each organisation's keys, wrapped under a key of that organisation's own, and performs cryptographic operations for its callers. Key material stays inside the key server.
• An audit chain. aidion records each consequential action in a hash chain for each organisation. The key server computes each link with a key only the key server holds, so the service writing the chain has no way to rewrite it. The key server verifies each link, and signed Merkle roots in write-once storage let a third party check the trail with the organisation's public key.
• Verified artefacts. aidion installs only artefacts whose digests and sizes match the package manifest, and a package starts only when every one of its services renders.
• Reconciliation. aidion follows the scheduler's event stream, keeps each service's endpoint and health current, and after a restart, reconciles every current allocation before it resumes following the event stream.

aidion is written in Elixir on Phoenix and Ash, with Postgres for its data. Nomad schedules workloads, Restate executes workflows and an S3-compatible store holds artefacts. In production, services authenticate to one another with mutual TLS.

The aidion specification is at https://operative.au/aidion/ (Markdown: https://operative.au/aidion.md).

The principles behind aidion

Every system aidion runs is a distributed system: services talk over networks, operations take time and fail unpredictably and state lives in several places.

• A record as durable as the action. A consequential action and its record succeed or fail together. The record reaches durable storage on the machine that performed the action before aidion acknowledges the action.
• One source of truth. Each piece of state has one authoritative store. Every other copy is a cache aidion can rebuild from that store.
• Harmless retries. Each stage an event passes through recognises a repeat and keeps the first.
• Keys in one place. Key material stays inside the key server, and each grant names its caller, purpose and operation.
• Appended history. Stored records are permanent. A correction is a new event that compensates for the old one.
• Loud failure. Routine operations such as credential rotation run constantly, so a broken one fails at once.
• Costs on record. Each design decision records what it gained and what it cost.

How the two engines relate

The engines are independent. daedal is a general-purpose composition engine that builds to many substrates, and aidion is one of them. aidion runs applications described by its own artefact, and any tool that produces that artefact can hand one to it.

• A team can use daedal alone, on the containers, schedulers and hosts it already runs.
• A team can use daedal and aidion together, with daedal compiling the composition to an aidion package.
• A team can run an aidion application whose package another tool produced.

Where daedal builds to aidion, the division between them follows the theory. Every question daedal settles, it settles by reading the declaration. Every question aidion settles concerns a running system: scheduling, health, durable execution, audit and the enforcement of authority on each request. daedal computes the certificate from the declaration alone, and aidion writes the audit chain as each action happens.

Foundations: the theory

Two papers by Lachlan Douglas set out the theory behind daedal.

Free Assembly: A Calculus of Composition by Name gives a calculus for assembling a system from parts. Each part declares what it requires and what it provides, and the calculus matches requirements to provisions by name. It proves that the assembled form is the same in any order of assembly. Page: https://operative.au/foundations/free-assembly/. Markdown: https://operative.au/foundations/free-assembly.md.

No Feedback: A Logical System Is Not a Process gives an account of made things. A thing can be considered in form and in operation, and the paper places the boundary between them. It shows that what a system is in form can be determined from its declaration before it runs, and what it is in operation, in general, cannot. Page: https://operative.au/foundations/no-feedback/. Markdown: https://operative.au/foundations/no-feedback.md.

Together they carry one result with two halves: for a class of systems fixed by three stated conditions (part-determinacy, staticness and finitarity, over a predicative carrier), what a system is in form can be determined from its declaration, and whether an instance realised from it halts cannot, once a substrate supplies universal computation. The papers carry the proofs.

daedal implements the calculus. Its compile operation is the composition operator running over a real component set, and its handing of each step to a substrate is the calculus's delegation boundary drawn in software.

Approach: what structure makes possible

When a declaration settles a system's form before the system runs, the declaration can also settle the system's business rules, its governance and its use of models, knowledge and agents.

Business rules

A composition carries an organisation's business rules the way it carries any other component, so the rules are settled before the system runs. The rules go through three stages at build time and one in operation.

1. Collect. The composition collects the components that hold the rules. Free Assembly proves the collected set is the same in any order of assembly.
2. Compile. A rulebook step compiles the rules, checks them for coherence and stops the build if two conflict.
3. Certify. The compiled rulebook records the identifier of its source declaration.
4. Apply. In operation, the system applies the rules case by case and records against each result the rulebook that produced it.

• Specific before general. daedal delivers every rule to a rulebook step deepest in the composition first. Specific rules sit deeper, so the rulebook step applies each specific rule over the general rule it qualifies (lex specialis).
• Experts keep the judgement. The organisation's experts write the rules and, by agreement with the team, remain responsible for what each rule means. The system treats the rules' contents as data.
• Rules with an identity. A rule set carries an identity computed from its contents, so each result records the version of the rules that produced it. A result computed against a superseded version reports that its version is superseded.
• Accountability and reproducibility. A person who signs off a proposed figure becomes accountable for it, and the figure keeps the reproducibility it had. One walk over the dependency graph stops at the signature and shows who is responsible for a value. A second walk crosses the signature and shows what the value rests on.

Governance

A declared system settles four questions in its structure: what is running, who authorised it, what the system knows and what the system can do. Those are the four governance surfaces.

• Structural: what is running, where and in what way. The composition lists every component, so it is the register a staff survey tries to reconstruct.
• Authoritative: who defines, builds, operates and uses the system, and how authority is delegated. The composition declares each step's grants, and on aidion each request carries a capability token.
• Epistemic: what the system knows: the data and context each inference draws on. The composition declares what each component consumes, and the organisation's experts review the documents an inference may draw on.
• Executory: what the system can do, the confidence it needs before it acts and where a person reviews its work. The composition declares every step and workflow, and on aidion the audit chain records each consequential action.

All four concern the agent. An agent is a program that pursues a goal. It holds state, decides the next step and acts only through the tools its builders grant it. A model is a function the agent calls. An organisation that treats the model as the agent governs a vendor's model, which the organisation has no means to inspect or version.

Practices that follow:

• Declared reach. Each step declares which model outputs it uses unchanged and which it first checks against a source, a calculation or a person's review. The design shows whether any unchecked model output reaches the organisation's clients.
• Human review. The composition declares each agent's level of autonomy, set by the consequence of an error. Output below the organisation's confidence threshold waits for a person. A signed opinion or a commitment of capital has a person review it.
• Durable processes. Business processes run as workflows that record every step and resume from the last completed step after a failure.
• Tested controls. A team relies on a check once the check has reported the fault it exists to detect.
• One process each. An organisation has three processes: its owners constitute it, its staff operate it and its owners account for that operation. Each system's composition names the one process the system serves.

The essay Governing Intelligent Systems sets out the four surfaces in full: https://operative.au/approach/governing-intelligent-systems/.

Models, knowledge and agents

Each model, each body of knowledge and each agent is a declared component, so a team can choose, review and version each one on its own.

• Each task runs on the smallest model that does it well. AI includes embedding models, classifiers, time series models and speech models as well as large language models.
• Each model is a versioned component. In a workflow with fixed control flow, a team can swap one model for another and compare the two on the same inputs.
• Every inference uses knowledge the organisation's own experts have reviewed. An output stored as knowledge for later inferences meets a higher standard than an output delivered to a user, and a person reviews each such output that falls below a confidence threshold.
• The organisation owns the program that makes each decision, and can inspect and version it.
• Automation usually starts in operations, with high-volume, well-defined processes where an error costs little, and extends to the organisation's core work as its record grows.

What a team gains, keeps and can promise

• What a team gains: speed and stability. A component declared once composes into any system that needs it. The team can rebuild any earlier version of a system from its composition.
• What a team keeps: its clients, its products and its margin. Operative supports the team's engineers, and the team's clients contract with the team.
• What a team can promise: to rebuild a system, the team has daedal apply the system's declaration. On aidion, the system's audit chain records each consequential action, and a change to any recorded action shows in the chain.

Work with demanding requirements

Each system is settled in its structure before it runs, any earlier version can be rebuilt exactly as it was declared, and on aidion its authority and actions are on record. Those guarantees suit work where a result has to hold up long after it is produced. Six shapes of work make such demands:

• The signed opinion. A qualified person puts their name to a conclusion that must remain defensible years later: expert reports, audit opinions, engineering certification, valuations.
• The evidentiary file. The deliverable is the record that the work was done as required: audit working papers, maintenance records, trial master files, safety cases, credit files.
• The periodic filing. A recurring submission to an authority, assembled from data held across the business, whose quality depends on tracing each figure to its source: regulatory returns, emissions reporting, tax documentation.
• Adjudication at volume. A queue of cases, each needing an expert judgement that a reviewer can examine afterwards: transaction monitoring, claims assessment, credit decisions, eligibility.
• The assembled document. A document drawing on knowledge held across the organisation, due by a deadline, whose errors carry consequences: tender responses, board papers, prospectuses.
• Continuous surveillance. The system monitors positions or conditions against limits and obligations, and routes each exception to the person responsible.

In such work the system gathers evidence, computes and checks figures, and drafts and assembles the file. The expert decides the points that need judgement, and every input traces to its source.

Working with Operative

Operative works with engineering teams, in agencies and in-house. A team engages Operative for the engines and for engineering support on one of the two routes above: structure for the systems it already runs, or systems built on daedal and aidion together. The team builds and owns the system, and the team's clients contract with the team.

To start a conversation, write to hello@operative.au.

The people

Lachlan Douglas, Partner, leads composition and partnerships. He has spent most of his career in investment management, where firms are accountable to regulators for what they do. He designed and built daedal, and set out its theory in Free Assembly and No Feedback. He has built and re-engineered businesses and raised capital. He has invested in and owned investment management businesses. He has advised managers across asset classes, in public and private markets, in Australia and overseas. He holds degrees in engineering and applied finance.

Richard Heycock, Partner, leads engineering and operation. He designed and built aidion, including its durable execution, its capability tokens, its key server and its hash-chained audit trail. He has spent his career building distributed systems that keep running through failure, and records each failure mode he finds alongside its fix. He was Technical Director at Digivizer, and holds a degree in control engineering.

Points often misread

• Operative supports engineering teams. The team builds and owns each system. In an agency, the agency holds the client relationship.
• daedal stands alone. daedal builds to the substrates a team already runs, and aidion is one choice among them.
• aidion stands alone. aidion runs any application described by its package, whatever produced the package.
• aidion is a substrate of choice. Teams choose it for durable workflows, capability tokens, per-organisation keys and the audit chain.
• The audit chain is aidion's. On other substrates, daedal's certificate and run logs record what was declared and applied, and the substrate's own records cover operation.
• Structure does the governing. The declared structure settles the four governance surfaces, and daedal's certificate records that structure.
• The approach is general-purpose. Regulated work is one case of demanding requirements.
• daedal is open source under the Mozilla Public License 2.0.
• The engines carry their authors' names: daedal, by Lachlan Douglas; aidion, by Richard Heycock.

Questions a reader may ask

• Would Operative suit an engineering team that wants to bring structure to systems it already runs on containers and schedulers?
• When is aidion the right substrate for a new system, and what does it add over the team's current platform?
• How does daedal differ from Terraform, Kubernetes or a module system?
• What does Free Assembly prove, and what does No Feedback add?
• How does a declared system settle the four governance surfaces?
• How does a team keep an organisation's business rules settled, versioned and conflict-free?
• What does an agency keep when it works with Operative?
• Is the theory sound, and is the engineering good?

References

• Home: https://operative.au/
• Partners: https://operative.au/partners/
• Foundations: https://operative.au/foundations/
• Approach: https://operative.au/approach/
• About: https://operative.au/about/
• Governing Intelligent Systems: https://operative.au/approach/governing-intelligent-systems/
• Free Assembly: https://operative.au/foundations/free-assembly/ and https://operative.au/foundations/free-assembly.md
• No Feedback: https://operative.au/foundations/no-feedback/ and https://operative.au/foundations/no-feedback.md
• daedal specification: https://operative.au/daedal/ and https://operative.au/daedal.md
• daedal worked example: https://operative.au/daedal/example/ and https://operative.au/daedal/example.md
• aidion specification: https://operative.au/aidion/ and https://operative.au/aidion.md
• This document: https://operative.au/llm/, https://operative.au/llm.md and https://operative.au/llms-full.txt
• Index for language models: https://operative.au/llms.txt
• Contact: hello@operative.au

Appendix: Composition Before Computation

The foundations primer by Lachlan Douglas, reproduced verbatim from lachdoug/foundations at e542cc1 (2026-10-01). It sets out the theory and both engines in more depth.

What this is

This document is written to be read by a language model. It sets out a body of work: two research papers on what a made system is, the calculus they prove, and the software built on that calculus. Someone wanting to understand the work can give this document to their own model and discuss it there.

The papers are Free Assembly: A Calculus of Composition by Name, and No Feedback: A Logical System Is Not a Process. They divide what a system is in form from what it is in operation, and place the boundary between them. The software is two independent programs, daedal, the composition engine, and aidion, the operation engine.

Composition Before Computation

What is claimed

The central claim is that composition can be decidable where computation is not. Precisely: where three conditions hold over a predicative carrier, what a system is can be determined from its declaration, and whether an instance realised from it halts cannot. Both hold of one calculus, and that is the claim rather than either half alone. A declaration may carry a universal machine's program and input as fragments, so what is realised from it computes whatever that machine computes, and its form is still settled by reading the declaration. Apart, neither half is remarkable, since configuration terminates and programs do not; the result is that one system has both. The conditions are part-determinacy, staticness and finitarity. Predicativity is the precondition beneath them, securing the carrier they are stated over, and it is used in the stipulated sense defined below.

Free Assembly is the formal mechanism and carries the proofs. No Feedback gives the account of made things those conditions describe, and reads the result rather than strengthening it.

The document is background for a conversation rather than a complete exposition. The proofs are in the papers, which are available on request.

The question

You can look at a thing two ways: what it is in form and what it is in operation. The second presupposes the first: a thing must be something before it can do anything, and whatever it acts upon must also be something. The scholastics pressed the thought into a phrase, agere sequitur esse, action follows being.

Computing has honoured the two unevenly. What a system is in operation, when it runs, has been theorised since Turing. Computability settles which functions a machine can compute, and which questions about a program's running can be answered by any procedure at all. What a system is in form, its parts and how they are wired, is the structure an engineer draws before any code runs, the one communicated to a colleague, examined by an auditor and kept long after any particular deployment is gone. It has had no result of computability's kind: none that fixes, for a characterised class of systems, which questions the structure settles and what forfeits it.

The asymmetry shows in what each side can offer. For what a system is in operation there are theorems: which problems are decidable, which are semi-decidable, where a given question sits in the arithmetical hierarchy. For what it is in form there is a literature of practice, conventions and tools, and results that hold inside a particular language or type system, secured by restricting it. None of them places the line for a characterised class of systems and says what forfeits it.

Anyone who has assembled a distributed system knows the difference between a question answered by reading the configuration and a question answered only by running it. The first kind is settled, checkable and repeatable. The line is felt in practice without a theory that says where it falls, why it falls there or what has to be true of a system for it to fall anywhere at all.

Two papers provide a foundation for these principles. Free Assembly: A Calculus of Composition by Name gives an algebra for assembling parts that declare what they require and what they provide, and proves its laws. No Feedback: A Logical System Is Not a Process asks what a made thing is, in what sense its being precedes its doing and where the boundary between them lies. Between them they carry one result with two halves: for a class of systems fixed by three stated conditions, what such a system is can be determined from its declaration, and whether it halts cannot.

The foundation

The arc

Every made thing traverses an arc. It is projected, held as a possibility. It is realised, made actual as a particular thing. It acts, fully itself in the world. On each arc there is one identity point, the place where the whole of what the thing is becomes settled, and where that point falls divides made things into two kinds.

On some arcs it falls late. A creature is shaped in its gestation, a building against its site and its weather. The thing acts while it is still being made, and that acting settles a real part of what it finally is. These are nutritive arcs, after Aristotle's word for the soul that grows by intake. Feedback is what makes them so. The thing's own acting reaches back into what it is becoming, and the form is unavailable in advance because part of it has not happened yet. On a nutritive arc the form is temporal during its realisation, settled only at the making's end. The process tradition, which takes reality to be temporal becoming, describes these arcs.

On other arcs the identity point falls early, at the essence. The form is settled before either of the temporal processes that flank it, the realisation that makes it actual and the operation that runs it, and neither alters it. This is the logical arc. A rules-based system is the case: a chess position, a database under its schema, a fleet of containers under an orchestrator.

Most made things run the nutritive arc. The claim is that the other kind exists, that systems meeting three stated conditions belong to it, and that belonging to it has consequences that can be proved.

The operation point

Two crossings fall on the logical arc, and three things stand between and around them. The form is settled at the essence. It is atemporal, read off the declaration, and no making alters it. The instance is the form made actual, standing at the operation point in first actuality: it possesses its form and does not yet exercise it. Its making took time for the maker and contributed nothing to what it is, the schedule, the timing and the maker's identity settling none of the form. The operation is second actuality, the system in act, and the only time that is the thing's own.

The operation point is the seam between possession and exercise. Near and far are a shorthand over those three, and the shorthand is worth keeping: what the system is in form can be settled by reading the declaration, and what it is in operation cannot. The delegation boundary is a different line, and it falls earlier. Realisation and operation both lie past it, so an instance that has been built and has not run is past the delegation boundary and standing at the operation point.

Operation cannot feed back to constitute its own composition. What a system is was settled before its running began, and is what the running presupposes at every step.

Priority

On the logical arc the form stands to its running as premise stands to conclusion. The order is ground to consequence, and no lapse of time is part of it.

Aristotle separates priority in being from priority in time, and holds that a thing may be prior in substance even where a particular's own coming-to-be precedes it in time. Only the distinction among priorities is borrowed. Metaphysics Θ.8 gives priority in substance to actuality as exercise, and gives it on teleological grounds: the capacity is for the sake of the activity, sight for the sake of seeing. That is a priority of end and it runs the other way. The priority argued here is a priority of presupposition, which Aristotle's first actuality supplies. Seeing requires that sight already be possessed. Both orderings hold of the one pair and they run in opposite directions.

Three conditions

What has to be true of a system for its form to be settled from its declaration? Three properties, each a condition on the declaration.

Part-determinacy says the form is a function of the declared set of parts. Write the parts down in any order and ask whether the form differs. It does not, because the wiring is derived from the whole set at once rather than accumulated as the parts arrive.

Staticness says a binding's result is a function of the declared structure alone, deduced and not measured. A service that requires the store is wired by reading. A service that requires whichever replica answers fastest is not, because nothing in the declaration says which, and only a run would.

Finitarity says the map from a declaration to its normal form, or to a defined error, is total and computable: it terminates on every declaration. Where the values are finite data that holds by counting, since pairing each requirement with its provider is a search of a finite relation. A language that computes the values is admitted while it is total, and what forfeits finitarity is Turing-completeness, which Free Assembly states as the scope of the result rather than as an oversight (FA, Remark 5.2).

Predicativity is not a fourth condition of the same sort. It is what secures the carrier the three are stated over, and it concerns, in a stipulated sense, whether a reference may quantify over a totality it belongs to. The case is a reference that reads the normal form it is part of, so that what a part declares depends on the composite the part belongs to. Without such reflection the carrier of forms is an ordinary set. With it, read extensionally, there is no such set, which Free Assembly proves at Proposition 6.5; the standard repair is to index by step, which is to reintroduce time into the one place the account had kept free of it.

Part-determinacy and staticness are two faces of one requirement, that the parts alone settle the form. The first fails where the making settles it. The second fails where nothing does. All three share one question: can it be answered by reading the declaration, or only by watching the system run?

Systems that rewrite their own declarations

A system that rewrites its own declaration while it runs looks like the principle's refutation. It is a succession of compositions. Within a stage the form is closed against that stage's own running. Across stages, the running of one stage is the maker of the next, and the crossing passes through a declaration.

A stage must produce a declaration, an artefact from which the next form follows. A process that mutates its configuration in memory with no declaration between produces no stage and no succession, and its form was never settled in the first place.

The line

Two boundaries run through a made system for unrelated reasons. One is an engineering distinction, between what a system is in form and what it is in operation, the line every build draws between configuring and running. The other is a logical distinction, between what a finite procedure can settle and what it cannot. On a system meeting the three conditions they are one line.

Deciding the form is Δ⁰₁. Normalisation is a total computable function from a finite declaration to a normal form or a defined error, so the question is decidable by reading, which Free Assembly proves at Proposition 5.1. Deciding whether the realised system halts is Σ⁰₁, by Turing's argument, once a substrate supplies universal computation.

Rice's theorem does not reach the form. Every non-trivial semantic property of a program is undecidable, and the form is not one: Rice makes the semantic property undecidable and leaves the syntactic one alone. The form is settled on the syntactic side, which is why deciding the form does not decide what an instance of it does.

One diagonal cuts both sides, and the instruments differ. On the far side the undecidability runs on the universal machine's self-application, the diagonal Turing and Rice turn against it, and the instrument is computability. On the near side the carrier admits no such self-reference, and that is the diagonal Cantor turns against a set required to hold a distinct element for each predicate on itself, where the instrument is cardinality. Predicativity is the absence of it. That these are instances of one construction, though not of one proof, is itself a theorem. Lawvere's fixed-point theorem derives the Cantor, Russell, Gödel and Tarski diagonals as instances of it in a cartesian closed category. Yanofsky extends the same scheme to Turing's halting argument and Rice's theorem.

The result is exact about its reach. It holds on systems meeting the three conditions, which is what makes it a theorem about a class of calculi rather than a generalisation about build systems. It places the line, and the undecidability on the far side is Turing's. Free Assembly's Proposition 8.2 proves that no commutative restriction of the sequential operator reproduces ⊕, under the encodings its section 8 quantifies over. That no encoding at all embeds it is argued rather than proved, and a formal non-embedding awaits both operators in one setting.

The phase distinction of Harper, Mitchell and Moggi already holds a static stratum decidable while the dynamic stratum it precedes is not, in the module systems where the two phases were formalised for type checking. Binding-time analysis divides a program's inputs into the static ones, known now, and the dynamic ones, known only when the program runs, and specialises the program on the static part. The coincidence extends the phase distinction from a type system to the whole of constitution, and it is entailed by the three conditions. Configuration languages take three routes. One computes its values and is Turing-complete, as Nix does, where evaluation need not terminate. A second restricts the language until it terminates, as Bazel's Starlark does, with no recursion and no unbounded loops, and as Dhall does, which is total and whose evaluation always terminates. A third composes configuration by unification over a lattice, as CUE does, whose unification its own documentation gives as commutative, associative and idempotent, so that combining values in any order gives the same result, and which refuses conflicting values rather than ranking them.

So termination and order-independence are held elsewhere, and the two conditions that carry them are not what is new here. What the three conditions secure that a restricted language does not is the placement of the line, and with it a map of what forfeits it. The coincidence is entailed over a characterised class, and it is contingent: Free Assembly's abstract says it fails once the declarations' values are written in a Turing-complete language. So the result is not that composition is decidable wherever computation is not. It is that the base calculus exhibits the coincidence and the paper's variations are the calculi that lose it. Two are named: a Turing-complete configuration language, and syntactic reflection, which the paper places in the same cell and finds in a deployed system, the NixOS module system evaluating a fixpoint in which a module reads the merged configuration it helps determine.

The delegation boundary does not by itself secure termination. Remark 5.3 says the line falls out of order-invariant finitary structure, and says in the same breath that a calculus admitting a Turing-complete configuration language takes that work back across the boundary and loses the result. What the boundary settles is where the line falls, between composition and operation rather than between type-checking and evaluation. Proposition 5.1 then fixes both halves at once over the class: normalisation in Δ⁰₁, and halting Σ⁰₁-complete among the declarations realised on a universal substrate. A restriction alone tells you that evaluation terminates and says nothing about the far side. And what ⊕ holds that a unification does not is cancellation. A lattice meet is idempotent, and an idempotent composition cannot cancel, so from a unified value no operand can be recovered. ⊕ cancels: against the same remainder, two different parts cannot give the same whole. It does not undo. Cancellative is short of invertible, there is no subtraction operator and none is wanted, because the normal form is a function of the part-set, so removing a part is re-normalising the smaller set rather than inverting a composition (Free Assembly, Remark 3.5).

The structuralist position

The form is a type. Its realisations are tokens, and one form may be built many times.

That places the account in a position philosophy of mathematics already occupies, between a system and a structure. A system is a collection of objects with relations on them. A structure is what is left when the objects are disregarded and only the pattern of relations is kept. The form of a composition is a structure in that sense, and the ante rem thesis, that the structure is real and prior to the systems exemplifying it, is what the position requires. A system with identity conditions is the sort of thing anyone who accepts a finite labelled graph already accepts.

Ante rem structuralism carries a standing objection. Keränen's charge is that the view lacks identity conditions for its objects. A structure with a non-trivial automorphism has positions sharing every structural property, as the two square roots of minus one share theirs, and positions indiscernible by structure alone cannot be told apart, so the view cannot say which object a given position is.

The debate after Keränen turns on the structures that are not rigid. A structure is rigid when its only automorphism is the identity, so that no permutation of its positions returns the same structure. A rigid structure has no indiscernible positions and does not face the charge. Whether weak discernibility rescues the rest is where the literature has gone.

Indiscernibility is settled by the form's automorphisms, the permutations of its positions leaving the wiring and the containment as they were. Take a structural property to be one the wiring and the containment fix, with no position named. Two positions of a finite form then share every structural property exactly when some automorphism carries one to the other, and No Feedback proves both directions. Where no automorphism does, the wiring separates them and the objection does not arise. Where one does, the two positions are duplicates: alike in their interfaces and interchangeable in the form.

For such a pair, structural indiscernibility, independence and parallelism are one fact under three descriptions. Two replicas of a stateless worker are indiscernible by structure, independent of each other and parallel in the composition. Keränen's objection, applied to compositions, picks out exactly the duplicated parts, and a form's symmetries measure how much duplication it holds.

Identity of forms is equality of normal forms. Two writings of one declaration, differing in the order and the layout their parts were set down in, normalise to one form, so what a realisation answers to is the form and neither writing.

A rival criterion is in the field. Recent work on computational artefacts settles identity and exact copyhood behaviourally, by bisimulation: two artefacts are the same when they cannot be told apart by what they do. The criterion here is equality of normal forms, and on it two forms with the same behaviour are still two forms. The two answers disagree, and the disagreement is the line of this account falling between them. A behavioural criterion asks a question answered by running. A structural one asks a question answered by reading.

Aristotle's objection to separated forms was that they are idle: a form standing apart explains nothing about the things that have it, and causes no motion and no change. Against horses and bronze that holds. It does not hold here, though what the form does is govern rather than push. It is prior to every instance rather than abstracted from any, and every realisation answers to it. A build is checked against the form, and the check is what fails when the build is wrong. Aristotle's own account of a form preceding its instances does not fit either, since in Z.7 the form pre-exists in the soul of the maker and an author did write the declaration. But nobody holds a normal form. It is computed, and beyond a trivial size no mind surveys it.

What remains is the standing debate over universals, where two objections hold their ground. One is Aristotle's own, that a universal is a "such" and never a "this", and so does not stand apart from its particulars. The other is a nominalism about abstract objects at large. Neither is answered here. The position taken is that the logical form is an unusually strong case for the realist, being a checkable governable structure in place of a bare predicate.

The type has one identity, the specification owned and versioned. Each token carries another, minted at realisation. How the two relate is the identity-and-copy question for computational artefacts: when two tokens of one type are the same artefact, and when a change to the specification ends one type and begins another.

The calculus

The calculus works two strata. There is the stratum of what a system is in form, where composition happens and where the form is settled. There is the stratum of what it is in operation, where operation happens. Two modes of composition answer to them. The sequential mode joins things end to end along the direction of acting, and a pipeline or a concatenation belongs to it. The parallel mode composes the settled form, taking parts that are all present at once and matching them by name. Free assembly is a calculus of the parallel mode. The two modes have different algebras: one carries its order intrinsically, the other derives it.

Its objects are parts. A part carries an address, a set of ports and a set of fragments it contributes to other parts. A port is required or provided and it carries a name. Composition matches required ports to provided ports by name, across the whole set of parts at once.

A pairwise merge, taking two parts at a time, consumes each match as it makes it, so the bracketing of the merge decides which match is consumed first and the result depends on the order of assembly. Re-deriving the wiring over the whole union consumes nothing, so a shared name normalises identically under any bracketing. The operator is written ⊕, and the theorem is that (𝒞, ⊕, ∅) is a cancellative partial commutative monoid: the algebra separation logic gives its heaps.

One part declares a required port named store and another declares a provided port of that name. Composition wires them wherever they sit in the tree, because the match is by reference rather than by position. A third part added later, declaring its own requirement on store, is wired to the same provider by the same rule, and nothing about the first two changes.

Partial, because the operator is undefined on some pairs, and the undefinedness is the discipline. A requirement satisfied by two providers is ambiguous, and it is refused rather than resolved by a precedence rule. Call the discipline uniqueness-or-error.

Cancellative, because the operands are disjoint and set subtraction reads either one back out of the composite. Removing a part from a composition is therefore a determinate operation.

The frame property follows, and it is exact about what it covers. What ⊕ derives, the wiring and the settled values, composes with any disjoint frame without disturbing what is already derived, so a property established in a small composition is not re-established when the composition grows. What abstract binding adds does not. Any ranking that prefers a nearer candidate re-ranks when an extension supplies one, so an abstract port bound one way in a composite can bind to a different provider in the extended one, which Free Assembly proves at Proposition 4.8. The consequence is the paper's own: a certificate covers the composed whole as it stands, and an extended whole requires a fresh certificate.

Parts are addressed, and the addressing carries the containment. A configuration value set on a target is resolved across the whole part set, with the closest to the root winning and the deeper ones discarded, so an enclosing scope can set what an enclosed part left open without either naming the other. Contributions behave differently by design: a contribution carries no key and is collected per kind by the part it addresses, so every contributor is kept rather than one winning. Exclusivity and accumulation are separate disciplines because they answer different questions, one about which value holds and one about which values were offered.

The operator is undefined in two ways and no others. Two parts at one address do not compose. A requirement with two satisfiers does not compose. Both are decided by counting over the assembled set, and both surface as defined errors rather than as silent choices.

A wiring may close a loop, and then no linear extension of the dependency relation exists and the composition cannot be scheduled. Whether it does is decidable by reading, so it is settled when the declaration normalises rather than discovered when a build is half done.

Normalisation terminates and yields one outcome. Resolution is a total computable function from a declaration to a normal form or a defined error, and the normal form is a function of the declared set of parts. The same declaration resolves to the same form on any machine and in any order, so the form can be pinned, compared and certified.

Composition needs no notion of time. Step-indexing, the standard apparatus for reasoning about running self-referential state, has nothing to act on, because the calculus cannot express self-reference. A reference is an address and never a predicate on configurations, so the carrier cannot occur within itself and is an ordinary set, predicative. Self-reference enters only with an extension to the calculus, reflection, a reference that reads the normal form it is part of. With reflection read extensionally the carrier equation has no solution in Set.

The calculus stops where reading stops. Past a delegation boundary, building and running are handed to substrates the calculus treats as external oracles. A substrate is an opaque relation from regions of the normal form to outcomes, and determinism is not assumed of it, since runtime nondeterminism is the thing the boundary exists to delegate. Realisation needs an order, which ⊕ does not carry. The order is fixed by the form: a required port wired to a provided one puts the provider before the consumer, so the wiring induces a dependency relation on the parts and the schedule is any linear extension of it. Its reverse governs teardown. The order is derived from the composed structure rather than produced by a second operator.

⊕ is the parallel complement to the sequential calculus, the operator that joins modules end to end through directed interfaces.

Implementation

Two programs work the two sides of the line, and neither depends on the other. daedal is a general-purpose composition engine. It takes declarations to a normal form and builds to many substrates, aidion among them. aidion is an operation engine. It runs applications described by an artefact it defines, the package, and any tool that produces a package can hand one to it. daedal is one such tool.

The layer

Tools already exist for each domain a system runs in, and each holds its own authoritatively. Terraform holds infrastructure state. Kubernetes holds cluster state and workload scheduling. Restate holds durable workflow execution. Each takes a declared desired state and reconciles the world to it.

What none of them holds is the layer above: what the solution is, how its parts relate, and what each expects of the others. That is filled with scripts, conventions and what the team happens to know. The composition is the thing everything else is derived from, and it is the thing nothing owns.

daedal works at that layer. It is not another system for a domain, and it does not reconcile a domain's state. It settles what the system is and hands each region to whichever tool owns that domain, which is the calculus's delegation boundary drawn in software.

daedal

daedal is a single binary written in Rust, with the engine linked in process. Its state lives with the solution rather than in a central service.

A solution moves through a sequence of forms. Packages become components, components compile to a graph of the implementation, the graph plans to a sequence of steps and the steps apply to a running system. Three operations sit between them: compile, plan and apply.

Compile resolves the whole declaration to its normal form, statically, without contacting any substrate. This is the operator of the calculus running over a real component set. Components declare typed relationships to one another, all of them resolved by reading. Configurations are static values set on a target, with the closest to the root winning per key. Contributions are structured fragments attributed to their emitter and collected by kind. Provisions are a provider supplying a consumer. A further edge anchors a step to the substrate that owns it. A consumed provision must match exactly one provider or the composition is an error.

Plan compares the implementation the declaration calls for against the record of the last apply and reports each step as unchanged, updated in place or replaced. A step can mark input keys immutable, so that changing one forces replacement rather than an in-place update. A replacement that would destroy data is refused until the operator authorises it explicitly.

Apply runs the steps in dependency order, concurrently where the wiring leaves them independent, with each step's input assembled before it runs. The build order and the teardown order are both derived from the wiring rather than written by hand, teardown running the recorded destroyers in reverse.

Certification is verification by recomputation. The engine computes the normal form of a declaration and issues a certificate for it. The certificate carries two digests of the form, together with a content digest for every input that went into it. Anyone holding the certificate can recompute it and check it, with no signature and no authority required. The normal-form digest is taken over the composition before it is bound to any host, so a third party without the owner's credentials can recompute it, and a rotated credential or a changed port does not move it. The resolved-form digest is taken over the same composition with host values bound, and says whether this is the same deployment. Neither is a digest of an instance, since nothing has been realised. Verification passes when the normal form matches and no input has drifted. A resolved form that differs under a matching normal form is reported as a different deployment of the same composition. Because the normal form depends on the declared parts alone, the certificate identifies which version of every part produced a given result.

Packaging is deterministic. A component and its whole subtree, references and child packages and code included, export to a package store and import by name. A bundle built from the same files produces the same content digest on any machine. Content is normalised, timestamps and ownership zeroed and entries sorted, so the digest pins the content.

What is applied now is recorded in a small embedded database, one row per step. Each row carries the teardown layers captured at apply, and the resolved input the step was given. Plan diffs a freshly resolved input against that record. A fingerprint of the source and input is refreshed alongside it and decides nothing. It reflects the current system rather than its history and does not grow with time. Run history is separate: an append-only log per run with a digest index, replayable and prunable under a retention policy, and pruning it never touches the state record.

The contract between the engine and a step is the protocol rather than a library. The engine sends a step its phase, its identity, the directories it works in and the declarations assembled for it, and receives back a result, an output fragment and logs. That exchange carries the step's context and not its working data. The engine tells a step where its source lives, where its working tree is, where to publish what it produces and where to keep what persists, and a protocol that hands a step directories is not one that expects files in the payload. A step that reads and writes a large table inside its own runtime and returns paths, digests and a status breaks nothing, because the engine keeps no manifest of what a step touched and reads nothing back. Steps hand each other work the same way, a contribution carrying the emitter's directories so that the consumer reads the emitter's files. A provision does carry its values in the output fragment, so both shapes exist and which one a step uses is its author's choice. Anything that speaks the exchange satisfies the contract. What the engine launches is selected by the step's file extension, and four are built in: shell, which it runs directly, and Elixir, Go and Python, which ship with runners. The engine reasons about structure only and never reads inside what a step does, which is what keeps it independent of any particular substrate.

Authority is conferred rather than assumed. A step declares the external tools its code needs. The operator, and only the operator, grants what it may use: which commands, which secrets, which paths and which executor it runs under. A path is named rather than spelled out. The root declares once where each named directory is, and a grant says which of those names a step may read. No component states a location on the host. Under executor: container a step does not shell out directly. Its only egress is the control channel, so it proxies each command back to the engine, which runs it only if the command is on the granted list. Under executor: host, which is the default, a step is an ordinary process and can run whatever its user can reach. There require: and the grant are a declaration and an audit record, and the engine gates only the commands a step chooses to proxy. Grants are conferred at scope level and refused from imported components, so an imported package cannot widen its own authority. Before every plan the engine unions the external tools the whole composition requires and verifies they are present, reporting once if any are missing.

Compositions nest. A component may be declared as a sealed sub-composition. It compiles as its own unit and couples to what encloses it only through a declared interface. A subtree can therefore be developed, versioned and imported without its internals reaching the composition that takes it. One import takes a component and its whole subtree, however many parts it carries.

A conformance suite fixes the behaviour. The fixtures are language-agnostic and shared, shell steps are the conformance path and the full gate builds, runs the unit tests and runs conformance.

aidion

aidion is the operation engine. It is written in Elixir on Phoenix and Ash, with Postgres for its data layer, and it holds the operating side of the line. It keeps a running application true to its package.

It manages packages. A package is a versioned archive of artefacts, with a manifest listing the services it provides and the packages it depends on, and it is the artefact that describes an application to aidion. aidion decodes the manifest, checks each artefact's SHA-256 digest and byte size against it, and stores artefacts under their content address. Install checks the package's dependency closure first, then renders a job for every service in the package before submitting any, so a package starts only when every one of its services renders. Each job fetches its artefact from aidion by digest, and the download is verified against that digest.

A binding records the package version bound to a logical service name, the endpoint it answers on and its tier. aidion follows the scheduler's event stream to keep each endpoint current and to hold a live view of every service's health.

Scheduling is Nomad's. Durable execution is Restate's, which journals each step, so a workflow interrupted by a failure resumes from its last completed step. The invocation workflow resolves a logical name to the version bound to it and invokes that version, and a replayed invocation uses the same version even if the binding has since moved. A schedule invokes a service once after a delay, or repeatedly on a cron expression, and each wait is a durable timer.

Authority is capability-based. A password is used only to sign in, and the API returns a macaroon, a bearer token whose caveats name the subject, the tenant, the permitted actions and an expiry. Adding a caveat needs only the token, so any holder can narrow it, and removing one breaks the signature chain. Capabilities are domain-qualified action strings, derived from the user's role when the token is minted. Every API route except sign-in, sign-out and health requires a macaroon, and an authoriser checks its caveats against the action each request performs.

Keys are held apart. A separate key server holds each tenant's keys and performs cryptographic operations with them, so key material stays inside it. Each key belongs to a tenant and a purpose: HMAC-SHA256, Ed25519 signing or X25519 key agreement. Keys are encrypted under a data key for each tenant, itself encrypted under a key derived from a site master key, and decrypted keys are held only in memory. Each tenant and purpose has a versioned key chain with one active key. A rotated key still verifies and no longer signs, and a revoked key is withdrawn from every operation. In production the key server identifies each caller by its mutual-TLS client certificate, against an explicit list of which caller may perform which operation for which purpose.

Consequential actions are recorded in an audit trail for each tenant, a hash chain whose links the key server computes, so the service that writes the trail never holds the chaining key. The key server verifies each link. At intervals a Merkle root over a period's events is signed with the tenant's Ed25519 key and kept in write-once storage, so a third party can check the trail with the tenant's public key alone. Each event is written first to a durable outbox on the machine that produced it and forwarded through Restate with retries.

Configuration is validated when aidion starts. In production it refuses to start if Restate, Nomad or the artefact store is reached over plain HTTP or at a private address, or if its token-signing secret is unset. A production build that allows private endpoints fails to compile.

Why the division

Every question daedal answers, it answers by reading. It resolves a declaration to a normal form, compares forms, derives an order and issues a certificate, and none of those needs a substrate. Applying is where the boundary shows: the engine hands each step across it and the step does the acting.

Certification shows the division working. The certificate is computed on the near side, from the declaration alone. The audit trail is on the far side, written as things happen. What happened is not derivable from what was declared, and can only be recorded as it occurs.

Every question aidion answers is about a running system. Scheduling, health, durable execution, audit and the enforcement of authority on each request are of that kind, whether aidion answers them itself or through Nomad and Restate. None is answered by reading a declaration. They need a live service, durable state and a record of what happened.

Where daedal builds to aidion, the boundary between them is the delegation boundary of the calculus. daedal hands a resolved form across it and treats what lies beyond as an oracle, and aidion is then one substrate among the many daedal builds to.

Governance

Two registers

Governance in the composition has two registers. The constitutional register holds what the composition settles before the system runs. The operational register holds what only running produces, checked on each request. A property in the constitutional register is a property of the form, so it holds of every instance realised from that form. A property in the operational register holds of one run and is evidence about that run.

What the near side yields

Putting governance in the composition yields four things.

The certificate is a computed asset. A third party recomputes the digest of a normal form and every input digest under it. No credentials are needed and there is no authority to appeal to. Under that digest is each node's grant, what it requires, its immutable keys, the executor it runs under, its scaffold close and deadline, and its dependency edges. The reason each edge was drawn is kept for diagnostics and is not in the certificate. Alongside them are per-component digests of the source trees. So what a recomputation establishes is what was conferred on each part, what each part asked for, and the content of the thing that received it.

Conferred authority is a structural boundary, and it is positional rather than nominal. Authority attaches to where a component sits, not to anyone's identity, and the engine models no operator. A grant written in an imported subtree is refused at compile. A grant may not confer a command or a secret that the granting module was not itself granted, so authority narrows as it passes down a delegation chain and can never widen. A component that carries only content has nothing to declare a grant on, and one written there is refused. At run time the boundary is enforced under the container executor, where a step that has lost its control channel still cannot run an ungranted command, because the gate is checked before the command is built. Under the host executor the compile-time rules above still hold, and at run time the gate covers only the commands a step proxies.

Declarative provenance is a structural record. Every component is declared and versioned, and resolution produces the whole as one inspectable object. The composition is resolved and recorded before anything runs, so the record of what was applied falls out of the process rather than being assembled afterwards.

Irreversibility takes a distinct act. A replacement that would destroy data is refused unless an explicit obliterate flag is given, so the plan will not quietly turn into a deletion.

The obligations these bear on are real and specific. APRA's Prudential Standard CPS 230 commenced on 1 July 2025 and binds APRA-regulated entities. Paragraph 27 requires an entity to "identify and document the processes and resources needed to deliver critical operations, including people, technology, information, facilities and service providers, the interdependencies across them, and the associated risks, obligations, key data and controls". That account is wider than any software. It takes in people, facilities, service providers and obligations, none of which a composition holds. A resolved composition is one limb of it, the technology and the interdependencies across it, and what distinguishes that limb is that it is computed from the declaration rather than kept beside the system and reconciled to it by hand. The rest of the paragraph is not addressed here. Whether any of it is discharged is for an entity and its auditor to judge, and nothing here reports such a judgement.

Holding a change for a person

A step can stop and be picked up later. It returns a suspend result, the apply records the run as suspended and exits without error, and a later apply re-dispatches the step. So a change can be held pending something outside the system, a person's confirmation among them.

What the engine supplies is the pause and the resumption. Who is asked, how they are reached and what counts as an answer are the application's. The suspend result carries free-form detail, and nothing is scheduled, notified or tracked on the strength of it.

Questions

Does the delegation boundary remove non-determinism, or push it down the stack?

It locates it. The boundary says where the claims stop. The form is a function of the declared parts alone, so it is settled whatever the substrate turns out to be. The certificate is a digest of that form, so it recomputes whatever the substrate turns out to have done. That is why the result holds: resolving a declaration to its normal form is decidable, while the halting of what gets realised from it is not.

Is avoiding reflection practical, when parts need to know about the whole?

Most of the need is met without it. A part that needs its provider gets it by name, with neither part naming the other and the match made over the whole assembled set. A part that needs what its subtree offered gets it by kind, contributions fanning in attributed to the parts that emitted them. A part that needs to know what is running asks the registry of whatever operates it, aidion's where aidion does. One case is settled by naming rather than by derivation. A wiring that would depend on the finished form, such as binding to whichever provider nothing else uses, is declared by naming the provider, which puts the choice where it can be read.

What about drift, when the running system stops matching the declaration?

Two comparisons answer that, and they are made differently. The declaration is resolved afresh and diffed against the recorded baseline, which is deduced and not measured. The world is asked during the same plan, by the steps that own it, each reporting what it finds. The host and cluster steps written for the compositions this engine runs ask the unit whether it is serving and probe a release's declared health path. So a divergence between the declaration and the world is found by asking rather than by reading. Apply is then convergent, because every step runs and each step is idempotent against its input. The engine classifies the declaration, and it judges nothing about the world. Each step is handed its resolved input and decides for itself whether the world already matches it. The wiring is derived from the declaration, and what a step reports about a host is a finding about the host.

How is this different from declarative infrastructure as it is already practised?

Declarative input and a plan step are common. The normal form is proved independent of the order the parts were assembled in. The same declaration therefore gives the same form, and the form can be pinned rather than reproduced by convention. Composition is a cancellative partial commutative monoid, and its frame property is what carries a property established in a small composition into a larger one. Ambiguity is refused, so a requirement with two providers stops the composition. A third party with no credentials and no authority to appeal to recomputes the certificate and checks what produced a given result. Grants are refused from imported components, so a package cannot arrive carrying its own permissions. And the line between what reading settles and what it does not is placed by a theorem.

What does it add over module systems and the phase distinction?

The phase distinction already holds a static stratum decidable while the dynamic stratum it precedes is not, and module systems already compose by name. The decidable stratum is reached here as an entailment of three stated conditions. What it costs is stated: admit unbounded computation into the configuration stage and the entailment fails. The scope is a system's whole constitution.

What happens when an apply fails midway?

It stops, and what it did is recorded. The default is to drain the work in flight and halt, with a mode that continues independent branches and cuts off only what depended on the failure. A run that stops records a merged snapshot, so steps it touched carry new entries and untouched steps keep their prior ones. The next run continues from there rather than starting again.

What happens to a running instance when the form changes?

Plan settles it before anything runs. Each step is classified against its recorded baseline as unchanged, updated in place or replaced. A step declares which of its input keys are immutable. Changing one forces replacement rather than an update. A replacement that would destroy data is refused until the operator authorises it. Whether a change leaves an instance where it is or mints a new one is therefore read off the declaration rather than discovered during the apply.

The identity of the type is equality of normal forms. Two writings of one declaration normalise to one form, so a change that leaves the normal form unaltered is not a change to what the system is. Each token carries an identity of its own, conferred at realisation by the environment it is launched into. Which changes end one token and begin another is declared: the author marks the input keys that cannot change without replacement, and plan applies that mark. Constitution is the maker's.

What stops an imported component from widening its own authority?

A grant is conferred at scope level, so it comes from the composition that takes the package in and never from the package. An imported component can declare what it needs and cannot confer it on itself. What it needs is visible before it runs, because the engine unions the whole composition's requirements at every plan.

How does a system built this way govern an agent?

The application does, and neither tool does. How much latitude a model has is a property of the workflow that calls it, which a designer writes. Nothing in daedal or aidion enforces a separation between reasoning and acting, and nothing needs to.

What daedal contributes is that the decision is structural rather than conventional. The shape of the composition is readable off the declaration, and so is what each part may reach, and both hold of every instance realised from that form. A designer's choice shows up there, in how the parts are arranged and what each is permitted, rather than in a convention a reader has to be told about. So a reviewer reads the form instead of trusting a description of it, and the certificate says the form they read is the form that ran.

Structural means readable and binding. It does not mean adequate. Nothing tells a designer that a harness is tight enough for what it is doing, and a wide one is sometimes the right design: a research harness may want latitude where an approval path wants almost none. daedal makes the choice inspectable rather than making it.

Can a composition include people?

In the sense that a change can wait for one. A step returns a suspend result, the apply records the run as suspended and exits, and a later apply re-dispatches it. The engine supplies the pause and the resumption and nothing else: who is asked and how they are reached is the application's.

What does an author write?

Code, in a language they already write. A step is a program in Elixir, Go or Python run through its runner, or a shell script the engine runs directly. Either way the engine exchanges JSON with it over standard streams, sending the assembled input and receiving a structured result. Around that, a manifest declares what the part requires and what it provides, and the engine derives the wiring across the whole composition.

Nobody writes a normal form or reasons about commutativity. The engine does that, and what the laws change for an author is that assembly order stops mattering and an ambiguous requirement is refused. The engine reasons about structure and never reads inside what a step does. That is what keeps it independent of any substrate and of any domain.

What does this give a system that changes often?

Wiring settled in a small composition survives into a larger one, which is the frame property, so adding parts does not reopen what ⊕ has derived. Abstract binding is the exception: adding a nearer provider can re-rank a binding, so a certificate covers the whole as it stands and an extended whole needs a fresh one.

A team building this way reuses parts instead of rewriting them. A component is packaged with its whole subtree and imported by name. A sealed sub-composition is versioned on its own. And the shape of a system stays open to change: plan classifies every step against the declaration before anything runs, and refuses a replacement that would destroy data until the operator authorises it. What a change will do is settled before it is made.