diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index 98a0c4b..3cfb57c 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -15,14 +15,13 @@ workflows:
     '.github/workflows/estate-rules.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/fork-governance-publish.yml':
-        - 'actions/checkout@v7.0.1'
         - 'actions/download-artifact@v8.0.2'
     '.github/workflows/fork-governance.yml':
         - 'actions/upload-artifact@v7.0.2'
     '.github/workflows/governance.yml': []
     '.github/workflows/hypatia-scan.yml': []
     '.github/workflows/instant-sync.yml':
-        - 'step-security/harden-runner@v2.22.3'
+        - 'step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43'
         - 'peter-evans/repository-dispatch@v4.0.1'
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
@@ -154,7 +153,7 @@ dependencies:
         commit: 'sha1-efb35369e0ad2afab669f228072c1b0d510eae64'
         owner_id: 2242
         repo_id: 204253808
-    'step-security/harden-runner@v2.22.3':
+    'step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43':
         ref: 'v2.22.3'
         commit: 'sha1-46b06cea07f9e64621fdf066ba77ac6915163d43'
         owner_id: 88700172
diff --git a/.github/workflows/fork-governance-publish.yml b/.github/workflows/fork-governance-publish.yml
index 58ea684..3f0a2f6 100644
--- a/.github/workflows/fork-governance-publish.yml
+++ b/.github/workflows/fork-governance-publish.yml
@@ -3,9 +3,10 @@
 # Never check out the PR or execute anything downloaded from its run.
 #
 # Trust model: a fork PR controls the PR-side Fork governance workflow, so
-# its artifacts can lie. Lane pass/fail is therefore derived from GitHub's
-# own run metadata (job conclusions), the run must have actually called the
-# pinned reusable workflows named by the DEFAULT branch's
+# its artifacts can lie. Publication requires the PR head and base copies of
+# the scan workflow to match the default branch's trusted copy byte-for-byte.
+# Lane pass/fail is derived from GitHub's own run metadata (job conclusions),
+# and the run must have actually called the pinned reusable workflows named by the DEFAULT branch's
 # fork-governance.yml (referenced_workflows), and the artifact's lane
 # claims must agree or publication is refused. What remains
 # artifact-sourced is display shading only (K9/Hypatia verdict colors,
@@ -75,6 +76,23 @@ jobs:
           # workflow that fakes or swaps a lane does not satisfy this.
           gh api "repos/$GITHUB_REPOSITORY/contents/.github/workflows/fork-governance.yml" \
             --jq .content | base64 -d > "$RUNNER_TEMP/trusted-fork-governance.yml"
+          # A malicious PR can call the pinned reusables AND forge lookalike
+          # jobs/artifacts. Require the actual PR head and base workflow files
+          # to match the trusted default, not merely the list of reusables.
+          gh api "repos/$GITHUB_REPOSITORY/pulls/$pr" > "$RUNNER_TEMP/current-pr.json"
+          jq -e --arg sha "$sha" '.state == "open" and .head.sha == $sha' \
+            "$RUNNER_TEMP/current-pr.json" >/dev/null
+          head_repo=$(jq -r '.head.repo.full_name' "$RUNNER_TEMP/current-pr.json")
+          base_sha=$(jq -r '.base.sha' "$RUNNER_TEMP/current-pr.json")
+          gh api "repos/$head_repo/contents/.github/workflows/fork-governance.yml?ref=$sha" \
+            --jq .content | base64 -d > "$RUNNER_TEMP/head-fork-governance.yml"
+          gh api "repos/$GITHUB_REPOSITORY/contents/.github/workflows/fork-governance.yml?ref=$base_sha" \
+            --jq .content | base64 -d > "$RUNNER_TEMP/base-fork-governance.yml"
+          if ! cmp -s "$RUNNER_TEMP/trusted-fork-governance.yml" "$RUNNER_TEMP/head-fork-governance.yml" ||
+             ! cmp -s "$RUNNER_TEMP/trusted-fork-governance.yml" "$RUNNER_TEMP/base-fork-governance.yml"; then
+            echo "::error::PR scan workflow differs from the trusted default; refusing to publish."
+            exit 1
+          fi
           grep -oE 'uses: [^[:space:]#]+' "$RUNNER_TEMP/trusted-fork-governance.yml" \
             | awk '{print $2}' | grep '/\.github/workflows/' | sort -u \
             > "$RUNNER_TEMP/expected-reusables.txt"
@@ -116,7 +134,7 @@ jobs:
           name: fork-governance-result
           path: evidence
           github-token: ${{ github.token }}
-          run-id: ${{ steps.source.outputs.run }}
+          run-id: ${{ github.event.workflow_run.id }}
 
       - name: Validate lane result data
         if: steps.source.outputs.pr != ''
@@ -151,7 +169,7 @@ jobs:
           name: k9-grid
           path: k9-grid
           github-token: ${{ github.token }}
-          run-id: ${{ steps.source.outputs.run }}
+          run-id: ${{ github.event.workflow_run.id }}
 
       - name: Download the Hypatia grid from the verified run
         if: steps.source.outputs.pr != ''
@@ -161,18 +179,16 @@ jobs:
           name: verdict-grid
           path: verdict-grid
           github-token: ${{ github.token }}
-          run-id: ${{ steps.source.outputs.run }}
+          run-id: ${{ github.event.workflow_run.id }}
 
-      - name: Checkout the pinned trusted renderer
+      - name: Fetch the pinned trusted renderer
         if: steps.source.outputs.pr != ''
-        uses: actions/checkout@v7.0.1
-        with:
-          repository: metadatastician/standards
-          ref: 34cf03f988b8ca95b91b45d9b3351f7d3babfb65
-          path: canon
-          sparse-checkout: scripts/fork-governance-render.sh
-          sparse-checkout-cone-mode: false
-          persist-credentials: false
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          set -euo pipefail
+          gh api 'repos/metadatastician/standards/contents/scripts/fork-governance-render.sh?ref=34cf03f988b8ca95b91b45d9b3351f7d3babfb65' \
+            --jq .content | base64 -d > "$RUNNER_TEMP/trusted-renderer.sh"
 
       - name: Render and publish the verified run's summary
         if: steps.source.outputs.pr != ''
@@ -196,7 +212,7 @@ jobs:
                 --sha "$sha" --run "$(jq -r '.run' evidence/result.json)" --repo "$GITHUB_REPOSITORY")
           [ ! -s k9-grid/report.md ] || args+=(--k9-report k9-grid/report.md)
           [ ! -s verdict-grid/report.md ] || args+=(--hypatia-report verdict-grid/report.md)
-          bash canon/scripts/fork-governance-render.sh "${args[@]}" >/dev/null
+          bash "$RUNNER_TEMP/trusted-renderer.sh" "${args[@]}" >/dev/null
           cat "$RUNNER_TEMP/fork-governance/body.md" >> "$GITHUB_STEP_SUMMARY"
           comment_id=$(gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/issues/$PR_NUMBER/comments" \
             | jq -r '[.[][] | select(.user.login == "github-actions[bot]"
diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml
index 63e6104..b218961 100644
--- a/.github/workflows/instant-sync.yml
+++ b/.github/workflows/instant-sync.yml
@@ -23,7 +23,7 @@ jobs:
       # risking the dispatch; tighten to block+allowlist once a main run
       # shows the observed set.
       - name: Harden runner (egress audit)
-        uses: step-security/harden-runner@v2.22.3
+        uses: step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43 # v2.22.3
         with:
           egress-policy: audit
       - name: Trigger Propagation
diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml
index 1c0b456..885a13d 100644
--- a/.github/workflows/main-estate-audit.yml
+++ b/.github/workflows/main-estate-audit.yml
@@ -29,59 +29,59 @@ jobs:
         with:
           fetch-depth: 0
           persist-credentials: false
-      
+
       - name: Required Files Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/required-files-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Code Hygiene Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/code-hygiene-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Manifest Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/manifest-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Idris2 ABI Purity Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/idris2-abi-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Zig UnifiedApiAdapter API Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/zig-unified-api-adapter-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Contractile Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/contractile-validation-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Recipes Set Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/recipes-set-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Affirmation Document Gate
         if: ${{ !cancelled() }}
         run: bash .github/affirmation-trusted/check.sh
-        
+
       - name: Academic Referencing Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/referencing-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Semantic Audit Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/semantic-audit-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: SPDX License Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/spdx-license-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Proof Runner Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/proof-runner-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: PRAT Testing Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/prat-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       # No "Panic Attack & Pons" step here (removed 2026-10-28): the
       # cicd-suite custom-tools-check composite prints "validation passed"
       # when neither tool is on PATH — which is always — so it certified
@@ -94,47 +94,47 @@ jobs:
       - name: WWW & Well-Known Compliance Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/www-compliance-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: BoJ Cartridge Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/boj-cartridge-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Formatting Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/formatting-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Accreditations & Badges Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/badges-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Metrics Extraction Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/metrics-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Linguist & Banned Languages Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/linguist-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Test & Benchmarks Dashboard Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/tests-benches-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Hosting & Site Status Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/hosting-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Git-Sea Analytics Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/gitsea-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Trust & Humans Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/trust-humans-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Are We UnAPI Gate (Secret Scanning)
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/secrets-check@bf7dd95cf49733019343ff485c2f45c6b261839c
-        
+
       - name: Reasonably Good Token Validation Gate
         if: ${{ !cancelled() }}
         uses: hyperpolymath/cicd-suite/actions/vaulted-tokens-check@bf7dd95cf49733019343ff485c2f45c6b261839c
diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index cea17dd..e934770 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -27,6 +27,7 @@ on:
     paths:
       - 'verification/proofs/lean4/**'
       - 'verification/proofs/agda/**'
+      - 'tests/lib/strip-proof-comments.awk'
       - '.github/workflows/proofs.yml'
   pull_request:
   workflow_dispatch:
@@ -281,6 +282,14 @@ jobs:
               echo "::error::axiom-audit failed to run for $m (exit $audit_status)"
               exit 1
             fi
+            # jq -s silently skips empty files. Require exactly one report per
+            # module even when the tool exits 1 (a reported violation).
+            if ! jq -e -s 'length == 1 and (.[0] | type == "object" and (.audited | type == "number"))' \
+                 "$work/report-$m.json" >/dev/null 2>&1; then
+              cat "$work/report-$m.json" || true
+              echo "::error::axiom-audit produced no valid JSON report for $m (exit $audit_status)"
+              exit 1
+            fi
           done
           report="$work/report.json"
           # Lean 4.16 stores compiler IR (`_cstage*`, equation/match auxiliaries)
diff --git a/.github/workflows/quality.yml b/.github/workflows/quality.yml
index 5f1b2a4..b66d3df 100644
--- a/.github/workflows/quality.yml
+++ b/.github/workflows/quality.yml
@@ -75,7 +75,12 @@ jobs:
       - name: Gate falsifiability canaries (R10)
         run: bash scripts/test-gate-falsifiability.sh
       - name: Workflow and gate regression tests
-        run: bash tests/workflows/review_regressions_test.sh
+        run: |
+          bash tests/workflows/review_regressions_test.sh
+          bash tests/workflows/audit_report_test.sh
+          bash tests/workflows/publisher_trust_test.sh
+          bash tests/workflows/setup_test.sh
+          bash tests/workflows/validate_workflows_test.sh
   docs-present:
     runs-on: ubuntu-latest
     timeout-minutes: 15
diff --git a/.github/workflows/trope-check.yml b/.github/workflows/trope-check.yml
index f58954a..9a4beb3 100644
--- a/.github/workflows/trope-check.yml
+++ b/.github/workflows/trope-check.yml
@@ -14,9 +14,11 @@ on:
     paths:
       - 'schemas/**'
       - 'src/idris2/**'
+      - 'src/rust/**'
       - 'src/interface/**'
       - 'abi.ipkg'
       - 'tests/conformance/**'
+      - 'tests/lib/strip-proof-comments.awk'
       - 'verification/proofs/idris2/**'
       - 'spec/**'
       - '.github/workflows/trope-check.yml'
diff --git a/build/setup.sh b/build/setup.sh
index 9fb76e0..97e11d8 100755
--- a/build/setup.sh
+++ b/build/setup.sh
@@ -134,11 +134,16 @@ detect_platform() {
             elif command -v choco >/dev/null 2>&1; then PKG_MGR="choco"
             fi
             ;;
-        FreeBSD*|DragonFly*)
+        FreeBSD*)
             OS="freebsd"
             DISTRO="freebsd"
             PKG_MGR="pkg"
             ;;
+        DragonFly*)
+            OS="dragonfly"
+            DISTRO="dragonfly"
+            PKG_MGR="pkg"
+            ;;
         OpenBSD*)
             OS="openbsd"
             DISTRO="openbsd"
@@ -257,40 +262,30 @@ install_just_pinned() {
         }
     fi
 
-    if [ -w /usr/local/bin ]; then
-        _just_dest="/usr/local/bin"
-        _just_elevated="false"
-    elif [ "$(id -u 2>/dev/null || echo 1)" = "0" ] \
-        || command -v sudo >/dev/null 2>&1 || command -v doas >/dev/null 2>&1; then
-        _just_dest="/usr/local/bin"
-        _just_elevated="true"
+    _just_dest="/usr/local/bin"
+    if [ -d "$_just_dest" ] && [ -w "$_just_dest" ] &&
+        install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary"; then
+        : # Installed without elevation.
+    elif [ -d "$_just_dest" ] && { [ "$(id -u 2>/dev/null || echo 1)" = "0" ] ||
+        command -v sudo >/dev/null 2>&1 || command -v doas >/dev/null 2>&1; } &&
+        as_root install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary"; then
+        : # Installed with elevation.
     elif [ -n "${HOME:-}" ]; then
         _just_dest="$HOME/.local/bin"
-        _just_elevated="false"
-        mkdir -p "$_just_dest"
+        if ! mkdir -p "$_just_dest" || ! install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary"; then
+            fail "Could not install just into $_just_dest"
+            rm -rf "$_just_tmp"
+            return 1
+        fi
         warn "Installing just into $_just_dest; ensure it is on PATH for future shells"
     else
         fail "No writable install directory for just"
         rm -rf "$_just_tmp"
         return 1
     fi
-
-    if [ "$_just_elevated" = "true" ] && [ ! -w "$_just_dest" ]; then
-        as_root install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary" || {
-            fail "Could not install just into $_just_dest"
-            rm -rf "$_just_tmp"
-            return 1
-        }
-    else
-        install -m 0755 "$_just_tmp/$_just_binary" "$_just_dest/$_just_binary" || {
-            fail "Could not install just into $_just_dest"
-            rm -rf "$_just_tmp"
-            return 1
-        }
-    fi
-    PATH="$_just_dest:$PATH"
-    export PATH
     rm -rf "$_just_tmp"
+    PATH="$_just_dest${PATH:+:$PATH}"
+    export PATH
 }
 
 # Ensure just is on PATH, reusing an existing installation when available.
@@ -320,8 +315,9 @@ install_just() {
         scoop)      scoop install just ;;
         winget)     winget install --exact --id Casey.Just ;;
         choco)      choco install just -y ;;
-        rpm-ostree) as_root rpm-ostree install just ;;
-        guix)       guix install just ;;
+        # rpm-ostree layers packages for the next boot; Guix's profile may
+        # not be on this process's PATH. The pinned binary is usable now.
+        rpm-ostree|guix) install_just_pinned ;;
         pkg)        as_root pkg install -y just ;;
         pkg_add)    as_root pkg_add just ;;
         pkgin)      as_root pkgin -y install just ;;
diff --git a/spec/calculus.adoc b/spec/calculus.adoc
index 90eb694..70fcb32 100644
--- a/spec/calculus.adoc
+++ b/spec/calculus.adoc
@@ -720,15 +720,16 @@ The tropechecker is a *pure function from Trope IR to a verdict object*:
 `p-sufficient` / `p-insufficient`, plus the witness edge (§6.2). It performs
 normalization (A3) and validation (HC-4 coherence; the prevent profile's
 rejection of deceptive values). Before grade accumulation, it MUST validate the
-graph structure, rejecting unknown node references, duplicate producers for a
-node, and cycles as validation faults; these inputs MUST NOT produce a verdict.
+graph structure, rejecting duplicate node or edge IDs, unknown node references,
+duplicate producers for a node, and cycles as validation faults; these inputs
+MUST NOT produce a verdict.
 Only a valid DAG proceeds to grade composition and final floor-subsumption.
 *It MUST NOT parse, execute, or otherwise depend on source.*
 
 Structural validation and the order-independent witness selection of §6.2 are
 implemented in both the reference (Idris2) and fast (Rust) cores and are
 conformance requirements: the `graph-invalid` corpus pins rejection of
-duplicate node IDs, undeclared references, duplicate producers and cycles,
+duplicate node and edge IDs, undeclared references, duplicate producers and cycles,
 and the `witness-permutation` cases pin that permuting the edge array cannot
 change the named witness.
 
