Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 7 additions & 3 deletions plugins/formal-model-check/stages/formal-model-check.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
7 changes: 6 additions & 1 deletion plugins/pr-convergence/stages/pr-convergence.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading