Governing a coding agent

Your coding agent — Claude Code, Codex, pi, a harness of your own — proposes a patch and asks to merge it. Today the answer comes from a permission prompt, a prefix rule, or increasingly a model classifier. None of those can see the repository's state, and none of them produces a reason you could show a release manager. This page builds the alternative: a 28-term change gate the harness consults before it acts, where the decision is derived by rules over typed facts and the bot cannot grant itself merge permission.

Why prompt-level policy is not enough

The research wiki's survey of harnesses (research/neurosymbolic-landscape/coding-agent-harnesses.md, 2026-09-02) finds the same shape everywhere:

• Policies cannot see state. Codex rules "evaluate command prefixes only — they cannot reference repository state, file contents, or environmental conditions." Gemini CLI's policy engine predicates over tool name, argument patterns and annotations only.
• The approval step is going neural. Codex auto_review, Claude Code auto mode, and Cursor Auto-review put a classifier inside the decision; Cursor calls its run modes "best-effort guardrails rather than a hard security boundary."
• Patch application has no base identity. No core harness checks a base hash before applying an edit; the one tool-local attempt "silently returns success when anchors are stale," and Claude Code shipped a fix for file tools following a symlink swapped after the permission check — a time-of-check/time-of-use gap between authorization and effect.
• The failures happen below the prompt. After PocketOS lost production data and its backups to a blanket-scope token, the post-mortem read: "Guardrails must be implemented at the API gateway and token-permission level, not in advisory text."

The same survey finds that no harness "declares a semantic domain graph with verified cross-tool preconditions/effects or maintains a fixed point over repository state" — and that every harness already exposes the slot such a thing would plug into: a typed, ordered permission decision with a reason string (PreToolUse hooks in Claude Code, BeforeTool in Gemini CLI, beforeShellExecution in Cursor, an MCP proxy for everything else).

The 28-term change gate

Eight classes and enumeration members, nine properties, eleven rules. The harness asserts what it observed about a proposal; the rules — and only the rules — assign :gateDecision. It runs today against the shipped engine.

# The change-gate overlay: a 28-term capability fragment that decides whether
# a coding agent's change proposal may land. The harness (or, today, your
# glue code) asserts what it observed about the proposal; the rules below —
# and only the rules — assign :gateDecision. The bot cannot grant itself merge
# permission: :gateDecision is horis:assignedBy horis:RulesOnly, so the gate
# refuses the value from every provenance except a rule.
#
# Runs today against the shipped engine (docs/framework/02-ontology.md,
# 03-world.md, 04-reasoning.md). The workflow/tool half — the candidate-
# artifact envelope, sandboxed checks, adapter-mediated commit — is PRP-008's
# (docs/framework/07-tools.md § The candidate-artifact boundary).

@prefix :      <https://example.org/change-gate#> .
@prefix horis: <https://w3id.org/horismos#> .
@prefix rdf:   <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs:  <http://www.w3.org/2000/01/rdf-schema#> .
@prefix xsd:   <http://www.w3.org/2001/XMLSchema#> .

## Domain (doc 02) — 8 classes and enumeration members

:ChangeProposal a rdfs:Class ;
    rdfs:label "Change proposal" ;
    rdfs:comment "One candidate patch/PR the harness materialized as facts." .

:Proposer a rdfs:Class ;
    horis:oneOf ( :Bot :Human ) .

:GateDecision a rdfs:Class ;
    horis:oneOf ( :Approved :NeedsHuman :Rejected ) .

## Observed facts (doc 02) — 8 properties the harness asserts

:proposedBy a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range :Proposer ;
    horis:cardinality "1" .

:targetBranch a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:string ;
    horis:cardinality "0..1" .

:baseMatchesHead a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:boolean ;
    rdfs:comment "The proposal's recorded base hash equals the branch head at check time." ;
    horis:cardinality "0..1" .

:testsPassed a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:boolean ;
    horis:cardinality "0..1" .

