Add bounded agent workflow planning and evidence guidance

.github/workflows/release.yml

@@ -467,7 +467,7 @@ jobs:
             ["schemaVersion", 1],
             ["artifactKind", "proofkit.json-report-cli-adapter-source"],
             ["format", "json"],
-            ["generatorId", "proofkit.json-report-cli-adapter-source.typescript.v1"],
+            ["generatorId", "proofkit.json-report-cli-adapter-source.typescript.v2"],
             ["language", "typescript"],
             ["sourceFileName", "proofkit-json-report-cli-adapter.ts"]
           ]) {

cmd/agentic-proofkit/main.go

@@ -2,11 +2,12 @@ package main
 
 import (
 	"context"
-	"fmt"
 	"os"
 
+	"github.com/mattn/go-isatty"
 	"github.com/research-engineering/agentic-proofkit/internal/app"
 	"github.com/research-engineering/agentic-proofkit/internal/kernel/cliexec"
+	"github.com/research-engineering/agentic-proofkit/internal/kernel/diagnostic"
 )
 
 func main() {
@@ -15,8 +16,13 @@ func main() {
 		os.Getenv(cliexec.PythonExecutableEnvironment),
 	)
 	if err != nil {
-		_, _ = fmt.Fprintln(os.Stderr, err)
+		diagnostic.WriteError(os.Stderr, err)
 		os.Exit(1)
 	}
-	os.Exit(app.RunWithRenderer(context.Background(), os.Args[1:], os.Stdin, os.Stdout, os.Stderr, renderer))
+	_, noColorPresent := os.LookupEnv("NO_COLOR")
+	capabilities := app.PresentationCapabilities{
+		StdoutIsTTY:    isatty.IsTerminal(os.Stdout.Fd()) || isatty.IsCygwinTerminal(os.Stdout.Fd()),
+		NoColorPresent: noColorPresent,
+	}
+	os.Exit(app.RunWithRendererAndCapabilities(context.Background(), os.Args[1:], os.Stdin, os.Stdout, os.Stderr, renderer, capabilities))
 }

docs/proofkit-contract-map.md

@@ -39,6 +39,7 @@ owner boundaries. It is not a second command-family inventory.
 
 | Family | Main commands | Caller provides | Proofkit owns | Consumer owns | Output authority |
 |---|---|---|---|---|---|
+| Agent workflow planning | `change-workflow-plan`, `native-evidence-guidance` | explicit checkpoint, completed stage ids, bounded context refs, governing authority ref, and required context ref ids | optional built-in `proofkit.reviewed-change.v1` checkpoint relation, reference-closed next-stage context, deterministic agent prompts, bounded text/JSON/envelope projections, and repository-neutral native-evidence guidance with closed applicability classes | custom workflow topology, repository state discovery, stage execution, native witness semantics, evidence collection, review conclusions, merge, release, deployment, and rollout authority | next-action plan, terminal workflow report, bounded agent envelope, or guidance catalog |
 | Adoption and scaffolding | `init`, `adoption-contract-envelope`, `adoption-workflow-plan`, `adoption-checklist`, `adoption-doctor`, `gradual-adoption`, `gradual-adoption-bootstrap`, `gradual-adoption-guidance`, `capability-map-admission`, `pilot-admission`, `scaffold-profile-plan`, `scaffold-project-structure`, `stack-preset` | adoption intent, aggregate adoption contract envelope, checklist facts, target paths, owner routes, caller-extracted stale authority vocabulary facts, explicit pre-spec capability observations, pilot records, stack preset id, optional init preset id | dry-run route selection, aggregate contract-envelope admission, deterministic starter plans, checklist/report admission, bounded guidance envelopes, dry-run manifests, pre-spec trust-mode admission, adoption gap and stale-authority classification, pilot shape admission | final files, final requirements, rollout policy, text extraction from files, code observation extraction, pilot truth | selected child output, plan, report, seed packet, or agent envelope |
 | Requirement source | `capability-map-admission`, `requirement-authoring-plan`, `requirement-source-admission`, `requirement-source-transition`, `spec-overview-claims`, `requirement-spec-tree`, `requirement-spec-tree-view`, `requirement-source-view`, `requirement-browser-server` | `requirements.v1.json`, caller-owned capability maps, caller-owned authoring facts, overview claim extraction, explicit spec hierarchy, view options | candidate seed admission, candidate-only authoring packets, source-shape admission, lifecycle checks, explicit tree topology/source-ref admission, shared safe renderer fragments, presentation-only views | requirement meaning, extraction completeness, Markdown extraction completeness, hierarchy ownership, proof adequacy, file materialization | capability map report, authoring packet, source report, spec-tree report, rendered view, or browser presentation |
 | Requirement proof binding | `requirement-bindings`, `binding-partition`, `proof-slice`, `evidence-graph`, `requirement-proof-resolver`, `requirement-proof-source-set`, `requirement-proof-view`, `spec-proof-bundle-admission` | requirement records, bindings, witness commands, source-set facts, receipt reports, partition policy | graph validation, binding partition projection, compact slices, declaration-only compact route projection with full binding identity and role-qualified witness routes, resolver projection, bundle linkage checks | selector resolution, oracle quality, witness execution, mutation adequacy, finding completeness, proof freshness, trust, assurance, merge policy | proof report, partition report, slice, declaration lookup graph, or view |
@@ -122,6 +123,7 @@ Semantic context routes are `requirement-context-compose`,
 | State or goal | Next Proofkit route | Stop or escalation condition |
 |---|---|---|
 | The agent does not know where to start. | `init`, or `init --preset` with `fresh`, `code-baseline`, `code-audit`, `legacy`, or `change-set` | Treat output as dry-run route guidance only. Stop before scanning, writing files, or making requirements authoritative. |
+| An agent needs a bounded, deterministic stage transition for an engineering change. | `change-workflow-plan` selects the optional built-in `proofkit.reviewed-change.v1` profile; use `--agent-envelope` for the compact work packet and `native-evidence-guidance` when the consuming repository has not yet materialized repository-specific evidence instructions. | Supply only explicit current checkpoint, completed stages, and admitted context references. Apply conditional guidance slots only when their applicability class matches a declared consumer mechanism. Stop before treating the profile, plan, or guidance as repository policy or as proof that a stage ran, evidence exists, review passed, or merge/release is authorized. |
 | No admitted spec/profile exists and the caller has explicit capability observations. | `capability-map-admission`; use `trustMode: "code_baseline"` only when maintainers intentionally freeze current code, otherwise use `trustMode: "audit_from_code"`. | Stop before treating seeds as stable requirements. The consumer owns observation extraction, materialization, requirement meaning, and proof adequacy. |
 | No admitted spec/profile exists and no capability observations exist. | `scaffold-project-structure`, `adoption-workflow-plan`, or `stack-preset` | Stop before writing files; the consumer owns materialization, overwrite policy, and final requirement text. |
 | Candidate boundary is uncertain. | `adoption-doctor` or `gradual-adoption-guidance --agent-envelope` | Escalate to owner review when the boundary is advisory, ambiguous, or missing native witnesses. |

docs/specs/proofkit-agent-workflow/overview.md

@@ -0,0 +1,86 @@
+# Proofkit Agent Workflow Spec
+
+This spec owns Proofkit's generic support for planning one engineering-change
+snapshot and for teaching a consuming repository to define executable native
+evidence. It does not own consumer product meaning, repository policy,
+witnesses, merge, release, rollout, or production-readiness decisions.
+
+The public capability is deliberately small:
+
+1. `change-workflow-plan` admits explicit JSON and projects one next action for
+   the optional built-in profile `proofkit.reviewed-change.v1`, whose ordered
+   stages are `architecture`, `design`, `implementation_plan`,
+   `implementation`, `verification`, `pull_request`, and `closeout`.
+2. `native-evidence-guidance` exposes one versioned 22-slot template for
+   repository-owned falsifiers, oracles, bounds, lifecycle, and non-claims.
+   Every slot names one closed applicability class: `always`,
+   `declared_input_channels`, `environment_or_network_access`,
+   `external_process`, or `mutable_artifacts`. The latter four apply only when
+   the consuming witness declares the named mechanism.
+3. Existing descriptors, dispatch, command families, root-shape CLI contracts,
+   agent envelopes, and package gates provide public-surface closure.
+
+Neither command scans a repository. Both command cores are stateless pure
+projections with no filesystem, Git, process, environment, clock, random,
+network, container, or provider dependency. No setup facade, agent-route extension,
+external prompt resource, persisted experiment state, or second source codec is
+introduced.
+
+## Requirements
+
+- `REQ-PROOFKIT-WORKFLOW-001`: one-time typed admission, pure deterministic
+  projection, and derived-output authority boundary.
+- `REQ-PROOFKIT-WORKFLOW-002`: named optional built-in profile, exact
+  seven-stage order, prefix/checkpoint biconditional, and a disjoint terminal
+  output.
+- `REQ-PROOFKIT-WORKFLOW-003`: 28 active state rows, one terminal row,
+  authority- and witness-gated executable envelope transitions, closed
+  blockers and clarifications when those preconditions are absent, exact
+  accepted-subject carry into each nonterminal successor, and an explicit
+  terminal stop packet.
+- `REQ-PROOFKIT-WORKFLOW-004`: typed subject/finding resolution, incoming
+  subject identity on every noninitial stage, and internally consistent
+  caller-declared digests.
+- `REQ-PROOFKIT-WORKFLOW-005`: shared 256-byte stable-ID admission before work,
+  global candidate-dependency resolution, one explicit nullable
+  governing-authority reference, role-preserving bounded least dependency
+  closure over explicit seeds, exact omission accounting, and output-byte
+  limits.
+- `REQ-PROOFKIT-WORKFLOW-006`: only existing launcher and presentation
+  capabilities outside explicit input, with no ambient repository authority,
+  setup facade, hidden policy, or agent-route extension.
+- `REQ-PROOFKIT-WORKFLOW-007`: pure deterministic repository-neutral
+  native-evidence guidance from one versioned typed table with five closed
+  applicability classes, explicit absent-channel decisions, and finite
+  nondisclosure corpora.
+- `REQ-PROOFKIT-WORKFLOW-008`: display-safe caller admission, no-leak denial,
+  exact retained-or-missing witness projection, bounded actionable and
+  terminal text with required coordinates and exact rendered successor delta,
+  and no styling of caller values.
+- `REQ-PROOFKIT-WORKFLOW-009`: explicit text/color selection and confinement of
+  ANSI to eligible terminal stdout.
+- `REQ-PROOFKIT-WORKFLOW-010`: one production catalog owner for stage,
+  checkpoint-schema, action-prerequisite, and successor semantics,
+  independently authored semantic and literal-duplication oracles, and an
+  AST-checked two-command carrier topology with no runtime experiment or
+  external template residue.
+- `REQ-PROOFKIT-WORKFLOW-011`: a finite factorized CLI relation closed across
+  descriptor/dispatcher/family/help/root-contract/witness/generated/package
+  surfaces, with npm-only non-runtime specification docs and cross-channel
+  runtime behavior proof.
+
+Shared stable-JSON/diagnostic hardening is owned by the supply-chain-quality
+spec. Typed local-reference closure is owned by the existing agent-envelope
+requirement. This workflow spec consumes those owners without duplicating them.
+
+## Non-Claims
+
+- Generated prompts are not authenticated and need not be obeyed or adequate.
+- The built-in reviewed-change profile is optional guidance, not universal
+  consuming-repository process policy or a custom workflow-graph engine.
+- Static prompt bytes do not prove provider token use or model reasoning.
+- Least dependency closure does not prove context truth, freshness, semantic
+  sufficiency, or global minimality.
+- A finite pilot does not prove universal repository fit.
+- This spec does not select a persisted requirement-source codec.
+- This spec does not approve merge, release, rollout, or production readiness.