Different jobs, explicit handoffs

No single screen or process is treated as the planner, permission giver, executor, observer, and judge.

The operational vocabulary these pages share, including occurrence, attempt, dispatch, settlement and indeterminate, is defined in the site glossary.

The contract

Contract

Automation may propose work — runbooks, scripts, Terraform plans, AI agents. Gates decide whether the proposal is admissible. Operators decide whether governed output is promoted.

Not approval

An agent saying “done.” Tests passing. A completed run. A green check. A demonstration succeeding.

Evidence

Every refusal names the gate, the failed predicate, the clock basis, and whether any effect occurred.

From proposal to review

Maude: author and check

Maude lets you edit a plan, check its structure and dependencies, compare revisions, and save a fixed snapshot. You can edit directly or review a proposed change. The current design demo uses deterministic sample proposals, not a live model. Accepting a change saves a new draft revision; check that revision again. A checked or locked plan grants no permission and proves no execution.

Constellation AG: decide and account for permission

Constellation AG checks current observations, the applicable mandate and policy, and the exact requested work. If the work is allowed, it records a one-use permission for that run. The contracts call the current mandate support standing; it is an input to the decision, not permission by itself.

Docket: keep custody of the attempt

Docket carries an authorized unit of work through its execution boundary and records the attempt and outcome. The executor and deployment environment still need their own carefully configured permission boundaries.

Docket's local execution-standing guide documents a bounded option for one exact run with a permission lifetime of no more than 300 seconds. Docket retains the permission snapshot it observed with that attempt's custody. Permission that is already revoked when Docket resolves it refuses; a later revocation does not rewrite a custody attempt that resolved successfully. Absent, expired, ambiguous, or mismatched permission state also refuses. Alpha.6 qualifies this surface only inside the named reviewed-local-copy/v1 composition; it is not Standing or a general authority service.

Nightshift: establish what needs attention now

Nightshift relates evidence over time. It can distinguish a current observation from an old one, and an observed condition from a missing answer. It does not turn old evidence into a fresh fact.

Phosphor: inspect without changing

Phosphor is the read-only inspector hosted with Constellation AG. It presents the joined record from the owning systems. Maude's separate design workspace can change a draft plan; navigating between the two does not merge their state or authority.

Trust and deployment boundaries

The contracts describe how responsibilities are divided; deployment must actually preserve that division. Service identities, filesystem access, executor configuration, database access, operator privileges, and access to a container daemon or its socket can bypass a software workflow if they are too broad. Docker-daemon access commonly permits broad host-level container, filesystem, and network changes. Constellation does not make those deployment privileges safe merely by recording a well-formed plan.

Operators should be able to tell which system owns each fact, which identity acted, what exact permission applied, and which evidence supports the displayed state. If an owner is unavailable or the evidence is incomplete, the interface should report absence or unknown rather than infer success.

What formal work does and does not establish

Linear Accountant's verification guide documents a Lean model for its arithmetic core and a Rust differential check. It does not prove Rust u64 behavior, persistence, deployment, or permission to act.

AG's formal-calculus crosswalk is an obligation map for a pinned Lean revision. It explicitly does not make a Lean theorem a runtime authority or prove that its Rust implementation is equivalent to the model.

Docket's trust model records the custody assumptions behind its recovery conclusions. Its invariant tags distinguish proved claims, doctrine that remains unproved, and implementation choices. Deployment evidence is still separate.

Staying within budget can still leave work unfinished

A task can spend no more than its allowance and still leave too little capacity to finish a mandatory obligation. Linear Accountant constrains execution spend; viability constrains the state execution is allowed to leave behind.

A bounded Lean model formalizes this distinction. For one additive resource, complete costs for the currently mandatory obligations, and no replenishment, spend + requiredReserve <= available is sufficient to leave those obligations affordable. Budget compliance and affordability of the current action alone are not sufficient (Resources.ObligationViability: budget_compliance_does_not_imply_viability, preserves_required_reserve_implies_viable).

This is a formalized bridge / invariant candidate. Linear Accountant's single-token consumption supplies the scalar subtraction behavior; the frozen OBLIGATION-VIABILITY-V0 experiment supplies bounded reserve and completion-viability behavior. The relationship is validated in those constituent semantics, not implemented as a cross-stack reserve controller.

Standing and action admission do not acquire a reserve check from this theorem. Current AG/Docket do not implement a live numeric obligation-cost, protected-reserve admission, or viability verdict. A future runtime guarantee needs an explicitly owned obligation-cost and protected-reserve admission rule. No new component or office is proposed here.

Baby River remains related resource and state-transition research, with separately bounded environment and measurement results. Neither it nor this scalar bridge proves observable viability or a sufficient renewal rate relative to state drift. Observable viability / indistinguishability and renewal-rate versus state-drift sufficiency remain deferred research notes, not current implementation work.

Read the governed recursive-improvement research note for a bounded design discussion of tactics, evidence, evaluation, reserves, and external amendment authority. It does not add a runtime composition or release commitment.

Future effects require a fresh decision

A past success, a settled occurrence, or a still-visible approval does not authorize the next effect. Before new work changes anything, the system needs fresh observations and the permission applicable to that specific transition. Reconciliation may inspect an existing uncertain attempt; it must not repeat the mechanics merely to obtain a tidier answer.

Adopting one piece

Nothing here asks you to replace Kubernetes, IAM, CI, schedulers, databases, or orchestration — and nothing asks for cryptographically verified timestamps on every action. Adoption begins at one transition whose consequences matter. The surrounding platform stays; the inserted component owns one narrow question, and refuses to silently inherit authority from the rest of the stack.

Pre-effect gate

Re-check, immediately before the effect, whether the evidence or standing that justified it is still usable. The earlier prototype shows the shape: checked valid, refused at exercise, nothing spent.

Receipt boundary

Wrap an existing executor so the premises, decision, exact attempted effect and outcome survive together. The current example is the alpha.6 Docket-custodied action; the older Git vertical remains a historical exhibit.

Read-only evaluator

Observe an existing system and classify what its evidence establishes, with no action authority to inherit. Current diagnostic source lives in Constellation NQ; the declared-deny probe is a classic-NQ historical specimen.

Governed effect custody

Carry one exact authorized attempt through execution and reconciliation while preserving uncertainty and refusing blind repetition. See Constellation Docket and the alpha.6 walkthrough.

These are the shapes the existing artifacts and exhibits actually demonstrate — different artifacts support different ones, and no artifact supports them all. The unit of adoption is not “the enterprise.” It is one consequential transition, one bounded claim, or one admitted effect class.

See what you can inspect today, or read the research directions behind these boundaries.