diff --git a/plugins/formal-model-check/stages/formal-model-check.md b/plugins/formal-model-check/stages/formal-model-check.md index 1d75e232f3..fd0986d06a 100644 --- a/plugins/formal-model-check/stages/formal-model-check.md +++ b/plugins/formal-model-check/stages/formal-model-check.md @@ -24,9 +24,13 @@ an exhaustive TLC exploration of a declared TLA+ model, driven by the the opt-in boundary, so once composed it is reachable via `amadeus-orchestrate next --stage formal-model-check` — `--single` optional (U6 activation-policy, FR-7(a)). It never joins a stock scope's workflow and -never runs on `push` / `pull_request`. Amadeus never runs it automatically: the -engine only emits a spec-hash advisory nudge when the watched spec changed -(ADR-1 option A, U6). +never runs on `push` / `pull_request`. When the watched spec changed, the +engine emits a spec-hash advisory nudge (ADR-1 option A, U6); whether that +advisory starts a run depends on the Intent autonomy mode: under `none` a +human decides whether to run it; under `semi` or `full` the advisory is routed +through the autonomy ladder as a `question` occurrence +(`amadeus-advisory-choice.ts`), and a `run-now` decision starts the check +unattended — any other ladder outcome falls back to the human. ## Stage body diff --git a/plugins/pr-convergence/stages/pr-convergence.md b/plugins/pr-convergence/stages/pr-convergence.md index 30512ff4dd..d613c22b0b 100644 --- a/plugins/pr-convergence/stages/pr-convergence.md +++ b/plugins/pr-convergence/stages/pr-convergence.md @@ -24,7 +24,12 @@ no merge conflict, every required check green, and every actionable review thread terminalised. It is an opt-in plugin stage (empty `scopes:`) — install is the opt-in boundary, so once composed it is reachable via `amadeus-orchestrate next --stage pr-convergence`. It never joins a stock -scope's workflow and Amadeus never runs it automatically. +scope's workflow. Whether a run starts depends on the Intent autonomy mode: +under `none` a human decides when to start it; under `semi` or `full`, an +engine advisory raised for this plugin is routed through the autonomy ladder +as a `question` occurrence (`amadeus-advisory-choice.ts`), and a `run-now` +decision can start it unattended — any other ladder outcome falls back to the +human. Installing the plugin also overlays `pr-convergence-report` onto the `code-generation` stage's `produces`. From that point the existing per-unit