Actuating
Mission
Actuating is a counterexample-to-construction compiler, not a patch scheduler or a repair-classification service. Learn the cause from the witnesses; change what permits the family, not just what permits the reported example.
accepted Goal -> initial construction -> local proof
frozen reviewed candidate -> cumulative accepted counterexamples
-> causal explanation -> discriminating sibling predictions
-> law-preserving construction -> sanctioned-path migration
-> family exclusion + required-valid preservation -> adversarial review
For admitted behavior B' and the supported invalid family Phi, establish:
B' intersect Phi = empty
required-valid subset B'
every sanctioned path to trusted behavior crosses a law-preserving boundary
A checked constructor is not sufficient by its name. Its admission, ownership, transitions, lifetime, and bypass closure must make the law hold in the declared domain. Untrusted bytes may exist; acquiring trusted status must enforce the law.
Authority and fact ownership
| Fact | Owner |
|---|---|
| Required behavior, compatibility, scope, authorized effects | accepted source or current user authority; bound directly by Actuating |
| Realized construction and exact diff | Git commit and tree |
| Executed validation and proof | the exact repository-native verifier |
| Review attempt, target, verdict, and provenance | CAS |
| Finding authority, applicability, duplicates, and admitted witnesses | $review-fold and review-fold/counterexample-corpus |
| Causal explanation, candidate selection, realization, and closure | $actuating |
| Mechanism challenger / boundary nomination / redundant factors | $metanoetic / $universalist / $reduce, interpreted by Actuating |
| Public effects and readback | $ship and the provider |
Supporting skills do not grant mutation or closure. Actuating owns no Ledger transition gate and no durable workflow store. Review Fold's corpus remains immutable witness evidence; current families, applicability, and architecture are recompiled. A narrative, route label, or equality of agent-authored digests cannot certify the construction.
Public routes
| Intent | Route | Mutation | Terminal result |
|---|---|---|---|
Bare $actuating or /goal $actuating |
implement -> Ship -> review-closeout | Explicitly authorized | complete |
$actuating implement |
compile and realize locally | Explicitly authorized | local complete |
$actuating analyze |
deepest honest read-only construction judgment | Forbidden | construction, incomparability, containment, or obstruction |
$actuating review-closeout |
falsify, realize successors, Ship, converge | Explicitly authorized | complete |
An unqualified review, inspect, audit, classify, or analyze request selects
analyze. It may acquire evidence about an existing candidate but cannot mutate,
publish, grant closure credit, or claim completion. Mutation requires explicit
implement, fix, resolve, address, or closeout intent.
implement begins from the accepted Goal and exact Git state. It dispatches no
review and requires no review receipt, counterexample, or initial falsification
wave. Existing owner evidence may inform it without a fresh review campaign.
Initial architecture decisions follow the Goal; no revoked predecessor theorem
is required to design software that does not yet exist.
Review-bearing routes accept parallel-reviews (default) or serial-reviews.
These change scheduling only. They do not change authority or the review inventory.
Source binding
Derive the Goal directly from the current accepted specification or direct user instruction; read the exact source, not just a prior summary. Preserve required outcomes, non-goals, hard constraints, compatibility contracts, permitted breaks, and migration obligations. Bind repository, immutable base, and authorized path scope; an implementation or plan cannot silently broaden them.
Separate required deliverables and source-fixed architecture from preferences, examples, and proposed means. Do not promote a suggested mechanism into a law or demote an explicit requirement. Source binding records obligations; Actuating chooses source-permitted means. A plan, review, or prior implementation cannot broaden source authority.
Keep semantic requirements distinct from execution authority. Bind mutation, validation, publication, and review posture to the accepted source and selected route; permission to work neither authorizes every effect nor proves completion. For each required law, retain applicability and its deciding observation. If that observation cannot be identified or required authority is missing, block only the dependent action or claim; continue independent authorized work.
Before affected mutation, refresh these bindings when the source, authority,
scope, compatibility, or required observations change. Have $review-fold
reclassify all available applicable findings and failures against the refreshed
Goal; preserve unresolved evidence and original provenance rather than erasing it
or inventing continuity. Existing review-epoch and proof-invalidation rules apply.
Reuse an adequate binding in the Working Set and existing downstream owner formats. No separate skill invocation, mandatory Goal Contract packet, durable record, or new identity is required. A summary or digest never replaces the source or proves completion.
Observe and adjudicate
At entry and after material change, bind the Goal, immutable base, exact head, current construction, proof inventory, and any publication state. Read the relevant source, not a remembered architecture. Unknown evidence receives no credit.
Before accepting validation for local completion or reviewability, inspect the base-to-candidate diff and actual check selection for deleted tests, weakened assertions, skipped checks, or reduced coverage, including changes made directly by Actuating. Map each affected check to its source-backed obligation; require preserved or stronger proof, a source-grounded oracle correction with independent evidence, or explicit authority retiring the obligation. A passing weakened suite cannot discharge an unchanged requirement. Keep unexplained proof loss unresolved and block only dependent completion or reviewability. Reuse the existing proof inventory; no separate critic, packet, or review stage.
Before counterexample-driven selection, reconcile relevant CAS, provider/PR, test, incident, migration, compatibility, verifier, and corpus evidence. Each live source is folded, proven non-current, or explicitly unavailable. An omitted live finding keeps the cut open; an unavailable source makes the affected horizon incomplete, not clean. Missing evidence blocks only claims or actions that depend on it; do not make provider availability a prerequisite for initial implementation.
Have $review-fold project the corpus, preserve original subjects, re-evaluate
current applicability, and classify proposed laws:
entailed current witness may create correctness pressure
strengthening non-blocking follow-up unless accepted authority adopts it
preference reject as a current correctness liability
new-requirement reopen Goal authority
underdetermined seek authority; no correctness mutation from the claim
Have Review Fold apply its counterexample admission for review findings and failed checks before treating either as a liability. A failed execution stays failed; its diagnosis is adjudicated, not its history. A discrepancy may expose a defect in the implementation, the witness's interpretation, an oracle, or a proof/assessment claim. Establish which obligation actually fails; do not default to changing production code or to trusting the checker. A refuted allegation returns to Review Fold; an oracle correction needs its own source-grounded obligation and independent evidence, never changed expectations merely to agree with the candidate. Unresolved premises justify authorized investigation, not an invented repair. Acceptance of a witness proves neither the proposed fix nor its claimed causal family.
Only current accepted witnesses authorize counterexample response. Duplicate
observations add provenance, not independent failures. Historical absence cannot
prove first occurrence, disjointness, or elimination under an incomplete horizon.
Review Fold captures newly accepted independent witnesses only with enclosing
corpus-write authority. Pass corpus_write_authorized on every handoff: true when
that effect is authorized; corpus_write_authorized: false for analyze or absent
authority. Read-only analysis may project and adjudicate available evidence but
never writes repository/source-memory stores or provisions tools for capture.
Other routes inherit their actual effect scope; supporting skills cannot expand it.
Actuating neither copies the corpus nor persists its current interpretation.
A rejected strengthening must not enter code to placate a reviewer or protect a clean streak. Reopen authority or remove it. Correcting an unsupported public overclaim may follow an existing truthfulness obligation; weakening an accepted requirement, compatibility promise, or release posture needs explicit authority.
Review-epoch immutability and evidence acquisition
Read review-contract.md. A review epoch opens on
the first CAS request against an exact locally proved reviewable head. While
open, freeze that subject and forbid successor mutation.
A material current entailed finding invalidates the candidate and all review credit immediately. It does not request a patch. Complete the initial six-lens wave against the frozen head: parallel siblings are non-cancelling; serial mode continues remaining initial lenses for evidence only. Required request-local recovery is part of the barrier. Fold the complete cut before closing the epoch.
A material later standard-confirmation finding stops further confirmations. Fold it and already-live required owner observations; do not launch another auxiliary wave on the invalidated head. A clean epoch closes after convergence. Outside an open review epoch, review is not a prerequisite for implementation.
Compile the first loss of guarantee
Combine current and applicable historical witnesses under the accepted law. Acceptance establishes a supported disagreement, not the causal explanation. Keep the law fixed while challenging the account: which assumption makes this witness surprising? Locate the first loss of guarantee and what can be chosen, written, ordered, interpreted, or authorized independently that must agree. The family remains a hypothesis, not its observed examples; keep distinct laws separate.
Before implementation, choose the smallest source-grounded discriminator that could refute that explanation, not merely repeat the failing example. When a semantic model is implicated, seek a supported case separating notions it conflates or a dependency the law does not require. If the model treats two cases alike but the law requires different observations, retain or derive the missing distinction; more checks on the unchanged proxy cannot recover it. A decisive source argument can suffice; no paired-case quota or forced redesign.
Distinguish a wrong model from omitted enforcement. Correcting a predicate does not prove every path uses it; applying it everywhere does not prove it expresses the law. For lifetime, aliasing, or composition, exercise permitted transitions from valid state and preserve required-valid counterparts. When source evidence identifies a shared obligation, ask whether an operation can omit or reinterpret it independently. Prefer making that omission unavailable over teaching each branch to remember another check. Preserve legitimate operation differences; a helper, exhaustive switch, or new type alone proves neither meaning nor coverage.
Compare adequate candidates under the same laws, observations, compatibility, resources, and proof bar. Remove, derive, or lawfully control the enabling freedom; retire redundant production interpretations without merging away independent verification. Test a plausible deletion, delegation, collapse, or replacement when redundancy is implicated, not two complete versions or a deletion quota. A local correction or shared validator can be adequate when admission, permitted operations, and sanctioned paths establish the law. Neither local-repair-first nor redesign is compulsory. Prefer stronger exclusion and fewer independently maintained truths; source size and lifecycle cost cannot justify weaker guarantees.
Use the construction argument when domain, operation, or migration coverage needs it. Samples discriminate an explanation; they do not prove an open-domain exclusion.
Architecture compilation
At a live boundary decision, use $first-principles with the cumulative evidence
to separate accepted obligations from inherited means. Reuse adequate derivations;
source-fixed outcomes remain binding even when not derived from technical premises.
No pre-mutation theorem-identity certificate is needed to reconsider a mechanism.
When the existing Metanoetic trigger fires, read both skills and apply $glaze
then $metanoetic verbatim in the same bounded challenger pass, before $universalist.
Run once per unchanged decision surface; reuse an already consumed challenger rather
than adding a pass. The incumbent may be the construction, causal explanation,
oracle/proof interpretation, or assessment of progress. Let the pass discover which
premises and evidence need reinspection; do not confine it to selecting a different
patch. A code rewrite or live architecture change is not a prerequisite for challenging
a suspect model. Keep the accepted Goal fixed. Supplied boundaries must be
preserved, made irrelevant by mechanism change, or requires new authority;
required observations, compatibility, effects, host capabilities, and authorized
resource ceilings still govern selection. Supply the resource account in the existing
decision: justify feasibility against those ceilings using applicable evidence or
a concrete bound; leave unestablished feasibility unresolved. Reuse evidence only
while its subject and assumptions remain applicable; add no separate report or
benchmark stage. Incumbent representations and lifecycle burdens are evidence, not
immutable constraints. Retaining a sound construction or
refuting an allegation can be the right outcome. Actuating adjudicates the result.
Encouragement changes neither admissibility nor the proof bar. Add no separate Glaze
report or adjudication stage, and no mandatory second review of the review.
Only when architecture is live, give $universalist one independently governed
axis, one typed hole, and source-derived domain evidence. Require candidate,
preserve-incumbent, unresolved, or obstructed with a compact code-bound argument,
its discriminator, and material migration/residual consequences. Missing evidence
or incomparable adequate candidates remain unresolved, not an invented obstruction
or arbitrary winner. Split independent seams and prove their composition.
Universalist nominates; Actuating selects and proves.
Choose the exact-head verifier before implementation and realize the mechanism,
migrations, and retirements together under the common proof obligations. Use $reduce
only for material retirement or smaller-construction challenges, not another audit.
An adopted change to an owner, representation, interpretation, or proof updates the
affected obligations regardless of its label. Native evidence may discharge coverage;
use explicit topology only where route or migration accounting requires it.
Realization and common proof obligations
There is one operation: realize the selected successor. Selection states an intended mechanism and falsifier; acceptance requires the actual exact-head code. Local experiments may occur only with mutation authority and outside an open review epoch. They are not reviewable, publishable as complete, or proof by intent.
Every correction, regardless of its eventual descriptive label, must establish:
current witness addressed and required-valid behavior preserved
supported causal family covered at the declared claim strength
preselected sibling/domain discriminator executed, or explicit limitation
all relevant sanctioned producers, consumers, transitions, and bypasses accounted for
admission and permitted operations enforce the required law in the declared domain
proof authority, inputs, domain, and public claim agree
all correctness-bearing Git changes have accepted authority
displaced primary compensators retired or justified by distinct obligations
complete Goal-required proof inventory on the exact candidate
For an invariant-style safety law, establish valid admission, preservation under permitted operations, implication of the law, and closure of sanctioned escapes. Cut coverage proves passage through an owner, not preservation afterward. Account for aliases, lifetime, interleavings, and externally visible effects when implicated; transient invalidity must not escape its owning transition. Required progress and trace behavior need their own arguments; disabling all operations is not success.
Prove every applicable changed-boundary obligation using the strongest adequate repository-native evidence. A closed construction/operation surface can establish coverage directly; an opaque type name or passing build alone cannot. Where route or migration coverage remains unestablished, use the source-derived topology proof in counterexample-guided-normalization.md. Never derive the verification domain solely from the candidate's asserted list. New unaccounted sanctioned paths invalidate coverage under either representation.
For finite domains, complete claims need exhaustive coverage or a justified construction proof. For open domains, they need a justified generator and preservation argument. Samples, sibling tests, and clean reviews are falsification evidence, not universal proof. Otherwise report the explicit bounded domain and residuals; never silently turn containment into elimination or weaken required behavior to obtain a green result.
isolated-restoration and construction-normalization may describe the actual
delta afterward. They are not pre-mutation certificates or different proof bars.
A changed owner, cut, carrier, interpretation, topology authority, proof universe,
or claim strength cannot be hidden in a batch labeled restoration. A public claim
correction retains its own authority and closure consequence. Unknown evidence
means investigate or block the affected claim, not invent a digest or a rewrite.
Recurrence and progress
Read post-elimination-falsification.md.
An exact current entailed same-claim witness revokes the exclusion claim. Reopen
the causal explanation and replay its applicable history before selecting the
successor. Source-domain omissions and authority failures cannot be dismissed as
missing assertions. Same broad law or owner alone does not establish recurrence.
A new head, route label, or family name does not erase contrary evidence.
Judge progress by the supported failure mechanism excluded, required-valid behavior preserved, sanctioned paths covered, and independently maintained truths retired. Learning that an explanation or oracle was wrong is useful without itself proving the code better. More findings can be valuable discovery; fewer findings, shorter runs, smaller diffs, and clean streaks do not by themselves establish efficacy. Use the existing offline comparison to assess additions and ablations, not a new review lane, runtime score, or store.
Construction Working Set
Keep the current Goal/head, admitted witnesses and source horizon, causal mechanism and discriminator, source-derived domain, actual proof, migrations, retirements, residuals, and unresolved work in the active thread or accepted implementation specification. Reuse owner evidence rather than re-expressing it in another packet. These are working facts, not a report template or durable Actuating store. Surface only material decisions and limitations; preserve historical witness provenance.
Review and closure
The initial inventory remains standard, soundness-skeptic, footgun-finder, invariant-ace, complexity-mitigator, and fresh-eyes. Standard is Codex's native review with no custom Actuating instruction file or argument. Auxiliaries retain their checked-in lenses; none substitutes for standard.
Only a completely realized, locally proved candidate is reviewable. Require
five consecutive distinct native/default standard cleans on one unchanged head;
the initial standard counts as one and the next four run serially. All five
auxiliary outcomes must also be terminal and adjudicated. A material finding or
head change resets all credit. Reviews falsify; they do not prove soundness by
failing to find a bug.
Read closure.md. implement ends at local completion;
publication and convergence belong to bare Actuating and review-closeout.
Closure requires exact Git, verifier, CAS, and Ship/provider facts as applicable.
An unresolved accepted liability, unauthorized strengthening, missing required
proof, or unowned residual cannot become unqualified complete. Complete the
object-level task before optional learning or memory capture.