diff --git a/src/idris2/Checker/Decode.idr b/src/idris2/Checker/Decode.idr
index 356bdea..28f4705 100644
--- a/src/idris2/Checker/Decode.idr
+++ b/src/idris2/Checker/Decode.idr
@@ -208,13 +208,16 @@ validateGraph ns es ou =
   case dupOf declared of
     Just d  => Left ("nodes/" ++ d ++ ": duplicate node id")
     Nothing =>
-      if not (elem ou declared)
-         then Left ("use_model/output: undeclared node \"" ++ ou ++ "\"")
-         else do
-           checkEdges declared [] es
-           if acyclic (length es) es es []
-              then Right ()
-              else Left "edges: cycle in the producer graph"
+      case dupOf (map eid es) of
+        Just d => Left ("edges/" ++ d ++ ": duplicate edge id")
+        Nothing =>
+          if not (elem ou declared)
+             then Left ("use_model/output: undeclared node \"" ++ ou ++ "\"")
+             else do
+               checkEdges declared [] es
+               if acyclic (length es) es es []
+                  then Right ()
+                  else Left "edges: cycle in the producer graph"
 
 export
 decodeDoc : JValue -> Either String Document
diff --git a/src/rust/src/lib.rs b/src/rust/src/lib.rs
index 8b6a9b3..698ad09 100644
--- a/src/rust/src/lib.rs
+++ b/src/rust/src/lib.rs
@@ -709,6 +709,11 @@ pub fn dec_edge(v: &Json) -> Result<Edge, String> {
         .and_then(|x| x.as_str())
         .ok_or("edges: missing id")?
         .to_string();
+    match v.field("effect").and_then(Json::as_str) {
+        Some("preserve" | "project" | "collapse" | "detach" | "attenuate" | "fuse") => {}
+        Some(effect) => return Err(format!("edges/{id}/effect: unknown effect \"{effect}\"")),
+        None => return Err(format!("edges/{id}/effect: missing or non-string effect")),
+    }
     let inputs = match v.field("inputs") {
         Some(i) => str_list(i),
         None => Vec::new(),
@@ -765,8 +770,8 @@ pub fn dec_floor(v: &Json) -> Result<Floor, String> {
     })
 }
 /// Validate the graph structure the calculus requires before grading: node
-/// IDs are unique, every referenced node (edge inputs, edge outputs, and
-/// `use_model.output`) is declared, each node has at most one producing
+/// and edge IDs are unique, every referenced node (edge inputs, edge outputs,
+/// and `use_model.output`) is declared, each node has at most one producing
 /// edge, and the producer graph is acyclic.
 ///
 /// Structural faults are validation faults and MUST NOT produce a verdict:
@@ -783,7 +788,11 @@ fn validate_graph(nodes: &[Node], edges: &[Edge], out: &str) -> Result<(), Strin
         return Err(format!("use_model/output: undeclared node \"{out}\""));
     }
     let mut producer: BTreeMap<&str, &str> = BTreeMap::new();
