monad-developers · aviggiano · Sep 30, 2026 · Sep 29, 2026 · Sep 29, 2026 · Sep 29, 2026
diff --git a/.ultrafuzz/prompts/properties/property-specification-fanin.md b/.ultrafuzz/prompts/properties/property-specification-fanin.md
@@ -26,21 +26,25 @@ Base test setup:
 
 ## 1. Consolidate
 
-Consolidate properties from every topology-required lens JSON into a single
+Consolidate properties from every lens JSON selected below into a single
 catalog. Each lens emits one `ultrafuzz/property-lens@2` output. Read and
 validate every selected lens JSON; it is the machine-readable source of truth.
 Use `{{schema_path}}/property-lens.schema.json` to validate each source catalog
 and assign every retained priority as `high`, `medium`, or `low`.
 
-Sealed JSON authority for every declared ancestor property-lens artifact:
+Sealed JSON authority for every ancestor property-lens artifact that passed
+verification:
 
 {{ancestor_contract_artifact_authority:ultrafuzz/property-lens@2}}
 
 Read the manifest definition instead of expecting an expanded lens path or
 source array in this prompt. Use each selected producer task's exact
 `logical_node_id` as `source_node_id`, and retain the selector's required
 run-relative `localeCompare` order. Do not infer a source from a Markdown
-companion, hard-coded lens list, or same-named workspace file.
+companion, hard-coded lens list, or same-named workspace file. A lens that did
+not pass verification is absent from this authority: consolidate the lenses it
+selects, and do not recreate a missing lens's properties from its reference
+material or from memory.
 
 Deduplicate equivalent properties across artifacts. When in doubt, err on the side of retaining multiple similar properties rather than risk removing one that represents a distinct concept or carries different meaning.
 
@@ -66,11 +70,11 @@ property with every distinct contributing source in `sources`. Never keep only
 the first source. Canonical IDs only need to remain stable within this run, but
 all downstream artifacts must use them unchanged.
 
-Coverage of the lens artifacts is total and machine-checked. Every property ID
-in every lens artifact must appear exactly once across the whole catalog as a
-source-node/property-ID pair in some canonical property's `sources`: the runtime rejects a lens ID that
-appears in no canonical property and rejects the same pair listed on two
-canonical properties. Deduplicating two rows therefore means listing both source
+Coverage of the selected lens artifacts is total and machine-checked. Every
+property ID in every selected lens artifact must appear exactly once across the
+whole catalog as a source-node/property-ID pair in some canonical property's
+`sources`: the runtime rejects a lens ID that appears in no canonical property
+and rejects the same pair listed on two canonical properties. Deduplicating two rows therefore means listing both source
 pairs on the one merged canonical property, never dropping one. You may not drop
 a lens row because it duplicates wording inside its own lens, reads as
 non-testable, or looks out of scope; merge it into the canonical property it

diff --git a/.ultrafuzz/topology.yml b/.ultrafuzz/topology.yml
@@ -8,6 +8,11 @@ groups:
   properties:
     label: Properties
     color: "#a16207"
+    defaults:
+      failure_policy: continue
+  property-catalog:
+    label: Property catalog
+    color: "#854d0e"
   goals:
     label: Threat goals
     color: "#be123c"
@@ -426,7 +431,7 @@ nodes:
   - id: property-specification-fanin
     kind: agentic
     prompt: properties/property-specification-fanin.md
-    group: properties
+    group: property-catalog
     depends_on:
       - property-specification-certora
       - property-specification-crytic

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,8 @@
 
 ### Breaking changes
 
