diff --git a/labs/12-product-engineering-loop/boatstack-distribution/release-notes/2026-07-27-denials-name-their-solutions.md b/labs/12-product-engineering-loop/boatstack-distribution/release-notes/2026-07-27-denials-name-their-solutions.md
new file mode 100644
index 000000000..8fa5d7ec0
--- /dev/null
+++ b/labs/12-product-engineering-loop/boatstack-distribution/release-notes/2026-07-27-denials-name-their-solutions.md
@@ -0,0 +1,7 @@
+### Denials now hand you the legal moves
+
+A denial that only states the rule leaves an agent — especially a smaller model — retrying the same blocked call. Every guard denial now carries its computed solution set: a short "You can:" list of exact runnable commands that are legal from the position the denial describes, with owed human inputs marked. A plan-gate denial lists the planning channel commands for that stage; an operation denial lists the inspection commands; a protected-path denial additionally names the verbs that own the path, straight from the state-ownership map.
+
+The picks are computed from the same declarations the guard enforces, and conformance sweeps keep the loop closed: every category of denial either enumerates picks or is a documented exception, and every pick passes the guard's own laws — the guard never hands out a command it would then deny.
+
+The plain reason string carries up to three picks on every host; the full set rides on the opt-in structured payload, additively, under the same schema version.
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/denial.go b/labs/12-product-engineering-loop/product-engineering-loop/denial.go
index 1412fff54..eca7d548e 100644
--- a/labs/12-product-engineering-loop/product-engineering-loop/denial.go
+++ b/labs/12-product-engineering-loop/product-engineering-loop/denial.go
@@ -58,6 +58,18 @@ type Denial struct {
 	Detail      string   // guidance; may contain `code` spans
 	Reassurance string   // "Nothing was written; your files are untouched." (empty if an effect occurred)
 	Hint        string   // recovery command, e.g. "boatstack-helper diagnose-hook"
+	// Options is the denial's computed solution set: the admissible commands
+	// from exactly the position the finding describes, so a weaker model picks
+	// a legal move instead of retrying the blocked one. Derived from the same
+	// declarations the guard enforces; renders as a short "You can:" list and
+	// rides in full on the structured payload.
+	// control-law: solution-set-derives-from-guard-declarations
+	Options          []PrescribedCommand
+	OptionsTruncated bool
+	// OwnerVerbs names the verbs that own a protected path (state-tamper
+	// denials), derived from the state-ownership map. Named, never compiled
+	// into runnable commands — their full arguments are not derivable here.
+	OwnerVerbs []string
 }
 
 // --- ANSI palette (truecolor; matches the approved mockup) -------------------
@@ -107,6 +119,29 @@ func (d Denial) Render(mode RenderMode) string {
 	}
 }
 
+// optionLines renders the solution set as at most `limit` numbered command
+// lines, plus an overflow note. Shared by the three text renderers so every
+// surface shows the same picks.
+// control-law: solution-set-derives-from-guard-declarations
+func (d Denial) optionLines(limit int) []string {
+	if len(d.Options) == 0 {
+		return nil
+	}
+	shown := d.Options
+	if len(shown) > limit {
+		shown = shown[:limit]
+	}
+	lines := make([]string, 0, len(shown)+1)
+	for i, option := range shown {
+		lines = append(lines, fmt.Sprintf("  %d) %s", i+1, option.CommandLine()))
+	}
+	hidden := len(d.Options) - len(shown)
+	if d.OptionsTruncated || hidden > 0 {
+		lines = append(lines, "  (more legal moves: run boatstack-helper next-status)")
+	}
+	return lines
+}
+
 func (d Denial) renderPlain(badge string) string {
 	var b strings.Builder
 	head := badge
@@ -122,6 +157,13 @@ func (d Denial) renderPlain(badge string) string {
 		b.WriteString("\n\n↳ ")
 		b.WriteString(d.Reassurance)
 	}
+	if len(d.OwnerVerbs) > 0 {
+		b.WriteString("\n\nThis path is owned by: " + strings.Join(d.OwnerVerbs, ", ") + ".")
+	}
+	if lines := d.optionLines(solutionSetTextCap); len(lines) > 0 {
+		b.WriteString("\n\nYou can:\n")
+		b.WriteString(strings.Join(lines, "\n"))
+	}
 	if d.Hint != "" {
 		b.WriteString("\n\nFalse positive? run: ")
 		b.WriteString(d.Hint)
@@ -141,6 +183,15 @@ func (d Denial) renderMarkdown(badge string) string {
 	if d.Reassurance != "" {
 		b.WriteString("\n\n↳ _" + d.Reassurance + "_")
 	}
+	if len(d.OwnerVerbs) > 0 {
+		b.WriteString("\n\nThis path is owned by: `" + strings.Join(d.OwnerVerbs, "`, `") + "`.")
+	}
+	if lines := d.optionLines(solutionSetTextCap); len(lines) > 0 {
+		b.WriteString("\n\nYou can:\n")
+		for _, line := range lines {
+			b.WriteString("\n" + line)
+		}
+	}
 	if d.Hint != "" {
 		b.WriteString("\n\nFalse positive? run `" + d.Hint + "`")
 	}
@@ -160,6 +211,15 @@ func (d Denial) renderANSI(badge string) string {
 	if d.Reassurance != "" {
 		b.WriteString("\n" + fgGray + "↳ " + d.Reassurance + ansiReset)
 	}
+	if len(d.OwnerVerbs) > 0 {
+		b.WriteString("\n" + fgGray + "this path is owned by: " + ansiReset + fgCode + strings.Join(d.OwnerVerbs, ", ") + ansiReset)
+	}
+	if lines := d.optionLines(solutionSetTextCap); len(lines) > 0 {
+		b.WriteString("\n" + fgGray + "you can:" + ansiReset)
+		for _, line := range lines {
+			b.WriteString("\n" + fgCode + line + ansiReset)
+		}
+	}
 	if d.Hint != "" {
 		b.WriteString("\n" + fgGray + ansiDim + "false positive? run " + ansiReset + fgCode + d.Hint + ansiReset)
 	}
@@ -206,6 +266,33 @@ func (d Denial) Structured() map[string]any {
 	if d.Hint != "" {
 		out["hint"] = d.Hint
 	}
+	// Additive keys only — schema_version stays 1; a consumer that ignores them
+	// loses nothing (the flat reason string already carries the capped picks).
+	// control-law: solution-set-derives-from-guard-declarations
+	if len(d.Options) > 0 {
+		options := make([]map[string]any, 0, len(d.Options))
+		for _, option := range d.Options {
+			row := map[string]any{
+				"verb":         option.Verb,
+				"command_line": option.CommandLine(),
+				"transition":   string(option.Transition),
+			}
+			if len(option.Args) > 0 {
+				row["args"] = option.Args
+			}
+			if len(option.RequiresHumanInput) > 0 {
+				row["requires_human_input"] = option.RequiresHumanInput
+			}
+			options = append(options, row)
+		}
+		out["options"] = options
+		if d.OptionsTruncated {
+			out["options_truncated"] = true
+		}
+	}
+	if len(d.OwnerVerbs) > 0 {
+		out["owner_verbs"] = d.OwnerVerbs
+	}
 	return out
 }
 
@@ -296,11 +383,27 @@ func DenialDemo(host string, mode RenderMode) string {
 		if i > 0 {
 			b.WriteString("\n\n")
 		}
-		b.WriteString(denialFor(host, finding).Render(mode))
+		b.WriteString(denialWithOptions(".", host, finding).Render(mode))
 	}
 	return b.String()
 }
 
+// denialWithOptions composes the pure finding→Denial mapping with the
+// enumerated solution set for the finding's position. denialFor stays pure
+// (DenialDemo and tests use it directly); the hook deny paths call this so
+// every real denial carries its picks.
+// control-law: solution-set-derives-from-guard-declarations
+func denialWithOptions(repo, host string, finding SafetyFinding) Denial {
+	d := denialFor(host, finding)
+	set := enumerateDenialSolutions(repo, host, finding)
+	d.Options = set.Options
+	d.OptionsTruncated = set.Truncated
+	if finding.Category == "workflow-state-tamper" {
+		d.OwnerVerbs = tamperOwnerVerbs(repo, finding.AttemptedPath)
+	}
+	return d
+}
+
 const reassureUntouched = "Nothing was written; your files are untouched."
 
 // denialFor maps a SafetyFinding to a structured Denial. It preserves every
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/denial_solutions.go b/labs/12-product-engineering-loop/product-engineering-loop/denial_solutions.go
new file mode 100644
index 000000000..3eaf32fb9
--- /dev/null
+++ b/labs/12-product-engineering-loop/product-engineering-loop/denial_solutions.go
@@ -0,0 +1,194 @@
+package boatstack
+
+import (
+	"strings"
+
+	"github.com/operatorstack/boatstack/boatstack/internal/deliverycontrol"
+)
+
+// A denial that only states the law leaves a weaker model looping on the same
+// blocked call. Each denial therefore carries the law's computed solution set:
+// the admissible commands from exactly the position the finding describes,
+// derived from the same declarations the guard enforces (the planning
+// enumeration for phase findings, the registry's observe rows, the
+// state-ownership map for protected paths) — never a hand-written list.
+// The enumeration reads only the finding's own fields and the declared tables,
+// so the deny path stays fast and cannot itself fail on unreadable state.
+// control-law: solution-set-derives-from-guard-declarations
+
+// denialMarker names a denial-prescribed helper verb outside the delivery
+// model, mirroring the planning./recovery. marker convention: self-describing
+// provenance, never a legal registry transition, never auto-driven.
+func denialMarker(verb string) deliverycontrol.TransitionID {
+	return deliverycontrol.TransitionID("denial." + strings.ReplaceAll(verb, "-", "_"))
+}
+
+// denialSolutionExceptions are the finding categories that deliberately carry
+// no solution set, with the reason. The totality sweep fails a new category
+// until it gains an enumeration rule or an entry here.
+var denialSolutionExceptions = map[string]string{
+	"malformed-tool-input":  "the tool event itself is unreadable; the Detail already names diagnose-hook with the exact host",
+	"unsupported-host":      "an unknown host has no trusted verb surface to enumerate",
+	"unresolved-repository": "without a repository identity no command can be assembled faithfully",
+}
+
+// enumerateDenialSolutions computes the solution set for a denial finding.
+// host is the coding host the hook is serving (for diagnose-hook assembly).
+func enumerateDenialSolutions(repo, host string, finding SafetyFinding) SolutionSet {
+	set := SolutionSet{Basis: "denial", Stage: finding.WorkflowStage}
+	if _, excepted := denialSolutionExceptions[finding.Category]; excepted {
+		return set
+	}
+	switch {
+	case finding.Category == "workflow-phase-bypass", finding.Category == "workflow-state-invalid":
+		// The finding carries the exact planning position; re-run the planning
+		// enumeration from it. Pure — no filesystem reads on the deny path.
+		status := NextStatus{
+			ObservedStage: finding.WorkflowStage,
+			NextOperation: finding.NextOperation,
+			Feature:       finding.BlockingFeature,
+		}
+		if finding.Category == "workflow-state-invalid" {
+			status.ObservedStage = "INVALID_STATE"
+			if finding.BlockingFeature != "" {
+				status.BlockingAmbiguity = []string{finding.BlockingFeature}
+			}
+		}
+		next := FlowNext{}
+		if cmd, _ := prescribePlanning(repo, status); cmd != nil {
+			next.Prescribed = cmd
+		}
+		planning := enumeratePlanningSolutions(repo, status, next)
+		set.Options, set.Truncated = planning.Options, planning.Truncated
+		return set
+
+	case finding.Category == "workflow-state-tamper":
+		// The state-ownership map already declares who may write the path; the
+		// pick list is the position observers plus the hook diagnosis, and the
+		// owning verbs surface separately (OwnerVerbs) — a verb whose full
+		// arguments we cannot derive is named, never fabricated into a command.
+		appendObserveOption(&set, repo, "", "delivery.next")
+		appendDiagnoseHook(&set, repo, host)
+		return set
+
+	case finding.Category == "workflow-publication-bypass":
+		if finding.BlockingFeature != "" {
+			if cmd, ok := prescribeCommand(repo, finding.BlockingFeature, NextStatus{ActiveSlice: finding.BlockingSlice}, PublishTransition); ok {
+				appendSolution(&set, *cmd)
+			}
+		}
+		appendObserveOption(&set, repo, finding.BlockingFeature, "delivery.recovery_status")
+		appendObserveOption(&set, repo, "", "delivery.next")
+		return set
+
+	case strings.HasPrefix(finding.Category, "operation-"):
+		// Observation-only by design: inspect the durable operation state before
+		// any retry (the observed-effect discipline).
+		appendSolution(&set, PrescribedCommand{
+			Verb: "operation-status", Args: repoFlagArgs(repo), AutoDerivable: true,
+			Transition: denialMarker("operation-status"),
+		})
+		appendSolution(&set, PrescribedCommand{
+			Verb: "mutation-status", Args: repoFlagArgs(repo), AutoDerivable: true,
+			Transition: denialMarker("mutation-status"),
+		})
+		return set
+
+	case finding.Category == "filesystem-destruction":
+		// The sanctioned actuator for the one deletion Boatstack owns; the
+		// operator confirmation is owed, never assumed.
+		appendSolution(&set, PrescribedCommand{
+			Verb: "workspace-reap", Args: repoFlagArgs(repo),
+			RequiresHumanInput: []string{"--confirm"},
+			Transition:         denialMarker("workspace-reap"),
+		})
+		appendDoctor(&set, repo)
+		appendObserveOption(&set, repo, "", "delivery.next")
+		return set
+	}
+
+	// Generic fallthrough (destruction families, sync bypass, anything new):
+	// the position observers and the installation diagnosis are always legal.
+	appendObserveOption(&set, repo, "", "delivery.next")
+	appendDoctor(&set, repo)
+	return set
+}
+
+// tamperOwnerVerbs derives the owning verbs of a protected path from the
+// state-ownership map: the guard-protected entry whose boatstack subtree the
+// attempted path names. Derived at runtime from StateRegistry — the same
+// declaration the statemap conformance holds to the guard patterns.
+// control-law: every-managed-path-has-a-declared-owner
+func tamperOwnerVerbs(repo, attempted string) []string {
+	if attempted == "" {
+		return nil
+	}
+	normalized := filepath_ToSlashLower(attempted)
+	w := WorkspaceFor(repo)
+	for _, entry := range StateRegistry() {
+		if !entry.GuardProtected {
+			continue
+		}
+		sample, err := entry.Sample(w)
+		if err != nil {
+			continue
+		}
+		key := boatstackSubtreeKey(filepath_ToSlashLower(sample))
+		if key != "" && strings.Contains(normalized, "boatstack/"+key) {
+			return entry.OwnerVerbs
+		}
+	}
+	return nil
+}
+
+// boatstackSubtreeKey extracts the first path segment after the last
+// "boatstack/" in a sample path — the subtree a guard-protected entry owns.
+func boatstackSubtreeKey(path string) string {
+	marker := "boatstack/"
+	index := strings.LastIndex(path, marker)
+	if index < 0 {
+		return ""
+	}
+	rest := path[index+len(marker):]
+	if cut := strings.IndexByte(rest, '/'); cut >= 0 {
+		return rest[:cut]
+	}
+	return rest
+}
+
+// filepath_ToSlashLower normalizes a path for fragment matching across
+// platforms and case conventions.
+func filepath_ToSlashLower(path string) string {
+	return strings.ToLower(strings.ReplaceAll(path, "\\", "/"))
+}
+
+func appendObserveOption(set *SolutionSet, repo, feature, transition string) {
+	descriptor, ok := deliverycontrol.Transition(deliverycontrol.TransitionID(transition))
+	if !ok {
+		return
+	}
+	if cmd, ok := prescribeObserve(repo, feature, descriptor); ok {
+		appendSolution(set, *cmd)
+	}
+}
+
+func appendDoctor(set *SolutionSet, repo string) {
+	appendSolution(set, PrescribedCommand{
+		Verb: "doctor", Args: repoFlagArgs(repo), AutoDerivable: true,
+		Transition: MarkerRecoveryDoctor,
+	})
+}
+
+func appendDiagnoseHook(set *SolutionSet, repo, host string) {
+	host = strings.ToLower(strings.TrimSpace(host))
+	if host == "" {
+		appendDoctor(set, repo)
+		return
+	}
+	appendSolution(set, PrescribedCommand{
+		Verb:          "diagnose-hook",
+		Args:          append([]string{"--host", host}, repoFlagArgs(repo)...),
+		AutoDerivable: true,
+		Transition:    denialMarker("diagnose-hook"),
+	})
+}
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/denial_solutions_conformance_test.go b/labs/12-product-engineering-loop/product-engineering-loop/denial_solutions_conformance_test.go
new file mode 100644
index 000000000..dfee3c8f4
--- /dev/null
+++ b/labs/12-product-engineering-loop/product-engineering-loop/denial_solutions_conformance_test.go
@@ -0,0 +1,193 @@
+package boatstack
+
+import (
+	"strings"
+	"testing"
+)
+
+// control-law: guard-never-prescribes-what-it-would-deny
+// control-law: solution-set-derives-from-guard-declarations
+//
+// Denial-basis conformance for the solution set. A denial that only states the
+// law leaves a weaker model looping on the same blocked call — the sibling
+// harness's paid canary recorded exactly that trajectory: sixteen no-progress
+// repair attempts escalating into a protected-boundary write. Every denial
+// therefore carries computed picks, and these sweeps hold that carrier total
+// (every category enumerates or is a documented exception) and closed (every
+// pick passes the guard's own text laws).
+
+// denialCategoryInventory is one representative finding per category
+// denialFor distinguishes, including the operation-* and generic fallthroughs.
+// Extend it together with denialFor; the totality sweep fails a category that
+// is neither enumerated nor excepted.
+var denialCategoryInventory = []SafetyFinding{
+	{Category: "malformed-tool-input", Reason: "empty-command", Source: "hook"},
+	{Category: "workflow-state-invalid", NextOperation: "discard-delivery", BlockingFeature: "stale", Source: "delivery-state"},
+	{Category: "workflow-state-tamper", Source: "delivery-state", AttemptedPath: ".git/boatstack/deliveries/demo/state.json"},
+	{Category: "workflow-phase-bypass", Source: "planning-state", WorkflowStage: "DRAFT_PLAN", NextOperation: "plan-gate", BlockingFeature: "demo"},
+	{Category: "workflow-phase-bypass", Source: "planning-state", WorkflowStage: "NOT_STARTED", NextOperation: "planning-write", AttemptedPath: ".product-loop/features/demo/plan.md"},
+	{Category: "workflow-publication-bypass", BlockingFeature: "demo", BlockingSlice: "s1", Source: "tool-input"},
+	{Category: "operation-in-flight", OperationID: "op_1", OperationState: "RUNNING", Source: "operation-state"},
+	{Category: "operation-already-succeeded", OperationID: "op_2", OperationState: "SUCCEEDED", Source: "operation-state"},
+	{Category: "operation-reconciliation-required", OperationID: "op_3", Source: "operation-state"},
+	{Category: "operation-retry-exhausted", OperationID: "op_4", Source: "operation-state"},
+	{Category: "operation-state-invalid", Source: "operation-state"},
+	{Category: "git-history-destruction", Source: "command"},
+	{Category: "workspace-sync-bypass", Source: "command"},
+	{Category: "filesystem-destruction", Source: "command"},
+	{Category: "database-destruction", Source: "command"},
+	{Category: "infrastructure-destruction", Source: "command"},
+	{Category: "external-resource-destruction", Source: "tool-input"},
+	{Category: "unsupported-host", Source: "hook"},
+	{Category: "unresolved-repository", Source: "hook"},
+	{Category: "symlink-entrypoint", Source: "entry.sh"},
+}
+
+// Totality: every denial category yields a non-empty solution set or sits on
+// the documented exception list with a reason.
+func TestEveryDenialCategoryEnumeratesOrIsExcepted(t *testing.T) {
+	for _, finding := range denialCategoryInventory {
+		set := enumerateDenialSolutions(".", "claude", finding)
+		if reason, excepted := denialSolutionExceptions[finding.Category]; excepted {
+			if reason == "" {
+				t.Errorf("exception for %s must carry a reason", finding.Category)
+			}
+			if len(set.Options) != 0 {
+				t.Errorf("%s is excepted but enumerates options — remove the stale exception", finding.Category)
+			}
+			continue
+		}
+		if len(set.Options) == 0 {
+			t.Errorf("category %s enumerates no options and is not a documented exception", finding.Category)
+		}
+	}
+}
+
+// Closure: every denial pick, after owed-input substitution, passes the
+// text-level guard laws — the managed-state path law and the destruction
+// classifier. The guard never hands out a command it would then deny as text.
+func TestDenialSolutionCommandsPassTheTextGuards(t *testing.T) {
+	for _, finding := range denialCategoryInventory {
+		set := enumerateDenialSolutions(".", "claude", finding)
+		for _, option := range set.Options {
+			line := substituteOwedFlags(option.CommandLine())
+			if deliveryStatePathPattern.MatchString(line) && !isPureReadOnlyCommand(line) && !approvedUpdatePublisherPattern.MatchString(line) {
+				t.Errorf("%s: pick %q names managed state the guard would deny", finding.Category, line)
+			}
+			if findings := classifySafetyText(line, "command", commandExecutesLiveSQL(line)); len(findings) > 0 {
+				t.Errorf("%s: pick %q trips the text guard: %+v", finding.Category, line, findings)
+			}
+			if option.AutoDerivable != (len(option.RequiresHumanInput) == 0) {
+				t.Errorf("%s: AutoDerivable must equal owed-input emptiness: %+v", finding.Category, option)
+			}
+			for _, owed := range option.RequiresHumanInput {
+				for _, arg := range option.Args {
+					if arg == owed {
+						t.Errorf("%s: owed flag %s fabricated into Args: %+v", finding.Category, owed, option)
+					}
+				}
+			}
+		}
+	}
+}
+
+// Relation: a phase-bypass denial's picks are exactly guard-admitted at the
+// finding's own stage — the same closure the flow basis holds, entered through
+// the denial door.
+func TestPhaseBypassDenialPicksAreGuardAdmitted(t *testing.T) {
+	finding := SafetyFinding{
+		Category: "workflow-phase-bypass", Source: "planning-state",
+		WorkflowStage: "DRAFT_PLAN", NextOperation: "plan-gate", BlockingFeature: "demo",
+	}
+	set := enumerateDenialSolutions(".", "claude", finding)
+	if len(set.Options) == 0 {
+		t.Fatal("phase-bypass must enumerate picks")
+	}
+	for _, option := range set.Options {
+		line := substituteOwedFlags(option.CommandLine())
+		if !controlledPhaseTransition(line, finding.WorkflowStage) {
+			t.Errorf("denial pick %q is not admitted at %s", line, finding.WorkflowStage)
+		}
+	}
+}
+
+// Ownership: a state-tamper denial names the attempted path's declared owner
+// verbs from the state-ownership map, and each named verb is a real one the
+// map declares for that subtree.
+func TestTamperDenialNamesDeclaredOwnerVerbs(t *testing.T) {
+	repo := safetyTestRepo(t)
+	cases := map[string][]string{
+		".git/boatstack/deliveries/demo/state.json":      {"activate-plan", "record-delivery-gate", "record-change", "publish-pr", "repair-state", "discard-delivery"},
+		".git/boatstack/updates/v9.9.9/pr-preview.json":  {"prepare-update-pr", "publish-update-pr"},
+		".git/boatstack/mutations/v1/abc.json":           {"activate-plan", "undo"},
+		".git/boatstack/quarantine/demo/receipt.json":    {"repair-state"},
+		"state-root/boatstack/registry.json":             {"attach", "detach"},
+		".git/boatstack/visual-evidence/x/manifest.json": {"record-pr-visual-evidence", "capture-evidence", "record-pr-visual-publication"},
+		"boatstack/repositories/sample/binding.json":     {"attach", "detach", "activate"},
+	}
+	for attempted, want := range cases {
+		got := tamperOwnerVerbs(repo, attempted)
+		if strings.Join(got, ",") != strings.Join(want, ",") {
+			t.Errorf("owner verbs for %s = %v, want %v", attempted, got, want)
+		}
+	}
+	if got := tamperOwnerVerbs(repo, ""); got != nil {
+		t.Errorf("empty attempted path must derive no owners, got %v", got)
+	}
+	if got := tamperOwnerVerbs(repo, "src/app.ts"); got != nil {
+		t.Errorf("unmanaged path must derive no owners, got %v", got)
+	}
+}
+
+// Rendering: the plain denial carries the capped "You can:" list; the
+// structured payload carries the full set additively under schema_version 1.
+func TestDenialRenderingCarriesTheSolutionSet(t *testing.T) {
+	finding := SafetyFinding{
+		Category: "workflow-phase-bypass", Source: "planning-state",
+		WorkflowStage: "DRAFT_PLAN", NextOperation: "plan-gate", BlockingFeature: "demo",
+	}
+	denial := denialWithOptions(".", "claude", finding)
+	if len(denial.Options) == 0 {
+		t.Fatal("denial must carry options")
+	}
+	for _, mode := range []RenderMode{RenderPlain, RenderMarkdown, RenderANSI} {
+		out := denial.Render(mode)
+		if !strings.Contains(strings.ToLower(out), "you can:") {
+			t.Errorf("mode %v must render the You can list:\n%s", mode, out)
+		}
+	}
+	plain := denial.Render(RenderPlain)
+	if got := strings.Count(plain, "\n  "); got > solutionSetTextCap+1 {
+		t.Errorf("plain rendering must cap the pick list, got %d lines:\n%s", got, plain)
+	}
+	structured := denial.Structured()
+	if structured["schema_version"] != 1 {
+		t.Fatalf("options are additive; schema_version must stay 1, got %v", structured["schema_version"])
+	}
+	options, ok := structured["options"].([]map[string]any)
+	if !ok || len(options) != len(denial.Options) {
+		t.Fatalf("structured options must carry the full set: %v", structured["options"])
+	}
+	for _, row := range options {
+		if row["command_line"] == "" || row["verb"] == "" || row["transition"] == "" {
+			t.Errorf("structured option incomplete: %v", row)
+		}
+	}
+
+	// Ownership derivation resolves per-worktree sample paths, which needs a
+	// real Git directory — the projected distribution runs these tests outside
+	// any repository, so the tamper case uses the git-backed fixture.
+	tamper := denialWithOptions(safetyTestRepo(t), "claude", SafetyFinding{
+		Category: "workflow-state-tamper", Source: "delivery-state",
+		AttemptedPath: ".git/boatstack/deliveries/demo/state.json",
+	})
+	if len(tamper.OwnerVerbs) == 0 {
+		t.Fatal("tamper denial must derive owner verbs")
+	}
+	if out := tamper.Render(RenderPlain); !strings.Contains(out, "This path is owned by: activate-plan") {
+		t.Errorf("tamper rendering must name the owners:\n%s", out)
+	}
+	if verbs, ok := tamper.Structured()["owner_verbs"].([]string); !ok || len(verbs) == 0 {
+		t.Errorf("structured tamper payload must carry owner_verbs")
+	}
+}
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/denial_test.go b/labs/12-product-engineering-loop/product-engineering-loop/denial_test.go
index 4f4aaaff1..f2c5517b7 100644
--- a/labs/12-product-engineering-loop/product-engineering-loop/denial_test.go
+++ b/labs/12-product-engineering-loop/product-engineering-loop/denial_test.go
@@ -154,7 +154,7 @@ func TestStructuredDenialObjectAndRichGate(t *testing.T) {
 
 	// Rich object is gated off by default; the flat reason stays complete.
 	t.Setenv("BOATSTACK_DENIAL_RICH", "")
-	out, err := structuredHookDeny("claude", finding)
+	out, err := structuredHookDeny(".", "claude", finding)
 	if err != nil {
 		t.Fatal(err)
 	}
@@ -172,7 +172,7 @@ func TestStructuredDenialObjectAndRichGate(t *testing.T) {
 
 	// Opt-in adds the object while keeping the flat reason.
 	t.Setenv("BOATSTACK_DENIAL_RICH", "1")
-	out, err = structuredHookDeny("claude", finding)
+	out, err = structuredHookDeny(".", "claude", finding)
 	if err != nil {
 		t.Fatal(err)
 	}
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/safety.go b/labs/12-product-engineering-loop/product-engineering-loop/safety.go
index f17686393..d0f85b628 100644
--- a/labs/12-product-engineering-loop/product-engineering-loop/safety.go
+++ b/labs/12-product-engineering-loop/product-engineering-loop/safety.go
@@ -807,7 +807,10 @@ func ClassifyCommand(repo, command string) []SafetyFinding {
 		return []SafetyFinding{{Category: "malformed-tool-input", Reason: "empty-command", Source: "tool-input"}}
 	}
 	if deliveryStatePathPattern.MatchString(command) && !isPureReadOnlyCommand(command) && !approvedUpdatePublisherPattern.MatchString(command) {
-		return []SafetyFinding{{Category: "workflow-state-tamper", Reason: "managed delivery state may be changed only by Boatstack transitions", Source: "delivery-state"}}
+		// AttemptedPath carries the matched managed-path fragment (bounded and
+		// secret-free, like the phase-bypass finding) so the denial can name the
+		// path's declared owner verbs from the state-ownership map.
+		return []SafetyFinding{{Category: "workflow-state-tamper", Reason: "managed delivery state may be changed only by Boatstack transitions", Source: "delivery-state", AttemptedPath: deliveryStatePathPattern.FindString(command)}}
 	}
 	if directPublicationPattern.MatchString(command) && !approvedPublisherPattern.MatchString(command) {
 		if finding, blocked := publicationBypassFinding(repo, "direct push or PR mutation is denied while a managed delivery slice is active", "tool-input"); blocked {
@@ -895,7 +898,7 @@ func ClassifyTool(repo, name string, input any) []SafetyFinding {
 	}
 	publicationText := strings.ToLower(combined)
 	if deliveryStatePathPattern.MatchString(combined) && regexp.MustCompile(`(?:write|edit|delete|remove|move|rename|create|update)`).MatchString(nameLower) {
-		findings = append(findings, SafetyFinding{Category: "workflow-state-tamper", Reason: "managed delivery state may be changed only by Boatstack transitions", Source: "delivery-state"})
+		findings = append(findings, SafetyFinding{Category: "workflow-state-tamper", Reason: "managed delivery state may be changed only by Boatstack transitions", Source: "delivery-state", AttemptedPath: deliveryStatePathPattern.FindString(combined)})
 	}
 	if (strings.Contains(publicationText, "pull_request") || strings.Contains(publicationText, "pull request")) &&
 		regexp.MustCompile(`(?:create|update|edit|merge|publish)`).MatchString(publicationText) {
@@ -1121,7 +1124,10 @@ func dedupeFindings(values []SafetyFinding) []SafetyFinding {
 type hookHostContract struct {
 	decode func([]byte) (string, any, error)
 	allow  func() ([]byte, error)
-	deny   func(SafetyFinding) ([]byte, error)
+	// deny takes the resolved repository so the denial can carry its computed
+	// solution set (empty when the repository could not be resolved).
+	// control-law: solution-set-derives-from-guard-declarations
+	deny func(repo string, finding SafetyFinding) ([]byte, error)
 }
 
 func decodeJSONObject(host string, value []byte) (map[string]any, error) {
@@ -1259,17 +1265,17 @@ func decodeGeminiHook(value []byte) (string, any, error) {
 	return name, input, nil
 }
 
-func structuredHookDeny(host string, finding SafetyFinding) ([]byte, error) {
-	message := denialMessage(host, finding)
+func structuredHookDeny(repo, host string, finding SafetyFinding) ([]byte, error) {
+	denial := denialWithOptions(repo, host, finding)
 	hookOutput := map[string]any{
-		"hookEventName": "PreToolUse", "permissionDecision": "deny", "permissionDecisionReason": message,
+		"hookEventName": "PreToolUse", "permissionDecision": "deny", "permissionDecisionReason": denial.Render(RenderPlain),
 	}
 	// Opt-in structured object for hosts that adopt rich denial rendering. Nested
 	// inside the host's existing container; the flat reason above is always the
 	// complete fallback for any host that ignores it. Off by default (no host
 	// documents tolerating unknown keys — see references/host-hook-contracts.md).
 	if denialRichEnabled() {
-		hookOutput["boatstackDenial"] = denialFor(host, finding).Structured()
+		hookOutput["boatstackDenial"] = denial.Structured()
 	}
 	value, err := json.Marshal(map[string]any{"hookSpecificOutput": hookOutput})
 	return append(value, '\n'), err
@@ -1282,13 +1288,14 @@ var hookHostContracts = map[string]hookHostContract{
 			value, err := json.Marshal(map[string]any{"continue": true, "permission": "allow"})
 			return append(value, '\n'), err
 		},
-		deny: func(finding SafetyFinding) ([]byte, error) {
-			message := denialMessage("cursor", finding)
+		deny: func(repo string, finding SafetyFinding) ([]byte, error) {
+			denial := denialWithOptions(repo, "cursor", finding)
+			message := denial.Render(RenderPlain)
 			payload := map[string]any{
 				"continue": true, "permission": "deny", "user_message": message, "agent_message": message,
 			}
 			if denialRichEnabled() {
-				payload["boatstackDenial"] = denialFor("cursor", finding).Structured()
+				payload["boatstackDenial"] = denial.Structured()
 			}
 			value, err := json.Marshal(payload)
 			return append(value, '\n'), err
@@ -1297,12 +1304,16 @@ var hookHostContracts = map[string]hookHostContract{
 	"claude": {
 		decode: func(value []byte) (string, any, error) { return decodePreToolUseHook("claude", value) },
 		allow:  func() ([]byte, error) { return nil, nil },
-		deny:   func(finding SafetyFinding) ([]byte, error) { return structuredHookDeny("claude", finding) },
+		deny: func(repo string, finding SafetyFinding) ([]byte, error) {
+			return structuredHookDeny(repo, "claude", finding)
+		},
 	},
 	"codex": {
 		decode: func(value []byte) (string, any, error) { return decodePreToolUseHook("codex", value) },
 		allow:  func() ([]byte, error) { return nil, nil },
-		deny:   func(finding SafetyFinding) ([]byte, error) { return structuredHookDeny("codex", finding) },
+		deny: func(repo string, finding SafetyFinding) ([]byte, error) {
+			return structuredHookDeny(repo, "codex", finding)
+		},
 	},
 	"gemini": {
 		decode: decodeGeminiHook,
@@ -1310,10 +1321,11 @@ var hookHostContracts = map[string]hookHostContract{
 			value, err := json.Marshal(map[string]any{"decision": "allow"})
 			return append(value, '\n'), err
 		},
-		deny: func(finding SafetyFinding) ([]byte, error) {
-			payload := map[string]any{"decision": "deny", "reason": denialMessage("gemini", finding)}
+		deny: func(repo string, finding SafetyFinding) ([]byte, error) {
+			denial := denialWithOptions(repo, "gemini", finding)
+			payload := map[string]any{"decision": "deny", "reason": denial.Render(RenderPlain)}
 			if denialRichEnabled() {
-				payload["boatstackDenial"] = denialFor("gemini", finding).Structured()
+				payload["boatstackDenial"] = denial.Structured()
 			}
 			value, err := json.Marshal(payload)
 			return append(value, '\n'), err
@@ -1322,12 +1334,13 @@ var hookHostContracts = map[string]hookHostContract{
 }
 
 // denialMessage renders the human-facing reason string embedded in a host's hook
-// decision. It delegates to the structured Denial model (denial.go) and renders
-// the plain, multi-line form — the safe default that every host displays. Richer
-// treatments (markdown, ANSI, the structured object) are produced from the same
-// Denial by the CLI/guard surfaces and the opt-in rich path.
-func denialMessage(host string, finding SafetyFinding) string {
-	return denialFor(host, finding).Render(RenderPlain)
+// decision. It delegates to the structured Denial model (denial.go) — including
+// the finding's computed solution set — and renders the plain, multi-line form,
+// the safe default that every host displays. Richer treatments (markdown, ANSI,
+// the structured object) are produced from the same Denial by the CLI/guard
+// surfaces and the opt-in rich path.
+func denialMessage(repo, host string, finding SafetyFinding) string {
+	return denialWithOptions(repo, host, finding).Render(RenderPlain)
 }
 
 // AmbientHookDecision is the entry point for a developer-level (user-scoped) guard
@@ -1355,19 +1368,19 @@ func HookDecision(options SafetyHookOptions) ([]byte, bool) {
 	contract, supported := hookHostContracts[host]
 	if !supported {
 		finding := SafetyFinding{Category: "unsupported-host", Reason: "unknown host is denied by the fail-closed guard", Source: "hook"}
-		value, _ := structuredHookDeny("codex", finding)
+		value, _ := structuredHookDeny("", "codex", finding)
 		return value, true
 	}
 	repo, err := ResolveRepository(options.Repo)
 	if err != nil {
 		finding := SafetyFinding{Category: "unresolved-repository", Reason: "repository identity could not be established", Source: "hook"}
-		value, _ := contract.deny(finding)
+		value, _ := contract.deny("", finding)
 		return value, true
 	}
 	if handled, malformed := completeSupervisedToolEvent(repo, host, options.Input); handled {
 		if malformed {
 			finding := SafetyFinding{Category: "malformed-tool-input", Reason: "invalid-post-event", Source: "hook"}
-			value, _ := contract.deny(finding)
+			value, _ := contract.deny(repo, finding)
 			return value, true
 		}
 		value, _ := contract.allow()
@@ -1381,19 +1394,19 @@ func HookDecision(options SafetyHookOptions) ([]byte, bool) {
 			reason = decodeErr.code
 		}
 		finding := SafetyFinding{Category: "malformed-tool-input", Reason: reason, Source: "hook"}
-		value, _ := contract.deny(finding)
+		value, _ := contract.deny(repo, finding)
 		return value, true
 	}
 	findings := ClassifyTool(repo, name, input)
 	if len(findings) == 0 {
 		if finding := superviseToolAttempt(repo, host, name, input, options.Input); finding != nil {
-			value, _ := contract.deny(*finding)
+			value, _ := contract.deny(repo, *finding)
 			return value, true
 		}
 		value, _ := contract.allow()
 		return value, false
 	}
-	value, _ := contract.deny(findings[0])
+	value, _ := contract.deny(repo, findings[0])
 	return value, true
 }
 
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/safety_corpus_test.go b/labs/12-product-engineering-loop/product-engineering-loop/safety_corpus_test.go
index 633f2cf3f..c5f786ce6 100644
--- a/labs/12-product-engineering-loop/product-engineering-loop/safety_corpus_test.go
+++ b/labs/12-product-engineering-loop/product-engineering-loop/safety_corpus_test.go
@@ -109,10 +109,19 @@ func TestGuardCorpusDualReward(t *testing.T) {
 			"content":   "Delivery state lives under `.git/boatstack/deliveries/` and is owned by the helper.",
 		}, "routine", false},
 		{"edit-note-mentions-git-reset", "Edit", map[string]any{
-			"file_path": filepath.Join(repo, "notes.md"),
+			"file_path":  filepath.Join(repo, "notes.md"),
 			"old_string": "TODO",
 			"new_string": "Never run `git reset --hard` on shared branches; use revert PRs.",
 		}, "routine", false},
+		// Solution-set picks: commands the guard itself enumerates as legal moves
+		// at THIS fixture's stage must pass the guard
+		// (guard-never-prescribes-what-it-would-deny). Stage-scoped picks like
+		// record-approval are held in their own fixture by the closure sweep.
+		{"pick-undo", "", `boatstack-helper undo --mutation abc123`, "routine", false},
+		{"pick-discard-delivery", "", `boatstack-helper discard-delivery --feature stale`, "routine", false},
+		{"pick-operation-status", "", `boatstack-helper operation-status`, "routine", false},
+		{"pick-record-change", "", `boatstack-helper record-change --feature demo --slice s1 --message fix --source-stage ci --classification implementation_repair`, "routine", false},
+		{"pick-next-status", "", `boatstack-helper next-status`, "routine", false},
 	}
 
 	var constTotal, constBlocked, routineTotal, routinePassed int
diff --git a/labs/12-product-engineering-loop/product-engineering-loop/safety_test.go b/labs/12-product-engineering-loop/product-engineering-loop/safety_test.go
index e92164541..9b127030b 100644
--- a/labs/12-product-engineering-loop/product-engineering-loop/safety_test.go
+++ b/labs/12-product-engineering-loop/product-engineering-loop/safety_test.go
@@ -100,7 +100,7 @@ func TestReapHelperIsExemptWhileRawWorktreeRemovalStaysDenied(t *testing.T) {
 	if len(rawFilesystem) == 0 || rawFilesystem[0].Category != "filesystem-destruction" {
 		t.Fatalf("raw worktree deletion was not denied: %#v", rawFilesystem)
 	}
-	if message := denialMessage("cursor", rawFilesystem[0]); !strings.Contains(message, "workspace-reap") {
+	if message := denialMessage(".", "cursor", rawFilesystem[0]); !strings.Contains(message, "workspace-reap") {
 		t.Fatalf("filesystem-destruction denial should redirect to workspace-reap: %s", message)
 	}
 
@@ -109,7 +109,7 @@ func TestReapHelperIsExemptWhileRawWorktreeRemovalStaysDenied(t *testing.T) {
 	if len(rawState) == 0 || rawState[0].Category != "workflow-state-tamper" {
 		t.Fatalf("raw runtime-state deletion was not denied: %#v", rawState)
 	}
-	if message := denialMessage("cursor", rawState[0]); !strings.Contains(message, "workspace-reap") {
+	if message := denialMessage(".", "cursor", rawState[0]); !strings.Contains(message, "workspace-reap") {
 		t.Fatalf("workflow-state-tamper denial should mention workspace-reap: %s", message)
 	}
 }
@@ -142,7 +142,7 @@ func TestWorkspaceSyncIsTheOnlyAllowedRepositoryAlignmentCommand(t *testing.T) {
 	if len(raw) == 0 || raw[0].Category != "git-history-destruction" {
 		t.Fatalf("raw hard reset was not denied: %#v", raw)
 	}
-	message := denialMessage("cursor", raw[0])
+	message := denialMessage(".", "cursor", raw[0])
 	for _, expected := range []string{"project-local workspace-sync", "do not scan delivery artifacts", "do not", "retry"} {
 		if !strings.Contains(message, expected) {
 			t.Fatalf("hard-reset denial omitted %q: %s", expected, message)