:lintPassed a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:boolean ;
    horis:cardinality "0..1" .

:touchesProtectedPath a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:boolean ;
    rdfs:comment "Any changed path matches the repo's protected set (CI config, release scripts, policy files)." ;
    horis:cardinality "0..1" .

:linesChanged a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:integer ;
    horis:min 0 ;
    horis:cardinality "0..1" .

:humanApprovals a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range xsd:integer ;
    horis:min 0 ;
    horis:cardinality "0..1" .

## The decision (doc 02) — 1 property no model, tool, or API caller may set

:gateDecision a rdf:Property ;
    rdfs:domain :ChangeProposal ; rdfs:range :GateDecision ;
    horis:cardinality "0..1" ;
    horis:assignedBy horis:RulesOnly .   # the bot cannot grant itself merge permission

## Rules (doc 04) — 11 rules. No two rules that conclude *different* values can match
## the same proposal: PRP-005's conflict check named four such pairs that priority had
## been resolving silently, and the two specific NeedsHuman rules now require green
## checks explicitly. Rules that agree may still overlap (both reject rules, both
## approve rules, a bot diff over 400 lines that also touches a protected path); the
## outcome is the same either way, but the proof cites whichever agreeing rule fired
## last, i.e. the lowest priority (PRPs/PRP-002-reasoning-substrate/02-tasks-and-gaps.md,
## 2026-09-05). The completeness covers at the end therefore each fill exactly one
## reported region and overlap no other rule, so a cover never takes a specific rule's
## explanation away.

:rejectStaleBase a horis:Rule ;
    horis:priority 100 ;
    horis:when [
        horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is false
    ] ;
    horis:then [ horis:property :gateDecision ; horis:value :Rejected ] ;
    horis:explain "Base hash no longer matches the branch head — the proposal was authored against stale state" .

:rejectFailingChecks a horis:Rule ;
    horis:priority 90 ;
    horis:when [
        horis:any (
            [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is false ]
            [ horis:subject :ChangeProposal ; horis:property :lintPassed  ; horis:is false ]
        )
    ] ;
    horis:then [ horis:property :gateDecision ; horis:value :Rejected ] ;
    horis:explain "A required check failed in the sandbox" .

:protectedNeedsHuman a horis:Rule ;
    horis:priority 50 ;
    horis:when [
        horis:all (
            [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :touchesProtectedPath ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:below 1 ]
        )
    ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "Protected paths need at least one human approval" .

:largeBotDiffNeedsHuman a horis:Rule ;
    horis:priority 40 ;
    horis:when [
        horis:all (
            [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :proposedBy ; horis:is :Bot ]
            [ horis:subject :ChangeProposal ; horis:property :linesChanged ; horis:exceeds 400 ]
            [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:below 1 ]
        )
    ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "A bot-authored change over 400 lines needs a human reviewer" .

:approveRoutineChange a horis:Rule ;
    horis:priority 10 ;
    horis:when [
        horis:all (
            [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :touchesProtectedPath ; horis:is false ]
            [ horis:subject :ChangeProposal ; horis:property :linesChanged ; horis:atMost 400 ]
        )
    ] ;
    horis:then [ horis:property :gateDecision ; horis:value :Approved ] ;
    horis:explain "Fresh base, green checks, no protected paths, small diff — routine change" .

:approveReviewedChange a horis:Rule ;
    horis:priority 20 ;
    horis:when [
        horis:all (
            [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
            [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:atLeast 1 ]
        )
    ] ;
    horis:then [ horis:property :gateDecision ; horis:value :Approved ] ;
    horis:explain "Fresh base, green checks, and a human approved it" .

# PRP-005 completeness-cover:start
# PRP-005's completeness check found that the six rules above decide nothing at all
# for a proposal whose evidence is incomplete. Both approve rules need
# `baseMatchesHead`, `testsPassed` and `lintPassed` to be *true*; both reject rules
# need one of them to be *false*; and a condition over an unassigned property is
# false (doc 02). A proposal whose checks never reported therefore matched no rule.
#
# The default is :NeedsHuman in every such region. There is no evidence of failure,
# so :Rejected would be wrong — and, more importantly, no evidence of success, so
# :Approved is never reachable from missing data. A gate that cannot see a check
# result asks a person; it does not guess.
:unrecordedCheckNeedsHuman a horis:Rule ;
    horis:priority 30 ;
    horis:when [ horis:all (
        [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:isNot false ]
        [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:isNot false ]
        [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:isNot false ]
        [ horis:any (
            [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:isEmpty true ]
            [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:isEmpty true ]
            [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:isEmpty true ]
        ) ]
    ) ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "A required check never reported — the gate cannot approve on evidence it does not have" .

# Checks are green and no approval is on record, yet the proposal fits neither approve
# rule and neither specific NeedsHuman rule. Each region below is one real situation
# with its own reason. Together they are disjoint from every rule above and from each
# other, so the proof always names the observation that is actually missing.

# The approval count itself was never recorded, and the change is not a routine one.
# Neither specific rule matches here: both need `humanApprovals below 1`, which is
# false on an unrecorded count.
:approvalCountUnrecordedNeedsHuman a horis:Rule ;
    horis:priority 30 ;
    horis:when [ horis:all (
        [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:isEmpty true ]
        [ horis:any (
            [ horis:none ( [ horis:subject :ChangeProposal ; horis:property :touchesProtectedPath ; horis:is false ] ) ]
            [ horis:none ( [ horis:subject :ChangeProposal ; horis:property :linesChanged ; horis:atMost 400 ] ) ]
        ) ]
    ) ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "Green checks, but the approval count was never recorded and the change is outside the routine envelope — a reviewer is required" .

# Whether the change touches a protected path was never recorded. A bot-authored diff
# over 400 lines is excluded so that :largeBotDiffNeedsHuman keeps that case.
:protectedPathStatusUnrecordedNeedsHuman a horis:Rule ;
    horis:priority 30 ;
    horis:when [ horis:all (
        [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:below 1 ]
        [ horis:subject :ChangeProposal ; horis:property :touchesProtectedPath ; horis:isEmpty true ]
        [ horis:any (
            [ horis:subject :ChangeProposal ; horis:property :proposedBy ; horis:is :Human ]
            [ horis:none ( [ horis:subject :ChangeProposal ; horis:property :linesChanged ; horis:exceeds 400 ] ) ]
        ) ]
    ) ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "Green checks and no human approval, but whether the change touches a protected path was never recorded — a reviewer is required" .

# No protected paths, but the diff size was never recorded, so the routine envelope
# cannot be confirmed.
:diffSizeUnrecordedNeedsHuman a horis:Rule ;
    horis:priority 30 ;
    horis:when [ horis:all (
        [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:below 1 ]
        [ horis:subject :ChangeProposal ; horis:property :touchesProtectedPath ; horis:is false ]
        [ horis:subject :ChangeProposal ; horis:property :linesChanged ; horis:isEmpty true ]
    ) ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "Green checks and no protected paths, but the diff size was never recorded — a reviewer is required" .

# A human-authored change over 400 lines with no approval on record.
# :largeBotDiffNeedsHuman deliberately covers only bot-authored diffs.
:largeHumanDiffNeedsHuman a horis:Rule ;
    horis:priority 30 ;
    horis:when [ horis:all (
        [ horis:subject :ChangeProposal ; horis:property :baseMatchesHead ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :testsPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :lintPassed ; horis:is true ]
        [ horis:subject :ChangeProposal ; horis:property :humanApprovals ; horis:below 1 ]
        [ horis:subject :ChangeProposal ; horis:property :touchesProtectedPath ; horis:is false ]
        [ horis:subject :ChangeProposal ; horis:property :linesChanged ; horis:exceeds 400 ]
        [ horis:subject :ChangeProposal ; horis:property :proposedBy ; horis:is :Human ]
    ) ] ;
    horis:then [ horis:property :gateDecision ; horis:value :NeedsHuman ] ;
    horis:explain "A human-authored change over 400 lines still needs a second person to approve it" .
# PRP-005 completeness-cover:end

Two lines carry most of the weight. horis:assignedBy horis:RulesOnly on :gateDecision means the gate refuses that property from every provenance except a rule firing. And horis:cardinality "1" on :proposedBy means a proposal with no declared proposer is not a proposal.

Run it

from horismos import HorismosValidationError, Ontology, World

onto = Ontology.load("examples/change-gate/change-gate.ttl")
world = World(onto)

def gate(subject: str, **observed: object) -> None:
    ref = world.assert_(":ChangeProposal", subject=subject, **observed)
    proof = world.explain(ref, ":gateDecision")
    print(proof.render() if proof else f"{subject}: no rule fired — no decision")

# A routine bot change: fresh base, green checks, small diff, no protected paths.
gate(":pr-41", proposed_by=":Bot", target_branch="main",
     base_matches_head=True, tests_passed=True, lint_passed=True,
     touches_protected_path=False, lines_changed=112, human_approvals=0)

:gateDecision = :Approved   via approveRoutineChange — "Fresh base, green checks, no protected paths, small diff — routine change"
  ├─ baseMatchesHead true is true   (asserted by the api)
  ├─ testsPassed true is true   (asserted by the api)
  ├─ lintPassed true is true   (asserted by the api)
  ├─ touchesProtectedPath false is false   (asserted by the api)
  └─ linesChanged 112 atMost 400   (asserted by the api)

That proof is the reason string your harness hook returns. Now the cases that matter.

A protected path with no human approval pends rather than merges:

gate(":pr-42", proposed_by=":Bot",
     base_matches_head=True, tests_passed=True, lint_passed=True,
     touches_protected_path=True, lines_changed=30, human_approvals=0)

:gateDecision = :NeedsHuman   via protectedNeedsHuman — "Protected paths need at least one human approval"
  ├─ baseMatchesHead true is true   (asserted by the api)
  ├─ testsPassed true is true   (asserted by the api)
  ├─ lintPassed true is true   (asserted by the api)
  ├─ touchesProtectedPath true is true   (asserted by the api)
  └─ humanApprovals 0 below 1   (asserted by the api)

A stale base is rejected even with everything else green — the highest-priority rule wins, and the proof names the clause:

gate(":pr-43", proposed_by=":Bot",
     base_matches_head=False, tests_passed=True, lint_passed=True,
     touches_protected_path=False, lines_changed=10, human_approvals=0)

:gateDecision = :Rejected   via rejectStaleBase — "Base hash no longer matches the branch head — the proposal was authored against stale state"
  └─ baseMatchesHead false is false   (asserted by the api)

The bot cannot approve itself. A model, a tool, or any API caller trying to write the decision is refused at the gate, in domain terms:

try:
    world.assert_(":ChangeProposal", subject=":pr-44",
                  proposed_by=":Bot", gate_decision=":Approved")
except HorismosValidationError as e:
    print(f"[{e.constraint}] {e}")

[provenance_refused] gateDecision may only be assigned by rules (horis:assignedBy horis:RulesOnly); assertion came from the api

Decisions track the facts. A large bot diff needs a human; when a human approves, the decision is re-derived; when the base drifts under it, the approval is withdrawn — all in the transaction that changed the fact, never a stale approval left standing:

gate(":pr-45", proposed_by=":Bot",
     base_matches_head=True, tests_passed=True, lint_passed=True,
     touches_protected_path=False, lines_changed=900, human_approvals=0)
gate(":pr-45", human_approvals=1)             # a reviewer approves
gate(":pr-45", base_matches_head=False)       # main moved; the hash no longer matches

:gateDecision = :NeedsHuman   via largeBotDiffNeedsHuman — "A bot-authored change over 400 lines needs a human reviewer"
  ├─ baseMatchesHead true is true   (asserted by the api)
  ├─ testsPassed true is true   (asserted by the api)
  ├─ lintPassed true is true   (asserted by the api)
  ├─ proposedBy :Bot is :Bot   (asserted by the api)
  ├─ linesChanged 900 exceeds 400   (asserted by the api)
  └─ humanApprovals 0 below 1   (asserted by the api)

:gateDecision = :Approved   via approveReviewedChange — "Fresh base, green checks, and a human approved it"
  ├─ baseMatchesHead true is true   (asserted by the api)
  ├─ testsPassed true is true   (asserted by the api)
  ├─ lintPassed true is true   (asserted by the api)
  └─ humanApprovals 1 atLeast 1   (asserted by the api)

:gateDecision = :Rejected   via rejectStaleBase — "Base hash no longer matches the branch head — the proposal was authored against stale state"
  └─ baseMatchesHead false is false   (asserted by the api)

Missing facts never produce a default approval — and they no longer produce silence either. An earlier draft of this gate left a proposal the harness could not fully observe with no :gateDecision at all, and relied on the caller to read that absence as stop. verify()'s completeness check reported the region, and closing it required a rule: :unrecordedCheckNeedsHuman derives an explicit :NeedsHuman whose proof names the checks that never reported, while :Approved stays unreachable from missing evidence. A workflow routes that decision to a person on a stated reason, not on a value that failed to arrive:

gate(":pr-46", proposed_by=":Human")
print(world.query(":ChangeProposal", gate_decision=":Approved"))

:gateDecision = :NeedsHuman   via unrecordedCheckNeedsHuman — "A required check never reported — the gate cannot approve on evidence it does not have"
  ├─ baseMatchesHead isNot false   (closed world)
  ├─ testsPassed isNot false   (closed world)
  ├─ lintPassed isNot false   (closed world)
  └─ any of:
     ├─ baseMatchesHead isEmpty   (closed world)
     ├─ testsPassed isEmpty   (closed world)
     └─ lintPassed isEmpty   (closed world)

[Ref(:pr-41)]

Only :pr-41 is approved. :pr-45 left the approved set in the transaction that recorded the base drift — there was no window in which a stale approval stood. (The test suite pins exactly this sequence: python/tests/test_devdocs_snippets.py.)

Read the proof, not the transcript

Every one of these outcomes is a proof tree with the rule's own horis:explain sentence at the root and the observed facts at the leaves. That is the artifact you attach to the merge, the artifact compliance asks for, and the artifact a later verification pass reasons about.

Where it plugs into your harness

The gate is a pure function of observed facts, so it sits wherever your harness lets deterministic code run before a model or a human sees the request:

Harness	Attach point (from the harness's own docs, per the research survey)	The fragment's job there
Claude Code	A PreToolUse hook (command or http handler) returning permissionDecision + permissionDecisionReason; declared per skill in SKILL.md frontmatter hooks	Materialize the proposal's facts, run the gate, return the proof as the reason; run before auto mode's classifier, not instead of it
Gemini CLI	A BeforeTool hook; policy rules can match toolAnnotations	Same — the policy engine keeps its precedence, the fragment supplies the state-aware decision
Cursor	beforeShellExecution / preToolUse hooks with permission: allow \| deny \| ask	Same; set failClosed: true — Cursor's hooks fail open by default
Codex, pi, anything over MCP	An MCP proxy or pi.on("tool_call", …) extension	The deterministic control the MCP maintainers themselves recommend over trusting tool annotations

A sketch of the Claude Code shape, so the mechanics are concrete:

A PreToolUse hook — sketch, not shipped code; check your harness's hook contract

import json, sys
from horismos import Ontology, World

event = json.load(sys.stdin)                          # the tool call the harness is about to make
facts = observe(event)                                # YOUR deterministic code: base hash, test status, paths…

world = World(Ontology.load("change-gate.ttl"))
ref = world.assert_(":ChangeProposal", subject=":this", **facts)
decision = world.value(ref, ":gateDecision")
proof = world.explain(ref, ":gateDecision")

verdict = {None: "ask", ":Approved": "allow", ":NeedsHuman": "ask", ":Rejected": "deny"}
print(json.dumps({"hookSpecificOutput": {
    "hookEventName": "PreToolUse",
    "permissionDecision": verdict[decision.curie if decision else None],
    "permissionDecisionReason": proof.render() if proof else "no rule fired — needs a human",
}}))

observe() is deliberately yours: computing baseMatchesHead is a hash comparison, testsPassed is a sandbox result, touchesProtectedPath is a glob match. Horismos does not do arithmetic or run your tests; it decides what the results imply and proves it. Turning those observations into a versioned, all-or-nothing snapshot with a conditional commit is what the coding-harness adapter in PRP-008 formalizes.

Skills as capability fragments

A SKILL.md today declares when to use a skill and which tools it may call. What it cannot declare is a precondition over world state, a bound on observable effect, or a proof. The framework's name for that missing piece is a Capability Fragment: a small ontology overlay attached to an existing skill or tool that proves when the capability is eligible, constrains its effect, and emits a proof — without replacing the harness's own state, sandbox, or approval machinery.

The change gate above is a capability fragment written by hand. The authoring agent's compiler mode (PRP-007) is meant to derive one from an existing SKILL.md, tool JSON Schema, or AGENTS.md: lift the machine-readable structure deterministically, let a model propose only the prose-derived conditions, verify, and emit a formalization coverage report that says which clauses became checkable constraints, which are test-backed, and which remain prose. See Authoring.

The candidate-artifact boundary

A coding agent necessarily generates novel text — patches, files, commands. That does not fit an ordinary ActionStep, whose arguments are read from the graph, and pretending it does would weaken neural proposes, symbolic decides by stealth. The framework's honest extension is the candidate-artifact boundary (LLM Boundaries, Tools):

1. Model output is a typed proposal envelope — patch, file, or command — never a tool argument.
2. Deterministic policy validates target paths, base hashes, syntax, and permissions.
3. A sandbox executes the declared checks.
4. Only then does a symbolic authorization step — the change gate above — permit application.

What the boundary proves: the proposal was policy-legal and passed its declared checks. What it does not and cannot prove: that the code is semantically correct. That stays a review and test claim, and the framework says so wherever the boundary is described.

Built today, landing next — honestly

Piece	Status
Typed proposal facts, RulesOnly decision, proofs, truth maintenance, the gate refusing self-approval	Runs today — everything on this page executed against the shipped engine
Workflow around it (ReasoningStep with onUnreachable → human, ActionStep firing a merge tool with a validated effect)	Declared vocabulary and Rust interpreter exist today (make demo runs the triage workflow); a change-gate workflow is a Turtle exercise, not new engine work
Base-hash check, sandbox execution, and the proposal envelope as a first-class typed boundary	Landing in PRP-008 (host-adapter/runtime side) — the envelope's horis: vocabulary is minted jointly with PRP-007
A coding-harness adapter that materializes repository state (branch, dirty files, test status, path scopes) as a versioned projection with conditional commit	Landing in PRP-008 — the second-domain proof that the host SPI is format-neutral, not FHIR-shaped
Compiling a fragment from an existing SKILL.md / tool schema, with a coverage report	Planned in PRP-007 (after PRP-008)
Completeness / conflict / dead-rule verification of the eleven rules, with domain-term witnesses	Yes — verify() proves :gateDecision total and conflict-free; Ontology.load refuses the overlay otherwise

Track the live status on the roadmap and in PRPs/BOARD.md.