+- **[config] [runtime] [prompts] [docs]** A property lens that fails no longer stops the campaign. The packaged `default` topology, which `ultrafuzz init` scaffolds, and the packaged `exhaustive` and `invariant-only` topologies change: their `properties` group now has `failure_policy: continue`, and `property-specification-fanin` moves to a new `property-catalog` group, which still halts. The fan-in consolidates the lenses that passed verification, and the strategies, specialists and review run without the failed lens's properties. The report is PARTIAL when the lens ran out of attempts and unverified when it failed its output contract, unless a later `resume --retry-failed` reruns the lens successfully. That resume, which Modal's durable resume always runs, reruns the failed lens, and when the lens's artifact verifier failed, also every node that started after the lens's attempt, which is most of the campaign. In `exhaustive`, `dynamic-strategy-generator` now also runs when some strategy attempts failed, using the ones that succeeded, instead of being skipped. The fan-in, strategies and specialists now have optional inputs, so when the artifact verifier of one of them fails, `state.json` no longer records `output_contracts.missing` or `terminal_disposition: task-output-validation-failure` for it and public eval diagnostics omit its `failure_code`; the verifier's error stays in `last_error`, as it already did for review tasks. The `exhaustive` and `invariant-only` profiles use the new topology after the upgrade. The `default` and `low-cost` profiles run the project's own `.ultrafuzz/topology.yml`, so an existing project keeps the old behaviour there, where one failed lens fails the run before any strategy starts and leaves it without a report, until you make three edits to that file: add `defaults: {failure_policy: continue}` to the `properties` group; add a `property-catalog` group with no `failure_policy` (the scaffold gives it `label: Property catalog` and `color: "#854d0e"`); and change the `property-specification-fanin` node's `group` from `properties` to `property-catalog`. If you have not customized that file, `ultrafuzz topology copy default .ultrafuzz/topology.yml --force` replaces it with the new default instead. Every existing project, whichever profile it runs, should also delete `.ultrafuzz/prompts/properties/property-specification-fanin.md` and rerun `ultrafuzz init`: a project prompt overrides the built-in one under every profile, and only the new prompt tells the fan-in to consolidate the lenses it is given instead of every lens in the topology.
+- **[runtime] [docs]** A `failure_policy: continue` group's results are now optional to every node outside that group, including nodes with no `group` and the nodes a dynamic group generates, not only to the group named `review`. Such a node runs without a failed input instead of being skipped, while nodes in the same group still require it. A node that reaches a failed ancestor of its own group only through another group, such as strategy `s2` after specialist `x` after strategy `s1`, now fails its input admission instead of being skipped; that is an `artifact-contract` failure, so the run's report is published unverified. To keep a chain strict, put all of it in one group.
 - **[runtime] [docs]** A final-report producer retry or verifier that runs in a restarted controller (resume, quota park, supervisor relaunch) now rebuilds `report.json#run_metadata.agent_execution` from `smithers/final-report-selections/<attempt-id>.json` in the run directory, which each producer attempt writes just before starting its agent, instead of running `smithers node` as a subprocess (a `--full-output` read of up to 64 MiB under a 180 s budget). This applies to workflows rendered by this release, at launch or by `resume --refresh-controller`; plain `resume` keeps running the workflow persisted at launch, even after a refresh. On a run launched by an earlier release, a verifier refreshed after its producer succeeded under the old workflow fails with `report producer selection was never recorded`, and mixing plain and refreshed resumes can make it fail with `run_metadata.agent_execution differs from the controller-observed producer`; in either case run `ultrafuzz resume <run-id> --refresh-controller --reset-node <report node>` (`node:final-report` in the packaged topologies), which reruns the report producer and its verifier rather than every failed task. Producer attempts after such a refresh leave the earlier release's attempts out of `agent_execution.failed_attempts`. After a restart the verifier compares against a run-directory file instead of the Smithers database. The reference docs now say that neither is a boundary against an agent running unsandboxed as the same user, which retires #585's claim that the run filesystem cannot be used to forge the producer (Refs #1143).
 - **[config] [runtime] [modal] [docs]** Removes per-node cloud execution (#134), which never completed a node in any release (#712, #713). `validate`, `doctor`, `run` and `eval run` reject `[execution] mode = "cloud"`, `execution.provider` and `[execution.providers.modal]` with `CONFIG_EXECUTION_CLOUD_REMOVED` before a run directory exists; remove `execution.provider` and `[execution.providers.modal]`, and set `mode = "local"` or delete it. The rest of `[execution]` is still accepted and validated but no longer affects execution: every agentic attempt runs locally. To use Modal, run the whole campaign inside one sandbox, as the unchanged `ultrafuzz-modal` eval runner does. A run planned with `mode = "cloud"` cannot be continued: `resume`, with or without `--refresh-controller`, reads the mode from the run's `smithers/resolved-config.json` and fails with `WORKFLOW_CLOUD_EXECUTION_REMOVED` before starting Smithers, so start a new run. It also fails, with `WORKFLOW_LIFECYCLE_FAILED`, for a run whose resolved config is missing or does not parse, which a plain `resume` used to continue without it. `ultrafuzz clean` no longer terminates Modal sandboxes tagged `purpose=ultrafuzz-node` or deletes the `ultrafuzz-node-*` volumes of earlier cloud attempts; remove those by hand in the Modal app the run used, which its `plan.json` records under `execution.providers.modal` until `ultrafuzz clean` deletes the run. The runtime `cloud-execution-generation` schema and the seven Modal node schemas are deleted, so `json validate` no longer recognizes them.
 - **[runtime] [docs]** A run launched by an earlier release whose dynamic groups have already expanded cannot be synchronized, resumed or reported after upgrading. Each synchronization re-renders the run's published prompts with the current code and compares the bytes, and this release changes the coverage text the final report prompt embeds (#1176) and the order of multi-path authority selectors (#1195), so such a run fails with `runtime rendered prompt changed`. Finish or cancel it before upgrading; `pause` and `cancel` still work on it.
@@ -24,6 +26,7 @@
 
 ### Other changes
 
+- **[runtime] [docs]** A task that started without a failed optional input, such as a review task without a failed strategy, keeps its result when `resume --retry-failed` reruns that input, whether the task is synchronized while the rerun is still running or after it succeeded. Before, the task failed with "optional dependency is not terminal for verifier admission" or "finalized optional dependency is missing from verifier admission", which could halt review and fail the run; in the first case a later task that checks the task's output, such as triage after dedupe, also failed for good. The retried node then counts as succeeded, so the report's completion can read COMPLETE and a `--require-complete` run can succeed, although the tasks that started before it verified never read its output. For a property lens, those are the property fan-in and everything after it.
 - **[runtime] [cli] [docs]** Production copies of `brace-expansion` and `undici` move past the High advisories published on 2026-09-29 (GHSA-6j4f-fj2g-mc7p and GHSA-qhr7-859c-m2p7 for `brace-expansion`, GHSA-rfgv-xxqx-mfg5 for `undici`) and the Moderate and Low advisories fixed alongside them (GHSA-q2hr-2g5m-vwhr, GHSA-3wwx-pv8p-q78v, GHSA-r53p-7pc4-xj5r). The CLI's two `brace-expansion` copies, both pulled in by `@oclif/core` through `minimatch`, move from 2.1.4 and 5.0.9 to 2.1.7 and 5.0.12. No npm release bundles these fixes yet, so the `[email protected]` patch now also carries `brace-expansion` 5.0.12 and `undici` 6.28.1 inside the operator npm, and the operator npm's pinned closure digest changes with it.
 - **[artifacts]** Concurrent ultrafuzz commands, such as `ultrafuzz status --watch` while `ultrafuzz cancel` runs, no longer lose or tear records in a run's `events.jsonl`, `usage.jsonl` or `attempts.jsonl`, or in the `.ultrafuzz/` audit journals. Each append holds a short-lived `<journal>.lock` next to the journal; a lock left by a killed process on the same host is taken over at once, and one that cannot be checked after 10 seconds.
 - **[runtime] [docs]** When `resume --retry-failed` retries a dynamic source whose verifier failed, it now also withdraws the rendered prompts of later nodes that wait on the group, so they render again from the new expansion. Before, if the retried source planned different items, a node whose prompt names the group's children (for example with `{{artifact_path:<group>}}`) failed every render with `runtime rendered prompt changed for <attempt>`. The packaged topologies were not affected (#1141).

diff --git a/docs/explanation/campaigns.md b/docs/explanation/campaigns.md
@@ -39,7 +39,8 @@ phase; they are evidence to inspect, not an automatic security submission.
 The default scaffold is the direct bug-finding workflow:
 
 - Eight property-discovery lenses produce the shared property catalog and may
-  publish concrete findings discovered while deriving properties.
+  publish concrete findings discovered while deriving properties. A lens that
+  fails is left out of the catalog; the campaign continues with the others.
 - Twenty direct strategies investigate boundary, accounting, input,
   round-trip, workflow, time, state-machine, dependency, parity, lifecycle, and
   coverage-expansion hypotheses.

diff --git a/docs/how-to/restart-continue.md b/docs/how-to/restart-continue.md
@@ -82,6 +82,17 @@ the resumed workflow decides the skip again from the restored task states. It
 stays skipped while the prerequisite is still failed, and runs once a reset lets
 the prerequisite succeed.
 
+Retrying a failed node of a `failure_policy: continue` group does not undo work
+that already ran without it. A task that started before the retried node
+verified keeps the result it produced without that node, and only tasks that
+start afterwards read the new output. The retried node then counts as
+succeeded, so the report's completion can read COMPLETE and a
+`--require-complete` run can succeed, although those earlier tasks never read
+its output. For a property lens, those are the property fan-in and everything
+after it. A retried artifact verifier is different: resetting its agent
+producer also resets every node that started after that producer's attempt, so
+those nodes run again.
+
 ## Replay A Linked Run
 
 Use replay when you want the workflow engine to replay the linked run from the

diff --git a/docs/reference/artifacts-reports.md b/docs/reference/artifacts-reports.md
@@ -638,10 +638,12 @@ of production issues and, in bounded classification mode, the triage
 classification, lifecycle enrichment, and severity assessment of production
 issues.
 
-New runs use `run.completion_policy = "best-effort"` by default. Stock strategy
-groups continue after ordinary task failures. Independent work can finish;
-work that needs a missing required result is skipped. Review uses successful
-results that pass the existing input checks. User-authored topologies retain
+New runs use `run.completion_policy = "best-effort"` by default. The stock
+property-lens, goal, strategy, and specialist groups continue after ordinary
+task failures. Independent work can finish; work that needs a missing required
+result is skipped. Nodes that combine another group's results, such as the
+property fan-in and review, use the successful results that pass the existing
+input checks. User-authored topologies retain
 their declared failure policies. The configured attempts and time limits remain
 in effect; reporting does not restart analysis or add recovery attempts.
 

diff --git a/docs/reference/prompt-catalog-data.yml b/docs/reference/prompt-catalog-data.yml
@@ -48,7 +48,7 @@ prompts:
     description: Derives target invariants and liveness properties using the Crytic reference.
   - path: properties/property-specification-fanin.md
     category: Property consolidation
-    description: Validates, merges, and deduplicates every property lens into one canonical property catalog.
+    description: Validates, merges, and deduplicates every verified property lens into one canonical property catalog.
   - path: properties/property-specification-runtime-verification.md
     category: Property design
     description: Derives target invariants using the Runtime Verification reference.

diff --git a/docs/reference/prompt-catalog.md b/docs/reference/prompt-catalog.md
@@ -27,7 +27,7 @@ The default topology binds 48 agentic nodes to 47 distinct prompt files. [`strat
 | [`properties/aviggiano-lens.md`](../../.ultrafuzz/prompts/properties/aviggiano-lens.md) | Property design | Derives target properties using Antonio Viggiano's property reference. |
 | [`properties/0kn0t-lens.md`](../../.ultrafuzz/prompts/properties/0kn0t-lens.md) | Property design | Derives target properties using the 0kn0t reference. |
 | [`properties/josselin-feist-lens.md`](../../.ultrafuzz/prompts/properties/josselin-feist-lens.md) | Property design | Derives DeFi rounding properties using the Montyly rounding reference under the Josselin Feist lens identity. |
-| [`properties/property-specification-fanin.md`](../../.ultrafuzz/prompts/properties/property-specification-fanin.md) | Property consolidation | Validates, merges, and deduplicates every property lens into one canonical property catalog. |
+| [`properties/property-specification-fanin.md`](../../.ultrafuzz/prompts/properties/property-specification-fanin.md) | Property consolidation | Validates, merges, and deduplicates every verified property lens into one canonical property catalog. |
 | [`strategies/boundary-tests.md`](../../.ultrafuzz/prompts/strategies/boundary-tests.md) | Strategy | Turns properties and workflows into adversarial boundary recipes while investigating confirmed production bugs. |
 | [`strategies/encode-decode.md`](../../.ultrafuzz/prompts/strategies/encode-decode.md) | Strategy | Investigates encoding, decoding, parsing, serialization, and promised inverse relationships. |
 | [`strategies/differential-library-tests.md`](../../.ultrafuzz/prompts/strategies/differential-library-tests.md) | Strategy | Performs lightweight public-surface differential checks using independently justified comparators. |