+    let mut edge_ids = BTreeSet::new();
     for e in edges {
+        if !edge_ids.insert(e.id.as_str()) {
+            return Err(format!("edges/{}: duplicate edge id", e.id));
+        }
         if !declared.contains(e.output.as_str()) {
             return Err(format!(
                 "edges/{}/output: undeclared node \"{}\"",
@@ -831,8 +840,8 @@ fn validate_graph(nodes: &[Node], edges: &[Edge], out: &str) -> Result<(), Strin
 /// # Errors
 /// Returns an error for unsupported versions, missing document fields,
 /// invalid nodes, edges, or floors, or a structurally invalid graph
-/// (duplicate node IDs, undeclared node references, duplicate producers,
-/// or cycles) — see `validate_graph`.
+/// (duplicate node or edge IDs, undeclared node references, duplicate
+/// producers, or cycles) — see `validate_graph`.
 pub fn dec_doc(v: &Json) -> Result<Doc, String> {
     // Accepted document versions (IR 0.2, R-2026-07-07). "0.1" stays accepted:
     // the wire format is identical, and 0.1 documents are normalized and graded
@@ -842,6 +851,15 @@ pub fn dec_doc(v: &Json) -> Result<Doc, String> {
         Some(o) => return Err(format!("version: unsupported \"{o}\" (accepted: 0.1, 0.2)")),
         None => return Err("missing \"version\"".into()),
     }
+    match v.field("profile").and_then(Json::as_str) {
+        Some("prevent") => {}
+        Some(profile) => {
+            return Err(format!(
+                "profile: unsupported \"{profile}\" (expected prevent)"
+            ))
+        }
+        None => return Err("profile: missing or non-string profile".into()),
+    }
     let nodes = v
         .field("nodes")
         .and_then(Json::as_arr)
@@ -1116,3 +1134,71 @@ mod grade_le_tests {
         assert!(grade_le(&loose, &residue), "floor 10 must be met by loss 6");
     }
 }
+
+#[cfg(test)]
+mod decoder_profile_effect_tests {
+    use super::*;
+
+    fn fixture() -> Json {
+        parse_json(include_str!(
+            "../../../tests/conformance/fixtures/atten-zero-normalizes.ir.json"
+        ))
+        .unwrap()
+    }
+
+    fn set_field(value: &mut Json, name: &str, replacement: Option<Json>) {
+        let Json::Obj(fields) = value else {
+            panic!("expected an object");
+        };
+        fields.retain(|(key, _)| key != name);
+        if let Some(replacement) = replacement {
+            fields.push((name.to_string(), replacement));
+        }
+    }
+
+    #[test]
+    fn document_requires_prevent_profile() {
+        assert!(dec_doc(&fixture()).is_ok());
+        for value in [None, Some(Json::Null), Some(Json::Str("detect".into()))] {
+            let mut doc = fixture();
+            set_field(&mut doc, "profile", value);
+            assert!(matches!(dec_doc(&doc), Err(e) if e.contains("profile")));
+        }
+    }
+
+    #[test]
+    fn edge_requires_a_writable_effect() {
+        let Json::Arr(edges) = fixture().field("edges").unwrap().clone() else {
+            panic!("expected edges");
+        };
+        let edge = &edges[0];
+        for effect in [
+            "preserve",
+            "project",
+            "collapse",
+            "detach",
+            "attenuate",
+            "fuse",
+        ] {
+            let mut edge = edge.clone();
+            set_field(&mut edge, "effect", Some(Json::Str(effect.into())));
+            assert!(dec_edge(&edge).is_ok(), "{effect}");
+        }
+        for value in [None, Some(Json::Null), Some(Json::Str("falsify".into()))] {
+            let mut doc = fixture();
+            let Json::Obj(ref mut fields) = doc else {
+                panic!("expected a document");
+            };
+            let Json::Arr(edges) = &mut fields
+                .iter_mut()
+                .find(|field| field.0 == "edges")
+                .unwrap()
+                .1
+            else {
+                panic!("expected edges");
+            };
+            set_field(&mut edges[0], "effect", value);
+            assert!(matches!(dec_doc(&doc), Err(e) if e.contains("effect")));
+        }
+    }
+}
diff --git a/tests/conformance/graph-invalid/duplicate-edge-id.json b/tests/conformance/graph-invalid/duplicate-edge-id.json
new file mode 100644
index 0000000..1c55400
--- /dev/null
+++ b/tests/conformance/graph-invalid/duplicate-edge-id.json
@@ -0,0 +1,119 @@
+{
+  "$schema": "https://github.com/hyperpolymath/trope-checker/schemas/trope-ir.schema.json",
+  "$comment": "SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>. SPDX-License-Identifier: MPL-2.0 | graph-invalid: duplicate IDs on a chain of distinct producer edges",
+  "version": "0.2",
+  "profile": "prevent",
+  "nodes": [
+    {
+      "id": "t0",
+      "type": "Trope",
+      "present": [
+        "quality",
+        "bearer",
+        "context",
+        "record"
+      ]
+    },
+    {
+      "id": "t1",
+      "type": "Trope",
+      "present": [
+        "quality",
+        "bearer",
+        "context",
+        "record"
+      ]
+    },
+    {
+      "id": "t2",
+      "type": "Trope",
+      "present": [
+        "quality",
+        "bearer",
+        "context",
+        "record"
+      ]
+    }
+  ],
+  "edges": [
+    {
+      "id": "e_att1",
+      "effect": "attenuate",
+      "inputs": [
+        "t0"
+      ],
+      "output": "t1",
+      "grade": {
+        "fate": {
+          "quality": {
+            "k": "Attenuated",
+            "delta": 3
+          },
+          "bearer": {
+            "k": "Attenuated",
+            "delta": 3
+          },
+          "context": {
+            "k": "Attenuated",
+            "delta": 3
+          },
+          "record": {
+            "k": "Attenuated",
+            "delta": 3
+          }
+        },
+        "bond": {
+          "k": "Intact"
+        },
+        "merge": {
+          "k": "Single"
+        }
+      }
+    },
+    {
+      "id": "e_att1",
+      "effect": "attenuate",
+      "inputs": [
+        "t1"
+      ],
+      "output": "t2",
+      "grade": {
+        "fate": {
+          "quality": {
+            "k": "Attenuated",
+            "delta": 4
+          },
+          "bearer": {
+            "k": "Attenuated",
+            "delta": 4
+          },
+          "context": {
+            "k": "Attenuated",
+            "delta": 4
+          },
+          "record": {
+            "k": "Attenuated",
+            "delta": 4
+          }
+        },
+        "bond": {
+          "k": "Intact"
+        },
+        "merge": {
+          "k": "Single"
+        }
+      }
+    }
+  ],
+  "use_model": {
+    "output": "t2",
+    "floor": {
+      "fate": {
+        "quality": {
+          "k": "Attenuated",
+          "delta": 7
+        }
+      }
+    }
+  }
+}
diff --git a/tests/workflows/audit_report_test.sh b/tests/workflows/audit_report_test.sh
new file mode 100755
index 0000000..6e61d62
--- /dev/null
+++ b/tests/workflows/audit_report_test.sh
@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Exercise the exact per-module report predicate used by the proof workflow.
+set -euo pipefail
+root=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd)
+filter=$(sed -n "s/.*jq -e -s '\([^']*\)'.*/\1/p" "$root/.github/workflows/proofs.yml")
+[[ -n "$filter" ]] || { echo 'Missing per-module report predicate' >&2; exit 1; }
+check() {
+  local expected=$1 input=$2 status
+  if printf '%s' "$input" | jq -e -s "$filter" >/dev/null 2>&1; then status=0; else status=1; fi
+  [[ "$status" == "$expected" ]] || { echo "Unexpected report result for: $input" >&2; exit 1; }
+}
+check 1 ''
+check 1 '{'
+check 1 '[]'
+check 1 '{}'
+check 1 '{"audited":"1"}'
+check 1 '{"audited":1} {"audited":2}'
+check 0 '{"audited":0}'
+check 0 '{"audited":10,"violations":[]}'
+echo 'PASS: every module must produce exactly one object with numeric audited'
diff --git a/tests/workflows/publisher_trust_test.sh b/tests/workflows/publisher_trust_test.sh
new file mode 100755
index 0000000..a1283bb
--- /dev/null
+++ b/tests/workflows/publisher_trust_test.sh
@@ -0,0 +1,44 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Exercise the publisher's actual source-verification step with mocked GitHub API responses.
+set -euo pipefail
+root=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd)
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+export RUNNER_TEMP="$work" GITHUB_REPOSITORY='owner/repo' GITHUB_EVENT_PATH="$work/event.json"
+export GITHUB_OUTPUT="$work/output" MOCK_DIR="$work"
+printf '%s\n' '{"workflow_run":{"id":17,"head_sha":"abc","run_attempt":1},"repository":{"full_name":"owner/repo"}}' > "$GITHUB_EVENT_PATH"
+printf '%s\n' 'uses: owner/canon/.github/workflows/scan.yml@123' > "$work/trusted.yml"
+cp "$work/trusted.yml" "$work/head.yml"
+mkdir "$work/bin"
+cat > "$work/bin/gh" <<'MOCK'
+#!/usr/bin/env bash
+set -euo pipefail
+case "$*" in
+  *'actions/workflows/fork-governance.yml'*) echo 8 ;;
+  *'actions/runs/17/jobs?'*) echo '[{"jobs":[{"name":"DEED syntax / lint","conclusion":"success"},{"name":"K9-DEED conformance / validate","conclusion":"success"},{"name":"Hypatia verdict grid / Hypatia Neurosymbolic Analysis","conclusion":"success"}]}]' ;;
+  *'actions/runs/17'*) echo '{"workflow_id":8,"event":"pull_request","status":"completed","repository":{"full_name":"owner/repo"},"head_sha":"abc","run_attempt":1,"referenced_workflows":[{"path":"owner/canon/.github/workflows/scan.yml@123"}]}' ;;
+  *'commits/abc/pulls'*) echo '[[{"number":12,"state":"open","head":{"sha":"abc"},"base":{"repo":{"full_name":"owner/repo"}}}]]' ;;
+  *'pulls/12'*) echo '{"state":"open","head":{"sha":"abc","repo":{"full_name":"owner/fork"}},"base":{"sha":"def"}}' ;;
+  *'repos/owner/fork/contents/'*) base64 -w0 "$MOCK_DIR/head.yml" ;;
+  *'repos/owner/repo/contents/'*) base64 -w0 "$MOCK_DIR/trusted.yml" ;;
+  *) echo "unexpected gh call: $*" >&2; exit 1 ;;
+esac
+MOCK
+chmod +x "$work/bin/gh"
+export PATH="$work/bin:$PATH"
+# Copy the YAML block itself, rather than a second implementation of the check.
+python3 - "$root/.github/workflows/fork-governance-publish.yml" > "$work/source.sh" <<'PY'
+import sys
+text = open(sys.argv[1]).read()
+step = text.split('      - name: Verify the source run and current pull request\n', 1)[1]
+script = step.split('        run: |\n', 1)[1].split('\n      - name:', 1)[0]
+print('\n'.join(line[10:] if line.startswith('          ') else line for line in script.splitlines()))
+PY
+bash "$work/source.sh"
+printf '%s\n' 'uses: owner/canon/.github/workflows/scan.yml@123' '# attacker adds forged jobs' > "$work/head.yml"
+if bash "$work/source.sh" >/dev/null 2>&1; then
+  echo 'FAIL: PR-modified workflow was accepted' >&2
+  exit 1
+fi
+echo 'PASS: publisher rejects PR-modified scan workflows even when reusable pins match'
diff --git a/tests/workflows/setup_test.sh b/tests/workflows/setup_test.sh
new file mode 100755
index 0000000..6ba191f
--- /dev/null
+++ b/tests/workflows/setup_test.sh
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Exercise setup's real platform and just-install functions without network or root.
+# The sourced functions invoke the mocks indirectly.
+# shellcheck disable=SC2329
+set -euo pipefail
+root=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd)
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+sed '$d' "$root/build/setup.sh" > "$work/setup-lib.sh"
+(
+  # shellcheck source=/dev/null
+  . "$work/setup-lib.sh"
+  uname() { case "$1" in -m) echo x86_64 ;; -s) echo DragonFly ;; esac; }
+  detect_platform
+  [ "$OS" = dragonfly ] && [ "$DISTRO" = dragonfly ] && [ "$PKG_MGR" = pkg ]
+)
+(
+  # shellcheck source=/dev/null
+  . "$work/setup-lib.sh"
+  HOME="$work/home"; export HOME
+  uname() { case "$1" in -m) echo x86_64 ;; -s) echo Linux ;; esac; }
+  curl() { return 0; }
+  sha256sum() { return 0; }
+  tar() { printf '#!/bin/sh\necho just\n' > "$4/just"; }
+  install() { case "$4" in /usr/local/bin/*) return 1 ;; *) /bin/cp "$3" "$4" && /bin/chmod +x "$4" ;; esac; }
+  as_root() { return 1; }
+  mkdir() { /bin/mkdir "$@"; }
+  rm() { /bin/rm "$@"; }
+  mktemp() { /usr/bin/mktemp "$@"; }
+  unset PATH
+  install_just_pinned
+  [ "$PATH" = "$HOME/.local/bin" ] && [ -x "$HOME/.local/bin/just" ]
+)
+echo 'PASS: setup preserves DragonFly identity and falls back when elevation fails with PATH unset'
diff --git a/wiki/Home.md b/wiki/Home.md
index 4f957c0..171e63d 100644
--- a/wiki/Home.md
+++ b/wiki/Home.md
@@ -24,9 +24,11 @@ Agda.
 
 ## The central open problem
 
-**CO-1** — the calculus has no operational model for `fix`/routing dynamics (gated by
-v0.1's **O4**, the limit carrier). Tracked at issue #10 (CO-1), #12 (O4). See
-`verification/proofs/INTEGRATION-REPORT.adoc` §4 and ADR `docs/decisions/0003-split-reference-semantics.adoc`.
+**CO-1** — an operational model for `fix`/routing dynamics has been designed, but
+not yet mechanised; full subject reduction remains open (issue #10). **O4**, the
+limit-carrier question (issue #12), is resolved under the ratified carrier repair
+and no longer gates CO-1. See `spec/notes/2026-07-07-co1-operational-model.adoc`
+and `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc` §4.
 
 ## Gates