diff --git a/certora_autosetup/autosetup/autosetup.py b/certora_autosetup/autosetup/autosetup.py
index 52bef8f3..a174db48 100644
--- a/certora_autosetup/autosetup/autosetup.py
+++ b/certora_autosetup/autosetup/autosetup.py
@@ -215,10 +215,6 @@ def _summarized_library_names(self) -> set[str]:
         llm = set(setup._methods_per_contract.keys()) & self._library_names
         return curated | llm
 
-    def _build_job_msg(self, contract_name: str, conf_file: Path) -> str:
-        """Build the msg string for a prover job."""
-        return ProverJobSpec.build_job_msg(self.config.orchestration_timestamp, contract_name, conf_file)
-
     def run(self, main_contract_handle: ContractHandle, skip_warmup: bool = False) -> AutosetupResult:
         """Execute the full autosetup pipeline.
 
@@ -811,7 +807,6 @@ async def prepare_contract_warmup() -> Optional[ProverJobSpec[Any]]:
                     contract_name=contract_name,
                     phase=f"Sanity Test Run - {contract_name}",
                     extra_args=autosetup.config.extra_args,
-                    msg=autosetup._build_job_msg(contract_name, test_config.path),
                 ))
 
                 if skip_warmup:
@@ -831,7 +826,6 @@ async def prepare_contract_warmup() -> Optional[ProverJobSpec[Any]]:
                     contract_name=contract_name,
                     phase="Sanity Warmup - warmup",
                     extra_args=autosetup.config.extra_args,
-                    msg=autosetup._build_job_msg(contract_name, warmup_config.path),
                 )
 
             async def prepare_and_run_warmup():
diff --git a/certora_autosetup/conf_runner/callbacks.py b/certora_autosetup/conf_runner/callbacks.py
index 45621a4d..1d1ff156 100644
--- a/certora_autosetup/conf_runner/callbacks.py
+++ b/certora_autosetup/conf_runner/callbacks.py
@@ -191,7 +191,6 @@ def _create_multi_assert_jobs_if_needed(self, result: ProverResult) -> List[Prov
                     phase=f"{result.job_spec.phase}_{rule_name}_multi_assert",
                     extra_args=result.job_spec.extra_args,
                     context=result.job_spec.context,
-                    msg=ProverJobSpec.build_job_msg(self.orchestration_timestamp, contract_name, new_config_path),
                 )
                 new_jobs.append(new_job_spec)
 
@@ -294,7 +293,6 @@ def _create_difficult_retry_jobs_if_needed(
                     phase=f"{result.job_spec.phase}_{rule_name}_difficult_retry",
                     extra_args=result.job_spec.extra_args,
                     context=result.job_spec.context,
-                    msg=ProverJobSpec.build_job_msg(self.orchestration_timestamp, contract_name, new_config_path),
                 )
                 new_jobs.append(new_job_spec)
 
diff --git a/certora_autosetup/conf_runner/conf_runner.py b/certora_autosetup/conf_runner/conf_runner.py
index 21ede3fa..a267cfef 100644
--- a/certora_autosetup/conf_runner/conf_runner.py
+++ b/certora_autosetup/conf_runner/conf_runner.py
@@ -137,7 +137,6 @@ def _run_all_configs(
                     contract_name=contract_name,
                     phase=f"{tool_name}-{config_name}",
                     extra_args=self.config.extra_args,
-                    msg=ProverJobSpec.build_job_msg(self.orchestration_timestamp, contract_name, config_file),
                 )
                 job_specs.append(job_spec)
                 self.log(
diff --git a/certora_autosetup/setup/call_resolution.py b/certora_autosetup/setup/call_resolution.py
index 22efe5a0..92f7fc2d 100644
--- a/certora_autosetup/setup/call_resolution.py
+++ b/certora_autosetup/setup/call_resolution.py
@@ -473,6 +473,9 @@ async def _run_prover_and_parse_calls(self) -> Optional[List[CallResolutionInfo]
             phase="call_resolution",
             config_file=config_content,
             extra_args=self.extra_args,
+            msg=ProverJobSpec.build_job_msg(
+                self.contract_name, self.config_file, suffix=f"(iteration {self.current_iteration})"
+            ),
         )
 
         prover_result = await self.prover_runner.check_with_prover(job_spec)
diff --git a/certora_autosetup/setup/sanity.py b/certora_autosetup/setup/sanity.py
index 3221eaea..f6d3b1ba 100644
--- a/certora_autosetup/setup/sanity.py
+++ b/certora_autosetup/setup/sanity.py
@@ -364,14 +364,6 @@ def _internal_confs_dir(self) -> Path:
         """Directory for transient conf copies, kept out of the user-facing certora/confs/ tree."""
         return self.prover_runner.project_root / DIR_INTERNAL_CONFS
 
-    def _build_job_msg(self, conf_file: Path) -> Optional[str]:
-        """Build the msg string for a prover job.
-
-        Format: "ProverLite <timestamp> <ContractName>: <conf_name>"
-        Returns None if no orchestration_timestamp is set.
-        """
-        return ProverJobSpec.build_job_msg(self.orchestration_timestamp, self.contract_name, conf_file)
-
     def log(self, level: str, message: str):
         """Simple contract logging utility."""
         log_with_contract("Sanity", level, self.contract_name, message)
@@ -598,7 +590,6 @@ async def _run_sanity_coverage_rerun(self, failing_methods: List[str], completio
                 phase=f"Sanity Coverage Rerun - {self.contract_name} - {method}",
                 config_file=coverage_config,
                 extra_args=self.extra_args,
-                msg=self._build_job_msg(coverage_config.path),
             ))
         return await self.prover_runner.submit_and_wait_for_jobs(job_specs, completion_callback=completion_callback)
 
@@ -728,7 +719,6 @@ async def _detect_optimal_hashing_bounds(self) -> Optional[int]:
                 phase="hashing_bound_detection",
                 config_file=bound_detection_config,
                 extra_args=self.extra_args,
-                msg=self._build_job_msg(bound_detection_config.path),
             )
 
             result = await self.prover_runner.check_with_prover(job_spec)
@@ -904,7 +894,6 @@ async def _test_configurations(
                 config_file=test_config,
                 extra_args=self.extra_args,
                 context=config,  # Store BoundConfiguration as context
-                msg=self._build_job_msg(test_config.path),
             )
             job_specs.append(job_spec)
 
diff --git a/certora_autosetup/utils/enhanced_config_manager.py b/certora_autosetup/utils/enhanced_config_manager.py
index 186b8888..afe060bd 100644
--- a/certora_autosetup/utils/enhanced_config_manager.py
+++ b/certora_autosetup/utils/enhanced_config_manager.py
@@ -75,6 +75,11 @@ class ProverJobSpec(Generic[ContextT]):
     context: Optional[ContextT] = None
     msg: Optional[str] = None  # Message for --msg argument
 
+    def __post_init__(self) -> None:
+        # When no msg is given, default it to "<Contract>: <conf_name>".
+        if self.msg is None:
+            self.msg = self.build_job_msg(self.contract_name, self.config_file.path)
+
     def get_cache_key(self, config_manager: "ConfigManager") -> str:
         """
         Generate cache key from config + all referenced files + extra_args.
@@ -100,20 +105,24 @@ def get_cache_key(self, config_manager: "ConfigManager") -> str:
         return cache_key
 
     @staticmethod
-    def build_job_msg(orchestration_timestamp: str, contract_name: str, conf_file: Path) -> str:
+    def build_job_msg(contract_name: str, conf_file: Path, suffix: Optional[str] = None) -> str:
         """Build the msg string for a prover job.
 
-        Format: "Certora <timestamp> <ContractName>: <conf_name>"
+        Format: "<ContractName>: <conf_name>" (with " <suffix>" appended if provided).
 
         Args:
-            orchestration_timestamp: Timestamp string from orchestration start
             contract_name: Name of the contract being verified
             conf_file: Path to the configuration file
+            suffix: Optional trailing text to disambiguate jobs that reuse the same
+                conf (e.g. an iteration marker); the caller decides its content
 
         Returns:
-            Formatted message string or None if no timestamp
+            Formatted message string
         """
-        return f"Certora {orchestration_timestamp} {contract_name}: {conf_file.stem}"
+        msg = f"{contract_name}: {conf_file.stem}"
+        if suffix:
+            msg += f" {suffix}"
+        return msg
 
 
 class ConfigManager:
diff --git a/composer/prover/core.py b/composer/prover/core.py
index 34d92891..7c0464d6 100644
--- a/composer/prover/core.py
+++ b/composer/prover/core.py
@@ -45,6 +45,9 @@
 from composer.prover.cloud import CloudJobError, cloud_results
 from composer.prover.ptypes import RuleResult
 from composer.prover.results import read_and_format_run_result
+from composer.prover.vacuity import (
+    VacuityEvidence, detect_vacuous_methods, format_vacuity_alert, instantiated_methods,
+)
 from composer.templates.loader import load_jinja_template
 from composer.prover.prover_protocol import ProverResult
 
@@ -97,10 +100,18 @@ class ProverReport:
     them through the return value.
 
     ``link`` is the prover run's URL (cloud) or local results directory.
+
+    ``vacuous_methods`` / ``instantiated_methods`` carry the per-run vacuity
+    view (see ``composer/prover/vacuity.py``): the methods detected as vacuous
+    in this run, and every method this run instantiated at all. The latter
+    lets the caller clear a previously-recorded vacuity verdict once a run
+    shows the method instantiated and healthy.
     """
     rule_status: dict[str, bool]
     result_str: str
     link: str
+    vacuous_methods: dict[str, VacuityEvidence] = field(default_factory=dict)
+    instantiated_methods: set[str] = field(default_factory=set)
 
     @property
     def all_verified(self) -> bool:
@@ -481,6 +492,11 @@ async def run_prover(
 
             all_results = list(parsed.values())
 
+            # Vacuity view of this run: methods whose sanity check failed across
+            # their instantiating rules. Computed here (rather than in callers)
+            # so every prover consumer sees the same alert in its report string.
+            vacuous = detect_vacuous_methods(all_results)
+
             # 10. Hand off to the handler when anything failed. It owns the
             # analysis approach, per-rule UI events, rendering, summarization
             # (if any), and storage of any keyed records (e.g. report_keys
@@ -498,6 +514,12 @@ async def run_prover(
                     rule_entries=[(r, None) for r in all_results],
                     diagnoses=[],
                 )
+
+            # Append the vacuity alert to whatever the handler/template rendered:
+            # a vacuous method most often surfaces as a *passing* (trivially
+            # verified) rule, so the alert must reach the agent on both branches.
+            if vacuous:
+                result_str = f"{result_str}\n\n{format_vacuity_alert(vacuous)}"
     except CloudJobError as exc:
         return f"Prover cloud job did not produce results (status {exc.status.value})."
 
@@ -512,4 +534,6 @@ async def run_prover(
         rule_status=prover_report,
         result_str=result_str,
         link=run_result["link"],
+        vacuous_methods=vacuous,
+        instantiated_methods=instantiated_methods(all_results),
     )
diff --git a/composer/prover/vacuity.py b/composer/prover/vacuity.py
new file mode 100644
index 00000000..dae30e75
--- /dev/null
+++ b/composer/prover/vacuity.py
@@ -0,0 +1,163 @@
+"""Vacuous-method detection over per-rule prover results.
+
+A parametric method whose sanity check fails in every rule that instantiates it
+(or in several rules while every other instantiation timed out or errored) is
+*vacuous*: every path through it reverts under
+the current verification model, so any rule instantiated with it passes
+trivially. Per-rule ``SANITY_FAILED`` results already reach the verify loop
+(``composer/prover/results.py`` attaches the ``METHOD_INSTANTIATION`` name to
+``RulePath.method``); this module aggregates them into a per-method verdict and
+renders the ``<vacuity_alert>`` the agent sees plus the ``verify_spec`` guard
+message. The guard itself is purely structural (no spec-text scanning): a
+verdict persists in graph state until a run re-instantiates the method
+healthily, so *any* route that hides the method (a ``filtered`` block, marking
+its rules "expected to fail", deleting the rule) leaves the verdict
+outstanding, and the PROVER stamp is withheld unless the agent formally
+acknowledges the method via the ``acknowledge_vacuous_method`` tool.
+
+The near-universal root cause is a setup defect — canonically a NONDET summary
+on a payable or side-effecting callee — so the alert prescribes a *repair
+ladder* that puts root-cause fixes first and ``filtered`` exclusion last.
+"""
+
+from typing import Iterable
+
+from pydantic import BaseModel
+
+from composer.prover.ptypes import RuleResult
+
+
+class VacuityEvidence(BaseModel):
+    """Why a method was flagged as vacuous: the rules whose sanity check it
+    failed, and a one-line diagnosis suitable for reports and agent state."""
+
+    method: str
+    affected_rules: list[str]
+    diagnosis: str
+
+
+def detect_vacuous_methods(results: Iterable[RuleResult]) -> dict[str, VacuityEvidence]:
+    """Group ``SANITY_FAILED`` results by instantiated method and flag the
+    methods that are sanity-failed in 100% of the rules that instantiate them,
+    OR in >= 2 rules while no instantiation reached a healthy verdict.
+
+    The 100% arm catches single-rule runs. The >= 2 arm catches a method that
+    is vacuous across the board when the remaining instantiations are
+    TIMEOUT/ERROR/SKIPPED — statuses that can *mask* an all-paths-reverting
+    method. A VERIFIED or VIOLATED instantiation, by contrast, requires
+    actually reaching the method's code, so it *disproves* all-paths
+    reversion: sanity failures alongside a healthy instantiation stem from
+    the failing rules' own preconditions (a rule-authoring problem), not
+    method vacuity, and must not be flagged here. A sanity failure on a
+    non-parametric rule (``path.method is None``) is likewise a
+    rule-authoring problem and is ignored.
+    """
+    instantiating: dict[str, set[str]] = {}
+    sanity_failed: dict[str, set[str]] = {}
+    healthy: dict[str, set[str]] = {}
+    for r in results:
+        method = r.path.method
+        if method is None:
+            continue
+        instantiating.setdefault(method, set()).add(r.path.rule)
+        if r.status == "SANITY_FAILED":
+            sanity_failed.setdefault(method, set()).add(r.path.rule)
+        elif r.status in ("VERIFIED", "VIOLATED"):
+            healthy.setdefault(method, set()).add(r.path.rule)
+
+    flagged: dict[str, VacuityEvidence] = {}
+    for method, failed_rules in sanity_failed.items():
+        all_rules = instantiating[method]
+        everywhere = failed_rules == all_rules
+        masked_majority = len(failed_rules) >= 2 and not healthy.get(method)
+        if not (everywhere or masked_majority):
+            continue
+        flagged[method] = VacuityEvidence(
+            method=method,
+            affected_rules=sorted(failed_rules),
+            diagnosis=(
+                f"sanity-failed in {len(failed_rules)} of {len(all_rules)} rule(s) "
+                "that instantiate it: the method reverts on every path under the "
+                "current verification model, so rules over it pass vacuously"
+            ),
+        )
+    return flagged
+
+
+def instantiated_methods(results: Iterable[RuleResult]) -> set[str]:
+    """Every method name instantiated in this result set (any status). Used to
+    clear a stale vacuity verdict once a later run shows the method healthy."""
+    return {r.path.method for r in results if r.path.method is not None}
+
+
+_REPAIR_LADDER = """\
+This is almost always a SETUP defect, not a property error. The canonical culprits are:
+  * a NONDET/CONSTANT summary applied to a payable or side-effecting callee (the summary drops
+    the callee's effects — e.g. its ability to accept msg.value — making the caller's success
+    path infeasible),
+  * an unresolved low-level `.call{value: ...}` that HAVOCs and can always be assumed to fail,
+  * a missing `link`, leaving a callee address unresolved.
+
+Repair in this order (the "repair ladder"); do NOT jump to a later step without attempting the earlier ones:
+  1. Fix or replace the offending summary so it preserves the callee's semantics — in particular
+     payable-ness: a payable callee must be able to accept the transferred value.
+  2. Write a minimal mock contract under `certora/mocks` (the `write_mock` tool) implementing the
+     callee's interface, and register it in the prover config with `edit_config` (AddFile, plus
+     AddLink if the callee is reached through a storage field).
+  3. Set `optimistic_fallback` to true via `edit_config` (set_flag) so unresolved calls are assumed
+     to succeed instead of always being able to revert.
+  4. ONLY as a last resort, formally acknowledge the method with the `acknowledge_vacuous_method`
+     tool, recording which of steps 1-3 you attempted and why each failed, and then exclude it
+     with a `filtered` block. Hiding a vacuous method (filtering it, marking its rules "expected
+     to fail", or deleting the rule) without that acknowledgment will not be accepted as a
+     passing result."""
+
+
+def format_vacuity_alert(evidence: dict[str, VacuityEvidence]) -> str:
+    """Render the ``<vacuity_alert>`` block appended to the prover report the
+    agent sees. Empty string when nothing was flagged."""
+    if not evidence:
+        return ""
+    lines = [
+        "<vacuity_alert>",
+        "The following method(s) are VACUOUS — every rule instantiated with them holds trivially",
+        "because their assertions are unreachable:",
+    ]
+    for method in sorted(evidence):
+        ev = evidence[method]
+        lines.append(f"  - {method}: {ev.diagnosis} (rules: {', '.join(ev.affected_rules)})")
+    lines.append("")
+    lines.append(_REPAIR_LADDER)
+    lines.append("</vacuity_alert>")
+    return "\n".join(lines)
+
+
+def format_vacuity_guard(blocked: dict[str, str]) -> str:
+    """Render the message returned by ``verify_spec`` when it withholds the
+    PROVER validation stamp: ``blocked`` maps each still-outstanding vacuous
+    method (no healthy re-instantiation, no acknowledgment) to its diagnosis.
+
+    The gate feeding this is purely structural — set membership over the
+    persisted verdicts and the acknowledgment ledger, never spec-text scanning
+    — so the message covers every hiding route (``filtered`` blocks,
+    ``expect_rule_failure`` skips, rule deletion) uniformly.
+    """
+    method_list = "\n".join(f"  - {m}: {d}" for m, d in sorted(blocked.items()))
+    return f"""\
+<vacuity_guard>
+The PROVER validation stamp was WITHHELD. The following method(s) were detected as VACUOUS
+(they revert on every path under the current verification model), and no later run has shown
+them healthy, nor have they been acknowledged:
+{method_list}
+
+A run where every rule passes while a known-vacuous method is hidden (via a `filtered` block,
+`expect_rule_failure` on its sanity-failing rules, or removing the rule) hides a setup defect
+instead of fixing it. Either:
+  * repair the root cause (repair ladder: 1. fix/replace the offending summary preserving payable
+    semantics, 2. `write_mock` + `edit_config` add_file/add_link, 3. `optimistic_fallback` via
+    `edit_config` set_flag), re-include the method, and rerun `verify_spec` — a run that
+    instantiates the method without a sanity failure clears its verdict automatically; or
+  * if steps 1-3 genuinely failed, call `acknowledge_vacuous_method` for the method, recording
+    which steps you attempted and why each failed, then rerun `verify_spec`. The feedback judge
+    will audit the quality of that acknowledgment.
+</vacuity_guard>"""
diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py
index ba8da4bd..d667064e 100644
--- a/composer/spec/cvl_generation.py
+++ b/composer/spec/cvl_generation.py
@@ -7,8 +7,11 @@
 """
 
 import hashlib
+import json
 from dataclasses import dataclass
-from typing import Annotated, Callable, Literal, NotRequired, override, Awaitable, Any, Protocol
+from typing import (
+    Annotated, Callable, Literal, Mapping, NotRequired, override, Awaitable, Any, Protocol, cast,
+)
 from typing_extensions import TypedDict
 
 from pydantic import BaseModel, Field
@@ -125,6 +128,10 @@ class GeneratedCVL(BaseModel):
     # (which skips the prover) can still reconstruct certora/confs. None for pre-existing
     # cache entries or runs where no config was established.
     config: dict | None = Field(default=None)
+    # The generation's mock contracts (state["mocks"]: project-root-relative path ->
+    # Solidity source), persisted so the conf's file references resolve on cache replay
+    # from a fresh checkout. Empty for pre-existing cache entries and mock-free runs.
+    mocks: dict[str, str] = Field(default_factory=dict)
     # The last prover-run link (URL or local results dir), persisted for the report and so a
     # cache hit retains it. None when the prover never produced a link.
     final_link: str | None = Field(default=None)
@@ -147,14 +154,55 @@ class CVLGenerationExtra(TypedDict):
     required_validations: list[str]
 
 
-def _compute_digest(curr_spec: str, skipped: list[SkippedProperty]) -> str:
+def _compute_digest(
+    curr_spec: str,
+    skipped: list[SkippedProperty],
+    *,
+    config: Mapping[str, Any] | None = None,
+    mocks: Mapping[str, str] | None = None,
+    acknowledged: Mapping[str, str] | None = None,
+) -> str:
     digester = hashlib.md5()
     digester.update(curr_spec.encode())
     for s in skipped:
         digester.update(f"{s.property_title}:{s.reason}".encode())
+    # The agent-mutable prover setup joins the digest the empty-contributes-nothing
+    # way: an absent or empty value hashes identically to the pre-field digest, so
+    # stamps from flows without these state keys (and cache entries predating them)
+    # stay valid. Canonical JSON keeps the hash order-independent and unambiguous.
+    if config:
+        digester.update(json.dumps(config, sort_keys=True).encode())
+    if mocks:
+        digester.update(json.dumps(mocks, sort_keys=True).encode())
+    if acknowledged:
+        digester.update(json.dumps(acknowledged, sort_keys=True).encode())
     return digester.hexdigest()
 
 
+def state_digest(state: CVLGenerationExtra) -> str:
+    """Digest of everything the validation stamps attest to: the spec text, the
+    skip declarations, and — when the flow carries them — the agent-mutable
+    prover setup (``config``, ``mocks``, and the ``acknowledged_vacuous``
+    ledger, layered onto this state by the source-mode ``ProverStateExtra``).
+
+    Both the FEEDBACK and PROVER stamps use this digest, so ANY post-stamp edit
+    to the setup (an ``edit_config`` flag flip, a rewritten mock, a new
+    acknowledgment) goes stale on completion and forces a re-verify AND a
+    re-judge over the setup that will actually be published — the stamp's
+    attestation would otherwise silently cover state the prover/judge never
+    saw. The extra keys are read dynamically with empty defaults because flows
+    without them (natreq) must hash identically to before.
+    """
+    extras = cast(Mapping[str, Any], state)
+    return _compute_digest(
+        state["curr_spec"] or "",
+        state["skipped"],
+        config=extras.get("config"),
+        mocks=extras.get("mocks"),
+        acknowledged=extras.get("acknowledged_vacuous"),
+    )
+
+
 def check_completion(
     state: CVLGenerationExtra,
 ) -> str | None:
@@ -162,7 +210,7 @@ def check_completion(
     spec = state["curr_spec"]
     if spec is None:
         return "Completion REJECTED: no spec written yet."
-    digest = _compute_digest(spec, state["skipped"])
+    digest = state_digest(state)
     validations = state["validations"]
     required = state["required_validations"]
     for key in required:
@@ -218,14 +266,11 @@ def validate_property_rules(
 def make_validation_stamper(key: str) -> Callable[[CVLGenerationExtra], dict[str, str]]:
     """Create a stamper for future prover tool integration.
 
-    The stamper reads curr_spec/skipped from state and returns
-    a dict suitable for merging into the validations state key.
+    The stamper reads the digest-covered state (see :func:`state_digest`) and
+    returns a dict suitable for merging into the validations state key.
     """
     def stamp(state: CVLGenerationExtra) -> dict[str, str]:
-        return {key: _compute_digest(
-            state["curr_spec"] or "",
-            state["skipped"],
-        )}
+        return {key: state_digest(state)}
     return stamp
 
 
@@ -245,13 +290,15 @@ class _LastAttemptCache(BaseModel):
 DESCRIPTION = "CVL generation"
 
 type FeedbackToolImpl = Callable[
-    [str, list[SkippedProperty], list[Rebuttal], str],
+    [str, list[SkippedProperty], list[Rebuttal], str, Mapping[str, Any]],
     Awaitable[PropertyFeedbackProtocol],
 ]
-"""``(cvl, skipped, rebuttals, within_tool) -> PropertyFeedback``. ``within_tool``
-is the calling ``_FeedbackSchema``'s ``tool_call_id``, plumbed through to the
-sub-graph's ``run_to_completion`` so its UI panel anchors under the parent
-tool widget."""
+"""``(cvl, skipped, rebuttals, within_tool, state) -> PropertyFeedback``.
+``within_tool`` is the calling ``_FeedbackSchema``'s ``tool_call_id``, plumbed
+through to the sub-graph's ``run_to_completion`` so its UI panel anchors under
+the parent tool widget. ``state`` is the calling generation's full graph state,
+so a judge's ``extra_inputs`` thunk can surface flow-specific evidence (e.g.
+vacuity verdicts, rule skips, and acknowledgments in the source-mode flow)."""
 
 @dataclass
 class FeedbackToolContext:
@@ -295,10 +342,10 @@ async def run(self) -> Command:
         if spec is None:
             return tool_return(self.tool_call_id, "No spec put yet")
         skipped = st["skipped"]
-        t = await feedback(spec, skipped, self.rebuttals, self.tool_call_id)
+        t = await feedback(spec, skipped, self.rebuttals, self.tool_call_id, st)
         msg = f"Good? {t.good}\nFeedback {t.feedback}"
         if t.good:
-            digest = _compute_digest(spec, skipped)
+            digest = state_digest(st)
             return tool_state_update(
                 self.tool_call_id, msg,
                 validations={FEEDBACK_VALIDATION_KEY: digest},
diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py
index 5f64d7b1..1053772b 100644
--- a/composer/spec/feedback.py
+++ b/composer/spec/feedback.py
@@ -1,5 +1,5 @@
 
-from typing import Callable, NotRequired, Sequence
+from typing import Any, Callable, Mapping, NotRequired, Sequence
 from typing_extensions import TypedDict
 from composer.spec.service_host import Sort, ServiceHost
 
@@ -59,9 +59,13 @@ def property_feedback_judge(
     prompt: InjectedTemplate[Properties] | TemplateInstantiation,
     props: list[PropertyFormulation],
     *,
-    extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None,
+    extra_inputs: list[str | dict] | Callable[[Mapping[str, Any]], list[str | dict]] | None = None,
     system_prompt: TemplateInstantiation | None = None,
 ) -> FeedbackToolContext:
+    # ``extra_inputs`` may be a static list, or a thunk over the calling
+    # generation's graph state (evaluated per feedback round, so the judge sees
+    # the evidence as it stands at judging time — e.g. the source-mode flow's
+    # vacuity verdicts, rule skips, and acknowledgments).
 
     if system_prompt is None:
         system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort})
@@ -105,13 +109,14 @@ async def the_tool(
         skipped: Sequence[SkippedProperty],
         rebuttals: Sequence[Rebuttal],
         within_tool: str,
+        state: Mapping[str, Any],
     ) -> PropertyFeedback:
         input_parts: list[str | dict] = []
         if extra_inputs:
             if isinstance(extra_inputs, list):
                 input_parts.extend(extra_inputs)
             else:
-                input_parts.extend(extra_inputs())
+                input_parts.extend(extra_inputs(state))
 
         input_parts.append("The proposed CVL file is")
         input_parts.append(cvl)
diff --git a/composer/spec/gen_types.py b/composer/spec/gen_types.py
index bf27022a..013bbf49 100644
--- a/composer/spec/gen_types.py
+++ b/composer/spec/gen_types.py
@@ -27,6 +27,12 @@
 PROPERTIES_DIR = CERTORA_DIR / PROPERTIES_SUBDIR
 #: AutoSetup / custom summaries live here.
 SUMMARIES_DIR = SPECS_DIR / "summaries"
+#: Agent-written mock contracts (the `write_mock` repair-ladder tool). Mocks are
+#: state-held during generation and only touch this directory when materialized
+#: for a prover run or persisted by the artifact store; each generation writes
+#: into its own subdirectory (``certora/mocks/<spec stem>/``) so concurrent
+#: batches never collide.
+MOCKS_DIR = CERTORA_DIR / "mocks"
 #: The autoprove run report (report.json, the optional rendered HTML, and the
 #: canonical slug<->id map) lives here -- a dedicated subdir so a consumer can
 #: include or exclude the human-facing report independently of the specs.
diff --git a/composer/spec/natspec/author.py b/composer/spec/natspec/author.py
index abcfb5ff..e1fc7214 100644
--- a/composer/spec/natspec/author.py
+++ b/composer/spec/natspec/author.py
@@ -1,5 +1,5 @@
 from dataclasses import dataclass
-from typing import Callable, Literal, override, Annotated, Literal
+from typing import Any, Callable, Literal, Mapping, override, Annotated, Literal
 from pydantic import Field, BaseModel, Discriminator
 
 from typing_extensions import TypedDict
@@ -209,7 +209,9 @@ async def generate_cvl_batch(
     if (cached := await root_ctx.cache_get(AuthorResult)) is not None:
         return cached.result_wrapped
 
-    def stub_feedback_extras() -> list[str | dict]:
+    def stub_feedback_extras(_state: Mapping[str, Any]) -> list[str | dict]:
+        # The judge-evidence thunk receives the generation's graph state; the
+        # natreq judge's extras are state-independent, so it is unused here.
         return [
             f"The current typechecking stub for the {contract_name} contract is",
             stub_reader(),
diff --git a/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py
index ae46480a..4ea0b8a1 100644
--- a/composer/spec/source/artifacts.py
+++ b/composer/spec/source/artifacts.py
@@ -16,7 +16,7 @@
 from composer.spec.context import SourceCode
 from composer.spec.cvl_generation import GeneratedCVL
 from composer.spec.gen_types import (
-    AP_REPORT_DIR, AUTOPROVE_INTERNAL_DIR, CERTORA_DIR, SPECS_DIR, under_project,
+    AP_REPORT_DIR, AUTOPROVE_INTERNAL_DIR, CERTORA_DIR, MOCKS_DIR, SPECS_DIR, under_project,
 )
 from composer.spec.prop import PropertyFormulation
 from composer.spec.source.prover import prover_config_overlay
@@ -92,7 +92,8 @@ def write_generated_spec(self, spec: SpecIdentity, result: GeneratedCVL) -> Path
         project-root-relative path (e.g. ``certora/specs/invariants.spec``).
 
         Bundle: ``specs/{stem}.spec``, ``properties/{stem}.commentary.md``,
-        ``properties/{stem}.property_rules.json``, and ``confs/{stem}.conf``.
+        ``properties/{stem}.property_rules.json``, ``confs/{stem}.conf``, and the
+        generation's mock contracts (if any) at their state-held paths.
         """
         specs_dir = ensure_dir(self._deliverable_dir() / "specs")
         (specs_dir / spec.spec_filename).write_text(result.cvl)
@@ -101,10 +102,26 @@ def write_generated_spec(self, spec: SpecIdentity, result: GeneratedCVL) -> Path
             spec.stem, "property_rules",
             {m.property_title: m.rules for m in result.property_rules},
         )
+        self._write_mocks(result.mocks)
         spec_path = SPECS_DIR / spec.spec_filename  # project-root-relative
         self._write_conf(spec, result.config, spec_path)
         return spec_path
 
+    def _write_mocks(self, mocks: dict[str, str]) -> None:
+        """The generation's mock contracts, at their exact state-held
+        (project-root-relative, per-generation-namespaced) paths — the conf's
+        ``files`` entries reference them there, so a cache replay from a fresh
+        checkout can recompile without rerunning the generation."""
+        for rel, content in mocks.items():
+            rel_path = Path(rel)
+            # Belt over the write_mock tool's validation: never write outside
+            # the canonical mocks directory.
+            assert not rel_path.is_absolute() and ".." not in rel_path.parts, rel
+            assert rel_path.parts[:len(MOCKS_DIR.parts)] == MOCKS_DIR.parts, rel
+            target = under_project(self._project_root, rel_path)
+            target.parent.mkdir(parents=True, exist_ok=True)
+            target.write_text(content)
+
     def _write_conf(
         self, spec: SpecIdentity, base_config: dict | None, spec_path: Path,
     ) -> None:
diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py
index a7e8df1f..bde724d2 100644
--- a/composer/spec/source/author.py
+++ b/composer/spec/source/author.py
@@ -1,4 +1,4 @@
-from typing import NotRequired, override, Literal, Annotated
+from typing import Any, Mapping, NotRequired, override, Literal, Annotated
 from typing_extensions import TypedDict
 import json
 
@@ -6,7 +6,8 @@
 from pydantic import Field, BaseModel, Discriminator
 
 from graphcore.tools.schemas import (
-    WithAsyncImplementation, WithImplementation, WithInjectedId, WithInjectedState,
+    WithAsyncDependencies, WithAsyncImplementation, WithImplementation, WithInjectedId,
+    WithInjectedState,
 )
 from graphcore.graph import tool_state_update
 from graphcore.summary import SummaryConfig
@@ -19,11 +20,12 @@
 from composer.spec.context import WorkflowContext, CVLGeneration, SourceCode
 from composer.spec.prop import PropertyFormulation
 from composer.spec.system_model import ContractComponentInstance, SolidityIdentifier
+from composer.prover.core import DEFAULT_GLOBAL_TIMEOUT
 from composer.spec.source.prover import ProverStateExtra, DELETE_SKIP, VALIDATION_KEY as PROVER_VALIDATION_KEY
 from langgraph.graph import MessagesState
 from langgraph.runtime import get_runtime
-from pathlib import Path
-from composer.spec.gen_types import CVLResource, TypedTemplate, import_statement_for
+from pathlib import Path, PurePosixPath
+from composer.spec.gen_types import CVLResource, MOCKS_DIR, TypedTemplate, import_statement_for
 from composer.spec.service_host import ServiceHost
 from composer.workflow.services import CacheLevel
 
@@ -67,6 +69,72 @@ async def run(self) -> Command:
                 self.rule_name: self.reason
             }
         )
+type RepairStep = Literal["summary_fix", "mock", "optimistic_fallback"]
+
+
+@tool_display(lambda p: f"Acknowledging vacuous method `{p['method']}`", None)
+class AcknowledgeVacuousMethod(
+    WithImplementation[Command], WithInjectedState[ProverStateExtra], WithInjectedId,
+):
+    """
+    Formally acknowledge a method that `verify_spec` flagged as VACUOUS (in a `<vacuity_alert>` /
+    `<vacuity_guard>` block), after the repair ladder failed to fix it. This is the ONLY way to
+    obtain the prover validation stamp while a known-vacuous method is excluded (via `filtered`,
+    `expect_rule_failure`, or rule removal): an unacknowledged vacuous method always withholds
+    the stamp. The feedback judge audits the quality of your acknowledgment, so record honestly
+    which repair-ladder steps you attempted and why each failed. The acknowledgment is cleared
+    automatically if a later run shows the method healthy.
+    """
+    method: str = Field(
+        description="The method's instantiation name exactly as flagged by the prover "
+        "(e.g. `Bank.deposit(uint256)`)"
+    )
+    steps_attempted: list[RepairStep] = Field(
+        description="The repair-ladder steps you actually attempted before acknowledging: "
+        "`summary_fix` (fixing/replacing the offending summary), `mock` (a mock contract via "
+        "`write_mock` + `edit_config`), `optimistic_fallback` (via `edit_config` set_flag). "
+        "Must be non-empty."
+    )
+    justification: str = Field(
+        description="Why each attempted step failed to repair the vacuity, concretely "
+        "(compiler/prover output, persisting sanity failure, etc.). The feedback judge "
+        "reads this verbatim."
+    )
+
+    @override
+    def run(self) -> Command:
+        known = self.state.get("vacuous_methods", {})
+        if self.method not in known:
+            return tool_state_update(
+                self.tool_call_id,
+                f"Method {self.method!r} is not currently flagged as vacuous. "
+                + (f"Currently flagged: {', '.join(sorted(known))}." if known
+                   else "No methods are currently flagged."),
+            )
+        if not self.steps_attempted:
+            return tool_state_update(
+                self.tool_call_id,
+                "At least one attempted repair-ladder step is required: acknowledge a vacuous "
+                "method only after genuinely attempting to repair the setup.",
+            )
+        if not self.justification.strip():
+            return tool_state_update(
+                self.tool_call_id,
+                "A non-empty justification is required: describe why each attempted "
+                "repair-ladder step failed.",
+            )
+        record = json.dumps({
+            "steps_attempted": sorted(set(self.steps_attempted)),
+            "justification": self.justification,
+        })
+        return tool_state_update(
+            self.tool_call_id,
+            f"Acknowledged {self.method} as vacuous. The feedback judge will audit this "
+            "justification; rerun `verify_spec` to obtain the validation stamp.",
+            acknowledged_vacuous={self.method: record},
+        )
+
+
 @tool_display(
     lambda p: f"Expecting rule `{p["rule_name"]}` to pass", None
 )
@@ -245,8 +313,83 @@ class RemoveLink(BaseModel):
     source_contract_name : SolidityIdentifier = Field(description="The Solidity identifier of the contract whose link should be removed")
     link_field_name : str = Field(description="The storage field holding the link within `source_contract_name` that should be removed")
 
-type ConfigEdit = Annotated[RemoveLink | AddLink | AddFile | RemoveFile, Discriminator("type")]
+# Agent-facing cost/soundness clamps for SetProverFlag (owner decision):
+#   * global_timeout may be raised to at most 2x the pipeline default the prover runs
+#     with anyway (DEFAULT_GLOBAL_TIMEOUT, the single source `make_prover_options`
+#     applies) — run cost stays owner-bounded, not agent-controlled.
+#   * loop_iter is capped at 5 unrollings.
+#   * optimistic_fallback is ADD-ONLY: the agent may enable it (repair-ladder step 3)
+#     but may never set it false — that could revert an autosetup-emitted
+#     recommendation, silently re-introducing the vacuity the flag was recommended for.
+_MAX_GLOBAL_TIMEOUT = 2 * int(DEFAULT_GLOBAL_TIMEOUT)
+_MAX_LOOP_ITER = 5
+
+type ProverFlagName = Literal[
+    "optimistic_fallback", "loop_iter", "global_timeout", "contract_recursion_limit"
+]
+
+
+class SetProverFlag(BaseModel):
+    # An explicit __doc__ (rather than a docstring literal) so the tool description the
+    # LLM sees carries the computed clamp bounds instead of hardcoded copies of them.
+    __doc__ = f"""
+    Set a whitelisted top-level prover flag in the configuration:
+
+    * `optimistic_fallback` (bool, add-only — may only be set to `true`): assume unresolved
+      low-level calls (`.call{{value: ...}}`, `send`, `transfer`) succeed instead of HAVOCing
+      and always being able to fail. Step 3 of the vacuity repair ladder. Setting it back to
+      `false` is not allowed (it could revert an autosetup recommendation).
+    * `loop_iter` (int, 1-{_MAX_LOOP_ITER}): the number of loop unrollings the prover performs.
+    * `global_timeout` (int, 1-{_MAX_GLOBAL_TIMEOUT}): the overall run timeout in seconds
+      (capped at twice the pipeline default).
+    * `contract_recursion_limit` (int, 0-10): the allowed depth of recursive calls between contracts.
+    """
+    # `rule_sanity` and `optimistic_loop` are DELIBERATELY not in this whitelist: vacuity
+    # detection (composer/prover/vacuity.py) depends on `rule_sanity: basic`, and
+    # `prover_config_overlay` sets both AFTER spreading the base config so they would win
+    # anyway — the whitelist keeps the agent from even trying (and from being confused by a
+    # silently-overridden edit).
+    type: Literal["set_flag"]
+    flag: ProverFlagName
+    value: bool | int = Field(description="The value to set: a bool for `optimistic_fallback`, an int for the other flags")
+
+def _validate_prover_flag(flag: ProverFlagName, value: bool | int) -> str | None:
+    """Per-flag validation for SetProverFlag; returns an error message or None if valid.
+
+    NB: ``bool`` is a subclass of ``int``, so the bool checks must come before any int check.
+    """
+    if flag == "optimistic_fallback":
+        if not isinstance(value, bool):
+            return f"optimistic_fallback expects a boolean value, got {value!r}"
+        if value is False:
+            return (
+                "optimistic_fallback is add-only: it may be set to true (repair-ladder "
+                "step 3) but never back to false — autosetup may have recommended it, and "
+                "unsetting that recommendation would re-introduce the vacuity it prevents"
+            )
+        return None
+    if isinstance(value, bool) or not isinstance(value, int):
+        return f"{flag} expects an integer value, got {value!r}"
+    match flag:
+        case "loop_iter":
+            if not (1 <= value <= _MAX_LOOP_ITER):
+                return f"loop_iter must be between 1 and {_MAX_LOOP_ITER}, got {value}"
+        case "global_timeout":
+            if not (1 <= value <= _MAX_GLOBAL_TIMEOUT):
+                return (
+                    f"global_timeout must be between 1 and {_MAX_GLOBAL_TIMEOUT} (seconds, "
+                    f"at most twice the pipeline default), got {value}"
+                )
+        case "contract_recursion_limit":
+            if not (0 <= value <= 10):
+                return f"contract_recursion_limit must be between 0 and 10, got {value}"
+    return None
+
+type ConfigEdit = Annotated[RemoveLink | AddLink | AddFile | RemoveFile | SetProverFlag, Discriminator("type")]
 
+@tool_display(
+    lambda p: f"Editing prover configuration ({len(p['edits'])} edit(s))", None
+)
 class ConfigEditTool(WithAsyncImplementation[Command | str], WithInjectedId, WithInjectedState[ProverStateExtra]):
     """
     Call this tool to make a edits to the prover configuration.
@@ -322,6 +465,10 @@ async def run(self) -> Command | str:
                     if not found:
                         return f"No existing link found that matches {src}:{fld}"
                     curr_config["link"] = new_links
+                case SetProverFlag(flag=flag, value=value):
+                    if (err := _validate_prover_flag(flag, value)) is not None:
+                        return err
+                    curr_config[flag] = value
 
         return tool_state_update(
             self.tool_call_id,
@@ -330,6 +477,96 @@ async def run(self) -> Command | str:
         )
 
 
+@tool_display(lambda p: f"Writing mock `{p['file_name']}`", None)
+class WriteMockTool(WithAsyncDependencies[Command | str, str], WithInjectedId):
+    """
+    Write a minimal Solidity mock contract implementing an interface, so the prover can resolve
+    calls to an otherwise-unresolved callee (step 2 of the vacuity repair ladder). The mock is
+    recorded against this generation's own `certora/mocks/` subdirectory and materialized on
+    disk for every prover run; the tool response names the exact project-root-relative path.
+    After writing the mock, register that path in the prover configuration with `edit_config`
+    (an `add_file` edit, plus an `add_link` edit if the callee is reached through a storage
+    field).
+
+    Keep the mock as small as possible: implement only the interface the caller needs, but
+    preserve the semantics that matter to the calling contract — in particular a `payable`
+    callee must remain `payable`. Writing an existing file name overwrites it, so you can
+    iterate on a mock in place.
+    """
+    # The bound dependency is the generation's namespace (its spec stem): mocks are held in
+    # graph state and materialized under certora/mocks/<namespace>/ only around prover runs,
+    # so concurrent batch generations never mutate shared paths in the project tree (the
+    # same isolation the tmp_spec idiom gives curr_spec).
+    file_name: str = Field(description="Bare file name for the mock, e.g. `MockOracle.sol` (no directories — the tool chooses this generation's mocks directory)")
+    content: str = Field(description="The full Solidity source of the mock contract")
+
+    @override
+    async def run(self) -> Command | str:
+        name = PurePosixPath(self.file_name)
+        if len(name.parts) != 1 or name.parts[0] in (".", ".."):
+            return f"Invalid file name `{self.file_name}`: provide a bare file name without directories"
+        if name.suffix != ".sol":
+            return f"Mock must be a Solidity source file (`.sol`), got `{self.file_name}`"
+        with self.tool_deps() as namespace:
+            rel = PurePosixPath(MOCKS_DIR.as_posix()) / namespace / name
+        return tool_state_update(
+            self.tool_call_id,
+            f"Recorded mock `{rel}`; it will be materialized there for every prover run. "
+            "Remember to register it in the prover configuration via `edit_config` "
+            f"(`add_file` with `{rel}`, plus `add_link` if the callee is reached through "
+            "a storage field).",
+            mocks={str(rel): self.content},
+        )
+
+
+def vacuity_judge_evidence(state: Mapping[str, Any]) -> list[str | dict]:
+    """The prover-side evidence the feedback judge audits (Criteria 5's
+    filter-legitimacy taxonomy): outstanding vacuity verdicts, the rule-skip
+    map with its recorded reasons, and the acknowledged-vacuous ledger, passed
+    verbatim from the generation's graph state.
+
+    Wired as the ``extra_inputs`` thunk of ``property_feedback_judge`` at the
+    ``batch_cvl_generation`` call site — the judge cannot re-derive any of this
+    from the CVL text, because vacuity is a prover-run observation, not a
+    spec-text property. Evaluated per feedback round over the then-current
+    state. Empty state contributes nothing (the natreq-style silent default).
+    """
+    parts: list[str | dict] = []
+    vacuous: dict[str, str] = state.get("vacuous_methods") or {}
+    if vacuous:
+        parts.append(
+            "The prover flagged the following method(s) as VACUOUS (their sanity check "
+            "failed: every rule instantiated with them passes trivially). Verdicts clear "
+            "automatically once a run shows the method healthy — these are still "
+            "outstanding:\n" + "\n".join(f"  - {m}: {d}" for m, d in sorted(vacuous.items()))
+        )
+    rule_skips: dict[str, str] = state.get("rule_skips") or {}
+    if rule_skips:
+        parts.append(
+            "The author marked the following rule(s) as \"expected to fail\" (excluded "
+            "from the prover pass/fail verdict), with these reasons:\n"
+            + "\n".join(f"  - {r}: {reason}" for r, reason in sorted(rule_skips.items()))
+        )
+    acks: dict[str, str] = state.get("acknowledged_vacuous") or {}
+    if acks:
+        lines: list[str] = []
+        for m, record in sorted(acks.items()):
+            try:
+                rec = json.loads(record)
+                lines.append(
+                    f"  - {m}: steps attempted: {', '.join(rec['steps_attempted'])}; "
+                    f"justification: {rec['justification']}"
+                )
+            except (ValueError, KeyError, TypeError):
+                lines.append(f"  - {m}: {record}")
+        parts.append(
+            "The acknowledged-vacuous ledger (structured records from the "
+            "`acknowledge_vacuous_method` tool — audit each acknowledgment on its merits "
+            "per the Criteria 5 taxonomy):\n" + "\n".join(lines)
+        )
+    return parts
+
+
 _PropertyGenTemplate = TypedTemplate[PropertyGenParams]("property_generation_prompt.j2")
 
 async def batch_cvl_generation(
@@ -343,10 +580,14 @@ async def batch_cvl_generation(
     description: str,
     source: SourceCode,
     spec_dir: Path,
+    mock_namespace: str,
 ) -> BatchGeneratedCVLResult:
     # *spec_dir* (project-root-relative) is where the caller will persist the spec
     # authored here. The prover resolves the spec's CVL imports relative to its own
     # directory, so resource imports are expressed relative to *spec_dir*.
+    # *mock_namespace* (the spec's stem) names this generation's private
+    # certora/mocks/<namespace>/ subdirectory: write_mock records mocks against it, so
+    # concurrent batch generations can never clobber each other's mock files.
     resource_views: list[ResourceView] = [
         {
             "description": r.description,
@@ -371,7 +612,19 @@ async def batch_cvl_generation(
     ).with_tools(
         static_tools()
     ).with_tools(
-        [prover_tool, ExpectRulePassage.as_tool("expect_rule_passage"), ExpectRuleFailure.as_tool("expect_rule_failure"), GiveUpTool.as_tool("give_up"), PublishResultTool.as_tool("result"), ctx.get_memory_tool()]
+        [
+            prover_tool, ExpectRulePassage.as_tool("expect_rule_passage"), ExpectRuleFailure.as_tool("expect_rule_failure"),
+            GiveUpTool.as_tool("give_up"), PublishResultTool.as_tool("result"),
+            # Setup-repair tools for the vacuity repair ladder: edit_config covers ladder
+            # steps 2 (register a mock via add_file/add_link) and 3 (optimistic_fallback via
+            # set_flag); write_mock produces the step-2 mock itself;
+            # acknowledge_vacuous_method is the structured last-resort ledger entry the
+            # verify_spec stamp gate and the feedback judge consult.
+            ConfigEditTool.as_tool("edit_config"),
+            WriteMockTool.bind(mock_namespace).as_tool("write_mock"),
+            AcknowledgeVacuousMethod.as_tool("acknowledge_vacuous_method"),
+            ctx.get_memory_tool(),
+        ]
     ).with_state(
         SourceCVLGenerationState
     ).with_output_key(
@@ -390,7 +643,10 @@ async def batch_cvl_generation(
         ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({
             "sort": "existing",
             "context": component
-        }), props
+        }), props,
+        # Vacuity verdicts, rule skips, and acknowledgments reach the judge with
+        # every feedback round — the evidence Criteria 5's taxonomy audits.
+        extra_inputs=vacuity_judge_evidence,
     )
 
     res_state = await run_cvl_generator(
@@ -404,6 +660,9 @@ async def batch_cvl_generation(
             input=[],
             required_validations=[FEEDBACK_VALIDATION_KEY, PROVER_VALIDATION_KEY],
             rule_skips={},
+            vacuous_methods={},
+            acknowledged_vacuous={},
+            mocks={},
             skipped=[],
             property_rules=[],
             validations={},
@@ -417,14 +676,16 @@ async def batch_cvl_generation(
         return GaveUp(reason=res_state["result"])
     d = res_state["curr_spec"]
     assert d is not None
-    # Persist the base prover config and last run link from the final state so a later cache
-    # hit (which skips the prover) can still reconstruct certora/confs and retain the link.
+    # Persist the base prover config, mocks, and last run link from the final state so a
+    # later cache hit (which skips the prover) can still reconstruct certora/confs — and
+    # the mock files those confs reference — and retain the link.
     return GeneratedCVL(
         commentary=res_state["result"],
         cvl=d,
         skipped=res_state["skipped"],
         property_rules=res_state["property_rules"],
         config=res_state["config"],
+        mocks=res_state["mocks"],
         final_link=res_state.get("prover_link"),
     )
 
diff --git a/composer/spec/source/common_pipeline.py b/composer/spec/source/common_pipeline.py
index dac066d1..1458fa34 100644
--- a/composer/spec/source/common_pipeline.py
+++ b/composer/spec/source/common_pipeline.py
@@ -182,6 +182,7 @@ async def _generate_batch(
                 description=label,
                 source=source_input,
                 spec_dir=SPECS_DIR,
+                mock_namespace=ComponentSpec(batch.feat.slugified_name).stem,
             ),
             semaphore,
         )
diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py
index 5799f162..d1c49d9b 100644
--- a/composer/spec/source/pipeline.py
+++ b/composer/spec/source/pipeline.py
@@ -255,6 +255,7 @@ async def stream_bugs():
                     description="Structural invariant CVL",
                     source=source_input,
                     spec_dir=SPECS_DIR,
+                    mock_namespace=InvariantSpec().stem,
                 ),
             )
             if isinstance(inv_cvl_result, GaveUp):
diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py
index c88490ad..66d5d083 100644
--- a/composer/spec/source/prover.py
+++ b/composer/spec/source/prover.py
@@ -14,7 +14,7 @@
 import time
 from contextlib import contextmanager
 from pathlib import Path
-from typing import Annotated, Callable, Iterator, override, AsyncContextManager
+from typing import Annotated, Callable, Iterator, cast, override, AsyncContextManager
 from typing_extensions import TypedDict, NotRequired
 
 from langchain_core.tools import InjectedToolCallId, tool, BaseTool
@@ -27,8 +27,9 @@
 from graphcore.graph import LLM
 
 from composer.prover.core import (
-    ProverOptions, ProverCallbacks, run_prover, DefaultCexHandler
+    ProverOptions, ProverCallbacks, ProverReport, run_prover, DefaultCexHandler
 )
+from composer.prover.vacuity import format_vacuity_guard
 from composer.prover.callbacks import ProverEventCallbacks
 from composer.ui.tool_display import tool_display
 from composer.diagnostics.stream import (
@@ -39,7 +40,7 @@
 from composer.diagnostics.timing import RunSummary, get_run_summary
 from graphcore.graph import tool_state_update
 from composer.spec.util import temp_certora_file
-from composer.spec.gen_types import SPECS_DIR
+from composer.spec.gen_types import MOCKS_DIR, SPECS_DIR
 
 
 _logger = logging.getLogger("composer.prover")
@@ -50,6 +51,11 @@ def prover_config_overlay(base_config: dict, *, main_contract: str, verify_targe
 
     Shared by the live ``verify_spec`` run and the persisted ``certora/confs`` dump so the
     two can't drift. ``verify_target`` is the ``<contract>:<spec path>`` the run verifies.
+
+    ``rule_sanity``/``optimistic_loop`` are set AFTER the base-config spread, so they win
+    over anything the agent's config edits put in ``base_config``. Vacuity detection
+    (``composer/prover/vacuity.py``) depends on ``rule_sanity: basic`` being forced here —
+    which is also why ``edit_config``'s ``SetProverFlag`` refuses those two flags.
     """
     return {
         **base_config,
@@ -83,6 +89,27 @@ class ProverStateExtra(TypedDict):
     # Link of the last prover run this generation performed (URL or local results dir).
     # Last-write-wins; absent until the first prover run. Read at completion onto GeneratedCVL.
     prover_link: NotRequired[str | None]
+    # Methods detected as vacuous by prior prover runs (instantiation name -> diagnosis).
+    # Must persist across verify_spec calls: once the agent excludes a vacuous method with a
+    # `filtered` block, later runs never re-instantiate it, so per-run detection alone would
+    # forget it. Shares the DELETE_SKIP-sentinel reducer with rule_skips — an entry is cleared
+    # when a later run instantiates the method without a sanity failure.
+    vacuous_methods: Annotated[dict[str, str], _merge_rule_skips]
+    # Agent-written mock contracts (project-root-relative path under the generation's
+    # certora/mocks/<stem>/ namespace -> Solidity source), written by the write_mock tool.
+    # State-held rather than written to disk so concurrent batch generations never mutate
+    # the shared project tree: verify_spec materializes them for the duration of a prover
+    # run, and the artifact store persists them (with the conf that references them) only
+    # for completed generations. Shares the DELETE_SKIP reducer idiom of rule_skips.
+    mocks: Annotated[dict[str, str], _merge_rule_skips]
+    # The acknowledged-vacuous ledger (instantiation name -> JSON record with
+    # `steps_attempted` and `justification`), written by the acknowledge_vacuous_method
+    # tool. The verify_spec stamp gate is `known_vacuous - acknowledged`: an acknowledged
+    # method no longer withholds the stamp, and the feedback judge audits the record's
+    # quality. An entry is cleared alongside its vacuity verdict when a run shows the
+    # method healthy, so a method that later turns vacuous *again* needs a fresh
+    # acknowledgment.
+    acknowledged_vacuous: Annotated[dict[str, str], _merge_rule_skips]
 
 type ProverEvents = CEXAnalysisStart | CloudPollingEvent | ProverOutputEvent | RuleAnalysisResult | ProverRun | ProverLink | ProverResult
 
@@ -156,6 +183,36 @@ async def on_prover_result(self, results: dict[str, RuleResult]) -> None:
         )
 
 
+def _vacuity_state_update(
+    state: ProverStateExtra, result: ProverReport
+) -> tuple[dict[str, str], dict[str, str], set[str]]:
+    """Fold this run's vacuity view into the persisted ``vacuous_methods`` state.
+
+    Returns ``(update, ack_update, known_vacuous)``: the reducer delta to merge
+    into ``vacuous_methods`` (newly detected methods added, previously-recorded
+    methods that this run instantiated *without* a sanity failure cleared via
+    DELETE_SKIP), the companion delta clearing ``acknowledged_vacuous`` entries
+    whose verdict just cleared (so a method that turns vacuous again later needs
+    a fresh acknowledgment), and the resulting set of methods still considered
+    vacuous — the set the stamp gate checks against. ``state.get`` tolerates
+    checkpoints predating these fields.
+    """
+    prior = state.get("vacuous_methods", {})
+    acks = state.get("acknowledged_vacuous", {})
+    update: dict[str, str] = {m: ev.diagnosis for m, ev in result.vacuous_methods.items()}
+    for m in prior:
+        if m in result.instantiated_methods and m not in result.vacuous_methods:
+            update[m] = DELETE_SKIP
+    ack_update = {
+        m: DELETE_SKIP for m, v in update.items() if v == DELETE_SKIP and m in acks
+    }
+    known_vacuous = {
+        m for m in (set(prior) | set(result.vacuous_methods))
+        if update.get(m) != DELETE_SKIP
+    }
+    return update, ack_update, known_vacuous
+
+
 class VerifySpecSchema(BaseModel):
     """
     Run the Certora prover to verify the current spec against the source code.
@@ -195,6 +252,44 @@ def tmp_spec(
     ) as tmp:
         yield tmp
 
+@contextmanager
+def materialized_mocks(root: str, mocks: dict[str, str]) -> Iterator[None]:
+    """Materialize the generation's state-held mock files onto the real project
+    tree for the duration of a prover run (the prover compiles from disk), then
+    remove them.
+
+    Mock paths are namespaced per generation (``certora/mocks/<spec stem>/``),
+    so concurrent batch generations write disjoint files and never observe each
+    other's mocks mid-compile. Removing them afterward keeps gave-up generations
+    from leaving stray sources behind; completed generations get their mocks
+    persisted by the artifact store alongside the conf that references them.
+    """
+    written: list[Path] = []
+    for rel, content in mocks.items():
+        target = Path(root) / rel
+        target.parent.mkdir(parents=True, exist_ok=True)
+        target.write_text(content)
+        written.append(target)
+    try:
+        yield
+    finally:
+        for target in written:
+            target.unlink(missing_ok=True)
+        # Also drop the namespace dirs we created (up to and including the
+        # mocks root, never above it) so gave-up generations leave no empty
+        # directories behind. rmdir refuses non-empty dirs, so a concurrent
+        # generation's still-materialized mocks are never disturbed.
+        mocks_root = Path(root) / MOCKS_DIR
+        for target in written:
+            directory = target.parent
+            while directory == mocks_root or mocks_root in directory.parents:
+                try:
+                    directory.rmdir()
+                except OSError:
+                    break
+                directory = directory.parent
+
+
 def _prover_sem(cloud: bool) -> AsyncContextManager[None]:
     if not cloud:
         return asyncio.Semaphore(1)
@@ -242,7 +337,7 @@ async def verify_spec(
                 content=json.dumps(config, indent=2),
                 ext="conf",
                 prefix="verify"
-            ) as config_path:
+            ) as config_path, materialized_mocks(project_root, state.get("mocks", {})):
                 async with sem:
                     result = await run_prover(
                         Path(project_root),
@@ -255,6 +350,7 @@ async def verify_spec(
 
             if isinstance(result, str):
                 return result
+            vacuity_update, ack_update, known_vacuous = _vacuity_state_update(state, result)
             all_verified = True
             for (r, stat) in result.rule_status.items():
                 if r in state["rule_skips"]:
@@ -263,12 +359,47 @@ async def verify_spec(
                     all_verified = False
                     break
             if rules is None and all_verified:
+                # HARD GUARD, purely structural: a persisted vacuity verdict only clears
+                # when a run instantiates the method without a sanity failure, so ANY
+                # route that hides the method while it is still broken — a `filtered`
+                # block, `expect_rule_failure` on its sanity-failing rules (dropping
+                # them from the all_verified check above), even deleting the rule —
+                # leaves the verdict outstanding. Withhold the PROVER validation stamp
+                # while any known-vacuous method lacks an acknowledged_vacuous ledger
+                # entry (written by the acknowledge_vacuous_method tool; the feedback
+                # judge audits the entry's quality).
+                unacknowledged = known_vacuous - set(state.get("acknowledged_vacuous", {}))
+                if unacknowledged:
+                    prior_verdicts = state.get("vacuous_methods", {})
+                    blocked = {
+                        m: (result.vacuous_methods[m].diagnosis
+                            if m in result.vacuous_methods else prior_verdicts[m])
+                        for m in unacknowledged
+                    }
+                    return tool_state_update(
+                        tool_call_id=tool_call_id,
+                        content="\n\n".join([result.result_str, format_vacuity_guard(blocked)]),
+                        prover_link=result.link, vacuous_methods=vacuity_update,
+                        acknowledged_vacuous=ack_update,
+                    )
+                # Stamp over the POST-update state: this same Command may clear
+                # acknowledged_vacuous entries (ack_update), and the ledger is part of
+                # the validation digest — stamping the pre-update state would yield a
+                # digest check_completion can never match.
+                effective = cast(StateWithSkips, {
+                    **state,
+                    "acknowledged_vacuous": _merge_rule_skips(
+                        state.get("acknowledged_vacuous", {}), ack_update
+                    ),
+                })
                 return tool_state_update(
                     tool_call_id=tool_call_id, content=result.result_str,
-                    prover_link=result.link, validations=stamper(state),
+                    prover_link=result.link, validations=stamper(effective),
+                    vacuous_methods=vacuity_update, acknowledged_vacuous=ack_update,
                 )
             return tool_state_update(
-                tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link
+                tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link,
+                vacuous_methods=vacuity_update, acknowledged_vacuous=ack_update,
             )
 
     return verify_spec
diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2
index d96585cc..1bef0e1a 100644
--- a/composer/templates/property_generation_prompt.j2
+++ b/composer/templates/property_generation_prompt.j2
@@ -75,21 +75,47 @@ feedback as soon as possible.
     (unknown) callee contract's state, you should use "ghost variables" to model this.
   + If the call was completely unresolved (no resolved selector/signature), consider using a "dispatch list"
     summary. Analyze the location of the unresolved call, and consider what the callee functions might be.
+  + If the unresolved call is a low-level `.call{value: ...}`/`send`/`transfer` with no resolvable target,
+    the HAVOC also lets the call *always fail*, which can make the caller revert on every path. Setting
+    `optimistic_fallback` via the `edit_config` tool (`set_flag`) assumes such calls succeed instead.
   + Do *NOT* try to mark ghost state as `persistent` to work around the HAVOC issue.
   + Do *NOT* apply a `NONDET` summary to a side-effecting function to make the HAVOC "go away", this makes
     the verification results useless.
 * If the counterexample appears to point to a potential issue in the code that should be reviewed by a security expert,
   use the "expect fail" tool to mark that the rule failure may be legitimate.
+* If the property or invariant is genuinely incorrect or actually invalid you may mark the property as "skipped" and
+  remove your attempts to formalize it from the spec
+* If the rule is failing due to a `SANITY_FAILURE`, this is due to the assertion in the rule/invariant being unreachable.
+  Diagnose which of two distinct root causes you are facing before acting:
+  + If the sanity failure is specific to a single rule, the preconditions in the rule and the logical encoding of the
+    implementation's code are themselves mutually unsatisfiable. In this case, you should try to identify places where
+    `require` statements in your rule may conflict with any assumptions/requirements in the code.
+  + If the *same method* sanity-fails across several rules that instantiate it (the prover report will flag this with a
+    `<vacuity_alert>` block), the method reverts on *every* path under the current verification model, and every rule
+    instantiated with it passes vacuously. This is almost always a SETUP defect, not a property error — canonically a
+    `NONDET`/`CONSTANT` summary on a payable or side-effecting callee, an unresolved `.call{value: ...}` that HAVOCs,
+    or a missing `link`. Repair it in this order (the "repair ladder"); do NOT jump to a later step without attempting
+    the earlier ones:
+    1. Fix or replace the offending summary so it preserves the callee's semantics — in particular payable-ness:
+       a payable callee must be able to accept the transferred value.
+    2. Write a minimal mock contract under `certora/mocks` with the `write_mock` tool, implementing the callee's
+       interface, and register it in the prover config with `edit_config` (`add_file`, plus `add_link` if the callee
+       is reached through a storage field).
+    3. Set `optimistic_fallback` to true via `edit_config` (`set_flag`) so unresolved calls are assumed to succeed
+       instead of always being able to revert.
+    4. ONLY as a last resort, acknowledge the method with the `acknowledge_vacuous_method` tool and then
+       exclude it with a `filtered` block — see below.
 * If you have a parametric rule or invariant that is persistently failing on a method, and that method should
   genuinely be excluded from the property/invariant being proven, use a `filtered` block to exclude it.
   + You should not use this strategy lightly; only do so when you are 95% certain that the method in question
     should be excluded from the property.
-* If the property or invariant is genuinely incorrect or actually invalid you may mark the property as "skipped" and
-  remove your attempts to formalize it from the spec
-* If the rule is failing due to a `SANITY_FAILURE`, this is due to the assertion in the rule/invariant being unreachable.
-  In other words, the preconditions in the rule and the logical encoding of the implementation's code are themselves
-  mutually unsatisfiable. In this case, you should try to identify places where `require` statements in your rule
-  may conflict with any assumptions/requirements in the code.
+  + NEVER hide a *vacuous* method (one flagged in a `<vacuity_alert>`) — whether via a `filtered` block, via
+    `expect_rule_failure` on its sanity-failing rules, or by deleting the rule: that hides a setup defect instead
+    of fixing it, and the prover validation stamp will be withheld while the vacuity verdict is outstanding. The
+    verdict clears only when a prover run shows the method instantiated without a sanity failure. If steps 1-3 of
+    the repair ladder genuinely failed, formally acknowledge the method with the `acknowledge_vacuous_method`
+    tool, recording which steps (`summary_fix` / `mock` / `optimistic_fallback`) you attempted and why each
+    failed; the feedback judge audits the quality of that acknowledgment.
 * For any other logical errors/issues not described here, address the changes in a methodical way. Use your
   adaptive thinking and the cvl researcher to come to *principled* solutions. Do *NOT* try to brute force
   the solution by trying random changes.
diff --git a/composer/templates/property_generation_system_prompt.j2 b/composer/templates/property_generation_system_prompt.j2
index 6a3cd772..48eec589 100644
--- a/composer/templates/property_generation_system_prompt.j2
+++ b/composer/templates/property_generation_system_prompt.j2
@@ -25,3 +25,9 @@ are good reasons to use this "expect failure" functionality:
   the rule failure is the intended result.
 2. Verifying the rule is hitting some limitation in the prover (including prover errors, etc.),
    and you have exhausted all reasonable alternative formulations to work around these prover limitations (errors, timeouts, imprecision).
+
+A `SANITY_FAILED` rule whose method was flagged VACUOUS (in a `<vacuity_alert>`) is NEVER a good reason: marking such
+rules "expected to fail" hides a setup defect exactly like filtering the method would, and the prover validation stamp
+will be withheld while the vacuity verdict is outstanding. The verdict clears only when a prover run shows the method
+healthy or when you formally acknowledge it with the `acknowledge_vacuous_method` tool (recording which repair-ladder
+steps you attempted and why each failed — the feedback judge audits that record).
diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2
index 537b2afc..1f555c78 100644
--- a/composer/templates/property_judge_prompt.j2
+++ b/composer/templates/property_judge_prompt.j2
@@ -140,6 +140,22 @@ Consider if any of the summaries added in the spec *trivialize* the verification
 if the specification summarizes away an invocation of a contract function which moves balances as "NONDET", then this effectively makes any balance
 transfers a NO-OP, which in turn trivializes any property that reasons about balances.
 
+A `NONDET` summary on a *payable* callee deserves explicit scrutiny: it drops the callee's ability to accept `msg.value`, which typically makes
+every caller revert on all paths, so any rule instantiated with those callers holds *vacuously*.
+
+A `filtered` block that excludes a method whose sanity failure stems from such a repairable summary is the same trivialization in disguise:
+the setup defect is hidden rather than fixed, and the property silently loses coverage of that method. A method exclusion (a `filtered`
+block, or an "expected to fail" marking of the affected rules) is legitimate in exactly two cases:
+1. The excluded method is a *documented harness helper* — verification-only scaffolding the harness exposes, not production behavior — and
+   the exclusion keeps helper-only transitions out of a production-behavior property.
+2. The excluded method appears in the *acknowledged-vacuous ledger* provided in your inputs (when available): the author formally
+   acknowledged the method as vacuous, recording which repair-ladder steps were attempted (summary fix preserving payable semantics /
+   mock for the callee / `optimistic_fallback`) and why each failed. Audit that record on its merits — an acknowledgment whose
+   justification is vague, does not match the recorded steps, or skips obviously-applicable repair steps must be rejected just like
+   an unacknowledged exclusion.
+Any other exclusion of a vacuously-passing method must be rejected. When your inputs include vacuity verdicts and rule-skip reasons,
+cross-check them: an exclusion of a method flagged vacuous with no matching ledger entry is never acceptable.
+
 ### Criteria 6: Manifest Errors
 
 {% if sort != "greenfield" %}
diff --git a/tests/test_autosetup_vacuity_prevention.py b/tests/test_autosetup_vacuity_prevention.py
new file mode 100644
index 00000000..d82d439a
--- /dev/null
+++ b/tests/test_autosetup_vacuity_prevention.py
@@ -0,0 +1,185 @@
+"""
+Tests for the autosetup-side vacuity prevention (plan Part D):
+
+- NONDET recipes never match payable / state-mutating methods
+  (``SummarySetup._nondet_ineligible`` + the recipe-level mutability bounds);
+- unresolved low-level value transfers yield an ``optimistic_fallback``
+  recommendation (``is_unresolved_value_transfer``);
+- ``ConfigManager`` merges recommended flags only through its whitelist.
+"""
+import json
+
+import pytest
+
+from certora_autosetup.setup.call_resolution import is_unresolved_value_transfer
+from certora_autosetup.setup.setup_summaries import Recipe, RecipeType, SummarySetup
+from certora_autosetup.utils.enhanced_config_manager import ConfigManager
+
+from prover_output_utility.models import CallResolutionInfo
+
+
+# ---------------------------------------------------------------------------
+# NONDET recipe eligibility
+# ---------------------------------------------------------------------------
+
+
+_NONDET_RECIPE = Recipe(
+    recipe_type=RecipeType.CUSTOM,
+    characteristic="anything",
+    properties={},
+    summary_type="NONDET",
+)
+
+
+def _method(name: str, mutability: str, contract: str = "Bank") -> dict:
+    return {"contractName": contract, "name": name, "stateMutability": mutability}
+
+
+class TestNondetIneligible:
+    def test_payable_excluded(self):
+        m = _method("deposit", "payable")
+        assert SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, {("Bank", "deposit")})
+
+    def test_payable_excluded_even_without_key(self):
+        """The mutability fallback catches a payable method missing from the key set."""
+        m = _method("deposit", "payable")
+        assert SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, set())
+
+    def test_state_mutating_excluded(self):
+        m = _method("withdraw", "nonpayable")
+        assert SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, set())
+
+    def test_view_and_pure_allowed(self):
+        for mutability in ("view", "pure"):
+            m = _method("peek", mutability)
+            assert not SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, set())
+
+    def test_non_nondet_recipe_unaffected(self):
+        recipe = Recipe(
+            recipe_type=RecipeType.NEW_CONTRACT,
+            characteristic="anything",
+            properties={},
+            summary_type="HAVOC_ALL_DELETE",
+        )
+        m = _method("deploy", "payable")
+        assert not SummarySetup._nondet_ineligible(recipe, m, {("Bank", "deploy")})
+
+
+def test_default_nondet_recipes_bounded_to_view_pure():
+    """Every default NONDET recipe must declaratively restrict stateMutability to
+    view/pure — the recipe-level arm of the payable-NONDET guard."""
+    # Unbound call with a stub self: SummarySetup.__init__ requires prebuilt
+    # compilation-analysis artifacts, and _build_recipes only touches self.log
+    # (and only on the custom-recipe branch, unused here).
+    class _StubSetup:
+        def log(self, *args, **kwargs):
+            pass
+
+    for recipe in SummarySetup._build_recipes(_StubSetup(), None):
+        if recipe.summary_type.upper() != "NONDET":
+            continue
+        bound = recipe.properties.get("stateMutability")
+        bound_values = bound if isinstance(bound, list) else [bound]
+        assert set(bound_values) <= {"view", "pure"}, (
+            f"NONDET recipe {recipe.recipe_type} admits non-view/pure methods: {bound!r}"
+        )
+
+
+# ---------------------------------------------------------------------------
+# optimistic_fallback recommendation predicate
+# ---------------------------------------------------------------------------
+
+
+def _call(snippet: str, callee: str = "[?].[?]", selector: str | None = None) -> CallResolutionInfo:
+    return CallResolutionInfo(
+        callee_name=callee,
+        caller_name="Bank.withdraw(uint256)",
+        call_site_snippet=snippet,
+        source_location="src/Bank.sol:42",
+        summary="AUTO havoc",
+        is_warning=True,
+        callee_resolution="UNRESOLVED",
+        selector=selector,
+    )
+
+
+class TestUnresolvedValueTransfer:
+    def test_call_value_flagged(self):
+        assert is_unresolved_value_transfer(_call('recipient.call{value: amount}("")'))
+
+    def test_call_value_with_spaces_flagged(self):
+        assert is_unresolved_value_transfer(_call('recipient.call{ value : amount }("")'))
+
+    def test_native_send_and_transfer_flagged(self):
+        assert is_unresolved_value_transfer(_call("payable(to).send(amount)"))
+        assert is_unresolved_value_transfer(_call("payable(to).transfer(amount)"))
+
+    def test_erc20_transfer_with_selector_not_flagged(self):
+        """High-level token.transfer carries a resolvable selector — not a native transfer."""
+        call = _call(
+            "token.transfer(to, amount)",
+            callee="[?].transfer(address,uint256)",
+            selector="0xa9059cbb",
+        )
+        assert not is_unresolved_value_transfer(call)
+
+    def test_plain_unresolved_call_not_flagged(self):
+        assert not is_unresolved_value_transfer(
+            _call("oracle.latestAnswer()", callee="[?].latestAnswer()")
+        )
+
+
+# ---------------------------------------------------------------------------
+# ConfigManager extra-flags whitelist
+# ---------------------------------------------------------------------------
+
+
+@pytest.fixture
+def manager(tmp_path) -> ConfigManager:
+    return ConfigManager(project_root=tmp_path)
+
+
+def _create(manager, tmp_path, **kwargs):
+    spec = tmp_path / "certora" / "specs" / "Bank.spec"
+    spec.parent.mkdir(parents=True, exist_ok=True)
+    spec.write_text("// spec")
+    conf_path = tmp_path / "Bank.conf"
+    return manager.create_config(
+        "Bank", [], [], spec, conf_path=conf_path, **kwargs
+    )
+
+
+class TestExtraFlags:
+    def test_create_config_merges_whitelisted(self, manager, tmp_path):
+        created = _create(
+            manager, tmp_path,
+            extra_flags={"optimistic_fallback": True, "contract_recursion_limit": 2},
+        )
+        conf = json.loads(created.path.read_text())
+        assert conf["optimistic_fallback"] is True
+        assert conf["contract_recursion_limit"] == 2
+
+    def test_create_config_rejects_non_whitelisted(self, manager, tmp_path):
+        # rule_sanity in particular: vacuity detection depends on the forced value.
+        for flag in ("rule_sanity", "optimistic_loop", "loop_iter"):
+            with pytest.raises(ValueError):
+                _create(manager, tmp_path, extra_flags={flag: True})
+
+    def test_create_config_rejects_ill_typed_values(self, manager, tmp_path):
+        with pytest.raises(ValueError):
+            _create(manager, tmp_path, extra_flags={"optimistic_fallback": 1})
+        with pytest.raises(ValueError):
+            _create(manager, tmp_path, extra_flags={"contract_recursion_limit": True})
+        with pytest.raises(ValueError):
+            _create(manager, tmp_path, extra_flags={"contract_recursion_limit": 99})
+
+    def test_apply_extra_flags_updates_existing_conf(self, manager, tmp_path):
+        created = _create(manager, tmp_path)
+        manager.apply_extra_flags(created.path, {"optimistic_fallback": True})
+        conf = json.loads(created.path.read_text())
+        assert conf["optimistic_fallback"] is True
+
+    def test_apply_extra_flags_rejects_non_whitelisted(self, manager, tmp_path):
+        created = _create(manager, tmp_path)
+        with pytest.raises(ValueError):
+            manager.apply_extra_flags(created.path, {"rule_sanity": "none"})
diff --git a/tests/test_config_edit.py b/tests/test_config_edit.py
index 6f261e94..ec97e57c 100644
--- a/tests/test_config_edit.py
+++ b/tests/test_config_edit.py
@@ -5,11 +5,14 @@
 not just correct Command objects.
 """
 import pytest
+from pydantic import ValidationError
 
 from langgraph.graph import MessagesState
 
+from composer.prover.core import DEFAULT_GLOBAL_TIMEOUT
 from composer.spec.source.author import (
-    ConfigEditTool, AddFile, RemoveFile, AddLink, RemoveLink,
+    ConfigEditTool, AddFile, RemoveFile, AddLink, RemoveLink, SetProverFlag,
+    _MAX_GLOBAL_TIMEOUT,
 )
 from composer.spec.source.prover import ProverStateExtra
 
@@ -52,6 +55,12 @@ def _remove_link(src: str, field: str) -> dict:
     return RemoveLink(type="remove_link", source_contract_name=src, link_field_name=field).model_dump()
 
 
+def _set_flag(flag: str, value: bool | int) -> dict:
+    # Raw dict (not SetProverFlag.model_dump()) so tests can exercise values the
+    # schema itself would reject before reaching the per-flag validation.
+    return {"type": "set_flag", "flag": flag, "value": value}
+
+
 def _edit(*edits: dict) -> ToolCallDict:
     return tool_call_raw(_EDIT, edits=list(edits))
 
@@ -200,6 +209,104 @@ async def test_remove_link_not_found(self):
         assert links == ["A:b=C"]
 
 
+# =========================================================================
+# SetProverFlag
+# =========================================================================
+
+
+class TestSetProverFlag:
+    async def test_set_optimistic_fallback(self):
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("optimistic_fallback", True)),
+        ).map_run(_config)
+        assert config["optimistic_fallback"] is True
+
+    async def test_optimistic_fallback_rejects_int(self):
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("optimistic_fallback", 1)),
+        ).map_run(_config)
+        assert "optimistic_fallback" not in config
+
+    async def test_optimistic_fallback_is_add_only(self):
+        """The agent may enable the flag but never disable it — setting false
+        could revert an autosetup-emitted recommendation."""
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("optimistic_fallback", False)),
+        ).map_run(_config)
+        assert "optimistic_fallback" not in config
+
+    async def test_optimistic_fallback_cannot_unset_autosetup_recommendation(self):
+        """An autosetup-recommended true in the base config survives a false edit."""
+        scenario = Scenario(ConfigTestState, TOOL).init(
+            config={"files": [], "optimistic_fallback": True}, rule_skips={},
+        )
+        config = await scenario.turn(
+            _edit(_set_flag("optimistic_fallback", False)),
+        ).map_run(_config)
+        assert config["optimistic_fallback"] is True
+
+    async def test_set_loop_iter(self):
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("loop_iter", 3)),
+        ).map_run(_config)
+        assert config["loop_iter"] == 3
+
+    async def test_loop_iter_out_of_range(self):
+        for bad in (0, 6):
+            config = await _scenario(files=[]).turn(
+                _edit(_set_flag("loop_iter", bad)),
+            ).map_run(_config)
+            assert "loop_iter" not in config
+
+    async def test_loop_iter_rejects_bool(self):
+        """bool is an int subclass; the validator must not accept True as a loop count."""
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("loop_iter", True)),
+        ).map_run(_config)
+        assert "loop_iter" not in config
+
+    async def test_set_global_timeout_at_clamp(self):
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("global_timeout", _MAX_GLOBAL_TIMEOUT)),
+        ).map_run(_config)
+        assert config["global_timeout"] == _MAX_GLOBAL_TIMEOUT
+
+    async def test_global_timeout_clamped_to_twice_default(self):
+        """The ceiling derives from the pipeline default, not a hardcoded cap."""
+        assert _MAX_GLOBAL_TIMEOUT == 2 * int(DEFAULT_GLOBAL_TIMEOUT)
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("global_timeout", _MAX_GLOBAL_TIMEOUT + 1)),
+        ).map_run(_config)
+        assert "global_timeout" not in config
+
+    async def test_set_contract_recursion_limit(self):
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("contract_recursion_limit", 2)),
+        ).map_run(_config)
+        assert config["contract_recursion_limit"] == 2
+
+    async def test_contract_recursion_limit_too_large(self):
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("contract_recursion_limit", 11)),
+        ).map_run(_config)
+        assert "contract_recursion_limit" not in config
+
+    async def test_sanity_and_optimistic_loop_not_settable(self):
+        """The flags vacuity detection depends on (forced by prover_config_overlay)
+        are rejected at the schema level, not just by run-time validation."""
+        for forbidden in ("rule_sanity", "optimistic_loop"):
+            with pytest.raises(ValidationError):
+                SetProverFlag(type="set_flag", flag=forbidden, value=True)  # type: ignore[arg-type]
+
+    async def test_failed_flag_aborts_batch(self):
+        """Atomicity: a rejected flag value rolls back the whole edit list."""
+        config = await _scenario(files=[]).turn(
+            _edit(_set_flag("loop_iter", 3), _set_flag("global_timeout", 99999)),
+        ).map_run(_config)
+        assert "loop_iter" not in config
+        assert "global_timeout" not in config
+
+
 # =========================================================================
 # Multiple edits
 # =========================================================================
diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py
index 85556bdd..8d843e1c 100644
--- a/tests/test_cvl_skips.py
+++ b/tests/test_cvl_skips.py
@@ -6,7 +6,7 @@
 """
 import pytest
 
-from typing import NotRequired, override, Iterable, Callable, Protocol
+from typing import Any, Mapping, NotRequired, override, Iterable, Callable, Protocol
 
 
 from dataclasses import dataclass
@@ -103,7 +103,8 @@ async def dummy_feedback(
     spec: str,
     s: list[SkippedProperty],
     rebuttals: list[Rebuttal],
-    within_tool: str
+    within_tool: str,
+    state: Mapping[str, Any],
 ) -> Feedback:
     return Feedback(good=True, feedback="")
 
@@ -130,6 +131,7 @@ async def impl(
         skipped: list[SkippedProperty],
         rebuttals: list[Rebuttal],
         within_tool: str,
+        state: Mapping[str, Any],
     ) -> Feedback:
         for sk in skipped:
             if sk.property_title not in skippable:
diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py
new file mode 100644
index 00000000..c8cd3cc3
--- /dev/null
+++ b/tests/test_vacuity.py
@@ -0,0 +1,614 @@
+"""
+Unit tests for composer/prover/vacuity.py and the verify_spec vacuity gate:
+vacuous-method detection over synthetic RuleResult sets, alert rendering, the
+acknowledge_vacuous_method ledger tool, and the purely structural hard guard
+that withholds the PROVER validation stamp while any known-vacuous method is
+neither shown healthy by a later run nor acknowledged in the ledger.
+"""
+
+import json
+
+import pytest
+
+from composer.prover.core import ProverReport
+from composer.prover.ptypes import RulePath, RuleResult, StatusCodes
+from composer.prover.vacuity import (
+    VacuityEvidence,
+    detect_vacuous_methods,
+    format_vacuity_alert,
+    instantiated_methods,
+)
+from composer.spec.cvl_generation import check_completion, state_digest
+from composer.spec.source.author import (
+    AcknowledgeVacuousMethod, ConfigEditTool, ExpectRuleFailure, WriteMockTool,
+    vacuity_judge_evidence,
+)
+from composer.spec.source.prover import StateWithSkips, VALIDATION_KEY
+
+from graphcore.testing import Scenario, tool_call_raw, ToolCallDict
+from graphcore.tools.results import result_tool_generator
+
+from .conftest import ProverMock, ProverToolResponse
+
+
+def _res(rule: str, method: str | None, status: StatusCodes) -> RuleResult:
+    return RuleResult(
+        path=RulePath(rule=rule, contract="Bank", method=method),
+        cex_dump=None,
+        status=status,
+    )
+
+
+DEPOSIT = "Bank.deposit(uint256)"
+WITHDRAW = "Bank.withdraw(uint256)"
+
+
+# =========================================================================
+# detect_vacuous_methods
+# =========================================================================
+
+
+class TestDetectVacuousMethods:
+    def test_vacuous_in_all_rules(self):
+        """Sanity-failed in 100% of the (3) instantiating rules -> flagged."""
+        results = [
+            _res(r, DEPOSIT, "SANITY_FAILED") for r in ("ruleA", "ruleB", "ruleC")
+        ]
+        flagged = detect_vacuous_methods(results)
+        assert set(flagged) == {DEPOSIT}
+        assert flagged[DEPOSIT].affected_rules == ["ruleA", "ruleB", "ruleC"]
+        assert "3 of 3" in flagged[DEPOSIT].diagnosis
+
+    def test_vacuous_in_single_rule_run(self):
+        """One rule, one instantiation, sanity-failed: 100% -> flagged."""
+        flagged = detect_vacuous_methods([_res("ruleA", DEPOSIT, "SANITY_FAILED")])
+        assert set(flagged) == {DEPOSIT}
+
+    def test_sanity_failed_in_one_of_many_not_flagged(self):
+        """Failed in 1 of 3 rules: below the >=2 threshold and not 100%."""
+        results = [
+            _res("ruleA", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleB", DEPOSIT, "VERIFIED"),
+            _res("ruleC", DEPOSIT, "VERIFIED"),
+        ]
+        assert detect_vacuous_methods(results) == {}
+
+    def test_two_rules_with_healthy_instantiation_not_flagged(self):
+        """>=2 sanity failures alongside a VERIFIED instantiation are a
+        rule-precondition problem, not method vacuity: a passing rule reached
+        the method's code, disproving all-paths reversion."""
+        results = [
+            _res("ruleA", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleB", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleC", DEPOSIT, "VERIFIED"),
+        ]
+        assert detect_vacuous_methods(results) == {}
+
+    def test_two_rules_with_violated_instantiation_not_flagged(self):
+        """VIOLATED also requires reaching the method's code, so it clears
+        the >=2 arm just like VERIFIED."""
+        results = [
+            _res("ruleA", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleB", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleC", DEPOSIT, "VIOLATED"),
+        ]
+        assert detect_vacuous_methods(results) == {}
+
+    def test_two_rules_flagged_when_others_timeout(self):
+        """TIMEOUT/ERROR can mask an all-paths-reverting method — the >=2 arm
+        still fires when no instantiation reached a healthy verdict."""
+        results = [
+            _res("ruleA", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleB", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleC", DEPOSIT, "TIMEOUT"),
+            _res("ruleD", DEPOSIT, "ERROR"),
+        ]
+        assert set(detect_vacuous_methods(results)) == {DEPOSIT}
+
+    def test_mixed_methods(self):
+        """Only the everywhere-failing method is flagged in a mixed result set."""
+        results = [
+            _res("ruleA", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleB", DEPOSIT, "SANITY_FAILED"),
+            _res("ruleA", WITHDRAW, "VERIFIED"),
+            _res("ruleB", WITHDRAW, "SANITY_FAILED"),
+            _res("ruleC", WITHDRAW, "VIOLATED"),
+        ]
+        assert set(detect_vacuous_methods(results)) == {DEPOSIT}
+
+    def test_non_parametric_sanity_failure_ignored(self):
+        """SANITY_FAILED with no method is a rule problem, not method vacuity."""
+        assert detect_vacuous_methods([_res("ruleA", None, "SANITY_FAILED")]) == {}
+
+    def test_instantiated_methods(self):
+        results = [
+            _res("ruleA", DEPOSIT, "VERIFIED"),
+            _res("ruleB", WITHDRAW, "SANITY_FAILED"),
+            _res("static", None, "VERIFIED"),
+        ]
+        assert instantiated_methods(results) == {DEPOSIT, WITHDRAW}
+
+
+# =========================================================================
+# format_vacuity_alert
+# =========================================================================
+
+
+class TestFormatVacuityAlert:
+    def test_empty_evidence_renders_nothing(self):
+        assert format_vacuity_alert({}) == ""
+
+    def test_alert_contains_ladder_and_methods(self):
+        evidence = detect_vacuous_methods(
+            [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")]
+        )
+        alert = format_vacuity_alert(evidence)
+        assert alert.startswith("<vacuity_alert>")
+        assert alert.endswith("</vacuity_alert>")
+        assert DEPOSIT in alert
+        # Repair ladder ordering: summary fix -> mock -> optimistic_fallback -> filtered.
+        assert (
+            alert.index("Fix or replace the offending summary")
+            < alert.index("write_mock")
+            < alert.index("optimistic_fallback")
+            < alert.index("filtered")
+        )
+
+
+# =========================================================================
+# verify_spec vacuity hard guard (mocked prover)
+# =========================================================================
+
+# The gate is purely structural (persisted verdicts minus the acknowledgment
+# ledger) — the spec text is irrelevant to it, so one spec serves every case:
+# it "hides" the vacuous method simply by not exercising it in run 2.
+_SPEC = """\
+rule solvency(method f) filtered { f -> f.selector != sig:deposit(uint256).selector } {
+    assert true;
+}
+"""
+
+_PROVER = "verify_spec"
+_RESULT = "result"
+
+_result_tool = result_tool_generator(
+    "result",
+    (str, "Commentary"),
+    "Signal completion",
+    validator=(StateWithSkips, lambda st, *_: check_completion(st)),
+)
+
+
+def _verify() -> ToolCallDict:
+    return tool_call_raw(_PROVER, rules=None)
+
+
+def _result(commentary: str) -> ToolCallDict:
+    return tool_call_raw(_RESULT, value=commentary)
+
+
+def _vacuous_report(*, rule_status: dict[str, bool], vacuous: dict[str, VacuityEvidence] | None = None,
+                    instantiated: set[str] | None = None) -> ProverReport:
+    return ProverReport(
+        rule_status=rule_status,
+        result_str="Prover report output",
+        link="local://test-run",
+        vacuous_methods=vacuous or {},
+        instantiated_methods=instantiated or set(),
+    )
+
+
+_DEPOSIT_EVIDENCE = {
+    DEPOSIT: VacuityEvidence(
+        method=DEPOSIT, affected_rules=["solvency"], diagnosis="sanity-failed in 1 of 1 rule(s)",
+    )
+}
+
+
+_ACK = "acknowledge_vacuous_method"
+
+
+def _acknowledge(
+    method: str = DEPOSIT,
+    steps: list[str] | None = None,
+    justification: str = "summary fix rejected by typechecker; mock failed to compile",
+) -> ToolCallDict:
+    return tool_call_raw(
+        _ACK,
+        method=method,
+        steps_attempted=steps if steps is not None else ["summary_fix", "mock"],
+        justification=justification,
+    )
+
+
+def _guard_scenario(certora_prover: ProverMock, *responses: ProverToolResponse):
+    prover_tool = certora_prover(responses)
+    return Scenario(
+        StateWithSkips,
+        prover_tool,
+        ExpectRuleFailure.as_tool("expect_rule_failure"),
+        AcknowledgeVacuousMethod.as_tool(_ACK),
+        _result_tool,
+    ).init(
+        curr_spec=_SPEC,
+        skipped=[],
+        property_rules=[],
+        validations={},
+        required_validations=[VALIDATION_KEY],
+        rule_skips={},
+        vacuous_methods={},
+        acknowledged_vacuous={},
+        config={"files": ["src/Foo.sol"]},
+    )
+
+
+def _result_accepted(st: StateWithSkips) -> bool:
+    return "result" in st
+
+
+class TestAcknowledgeVacuousMethod:
+    """The ledger tool's own validation, exercised against pre-seeded state."""
+
+    def _scenario(self, vacuous: dict[str, str] | None = None):
+        return Scenario(StateWithSkips, AcknowledgeVacuousMethod.as_tool(_ACK)).init(
+            curr_spec=_SPEC,
+            skipped=[],
+            property_rules=[],
+            validations={},
+            required_validations=[VALIDATION_KEY],
+            rule_skips={},
+            vacuous_methods=vacuous if vacuous is not None else {DEPOSIT: "diagnosis"},
+            acknowledged_vacuous={},
+            config={},
+        )
+
+    @pytest.mark.asyncio
+    async def test_acknowledgment_recorded_as_structured_ledger_entry(self):
+        acks = await self._scenario().turn(_acknowledge()).map_run(
+            lambda st: st["acknowledged_vacuous"]
+        )
+        record = json.loads(acks[DEPOSIT])
+        assert record["steps_attempted"] == ["mock", "summary_fix"]
+        assert "typechecker" in record["justification"]
+
+    @pytest.mark.asyncio
+    async def test_unknown_method_rejected(self):
+        scenario = self._scenario().turn(_acknowledge(method=WITHDRAW))
+        msg = await scenario.run_last_single_tool(_ACK)
+        assert "not currently flagged" in msg
+        assert DEPOSIT in msg  # the response lists what IS flagged
+
+    @pytest.mark.asyncio
+    async def test_empty_steps_rejected(self):
+        acks = await self._scenario().turn(_acknowledge(steps=[])).map_run(
+            lambda st: st["acknowledged_vacuous"]
+        )
+        assert acks == {}
+
+    @pytest.mark.asyncio
+    async def test_blank_justification_rejected(self):
+        acks = await self._scenario().turn(_acknowledge(justification="  ")).map_run(
+            lambda st: st["acknowledged_vacuous"]
+        )
+        assert acks == {}
+
+
+class TestVerifySpecVacuityGuard:
+    """Run 1 detects the vacuous method; run 2 passes because the spec hides it
+    (filter / skip / rule removal — the gate cannot tell and must not care).
+    The stamp must be withheld until the method is acknowledged or shown healthy."""
+
+    @pytest.mark.asyncio
+    async def test_unacknowledged_hidden_method_withholds_stamp(self, certora_prover: ProverMock):
+        scenario = _guard_scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            _verify(),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert not accepted
+
+    @pytest.mark.asyncio
+    async def test_guard_message_names_method_ladder_and_tool(self, certora_prover: ProverMock):
+        scenario = _guard_scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}),
+        )
+        msg = await scenario.turn(_verify()).turn(_verify()).run_last_single_tool(_PROVER)
+        assert "vacuity_guard" in msg
+        assert "WITHHELD" in msg
+        assert DEPOSIT in msg
+        assert "acknowledge_vacuous_method" in msg
+        assert "write_mock" in msg  # the repair ladder is restated
+
+    @pytest.mark.asyncio
+    async def test_acknowledged_method_grants_stamp(self, certora_prover: ProverMock):
+        """The structured escape hatch: a ledger entry written by the tool."""
+        scenario = _guard_scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            _acknowledge(),
+            _verify(),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert accepted
+
+    @pytest.mark.asyncio
+    async def test_rule_skip_bypass_still_blocked(self, certora_prover: ProverMock):
+        """The expect_rule_failure bypass: the sanity-failing rule drops out of
+        the all-verified check, but the persisted verdict still withholds the
+        stamp — no matter how persuasive the free-text skip reason sounds
+        (the old lexical hatch is gone; only the ledger clears the gate)."""
+        scenario = _guard_scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            tool_call_raw(
+                "expect_rule_failure", rule_name="solvency",
+                reason="attempted summary fix, mock, and optimistic_fallback; all failed",
+            ),
+            _verify(),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert not accepted
+
+    @pytest.mark.asyncio
+    async def test_acknowledged_rule_skip_grants_stamp(self, certora_prover: ProverMock):
+        """Skipping the sanity-failing rules is fine once the method itself is
+        acknowledged in the ledger."""
+        scenario = _guard_scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            tool_call_raw("expect_rule_failure", rule_name="solvency", reason="vacuous, acknowledged"),
+            _acknowledge(),
+            _verify(),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert accepted
+
+    @pytest.mark.asyncio
+    async def test_healthy_reinstantiation_clears_verdict(self, certora_prover: ProverMock):
+        """Run 2 instantiates the method without a sanity failure (the setup was
+        repaired) — the vacuity verdict clears and nothing blocks the stamp."""
+        scenario = _guard_scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}, instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            _verify(),
+            _verify(),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert accepted
+
+    @pytest.mark.asyncio
+    async def test_healthy_reinstantiation_clears_acknowledgment(self, certora_prover: ProverMock):
+        """When the verdict clears, its ledger entry clears with it: a method
+        that turns vacuous AGAIN later needs a fresh acknowledgment, so a stale
+        acknowledgment can never pre-clear a future verdict."""
+        scenario = _guard_scenario(
+            certora_prover,
+            # Run 1: vacuous. Acknowledged. Run 2: healthy (verdict + ack clear).
+            # Run 3: vacuous again. Run 4: hidden again -> guard must re-fire.
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}, instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE,
+                            instantiated={DEPOSIT}),
+            _vacuous_report(rule_status={"solvency": True}),
+        )
+        final = await scenario.turns(
+            _verify(),
+            _acknowledge(),
+            _verify(),
+            _verify(),
+            _verify(),
+        ).map_run(lambda st: (st["acknowledged_vacuous"], Scenario.last_single_tool(_PROVER, st)))
+        acks, last_prover_msg = final
+        assert acks == {}  # cleared by the healthy run, not re-established
+        assert "vacuity_guard" in last_prover_msg
+        assert "WITHHELD" in last_prover_msg
+
+
+# =========================================================================
+# Digest coverage of the agent-mutable setup
+# =========================================================================
+
+
+def _digest_state(**overrides) -> StateWithSkips:
+    base: dict = dict(
+        curr_spec="rule r { assert true; }",
+        skipped=[],
+        property_rules=[],
+        validations={},
+        required_validations=[VALIDATION_KEY],
+        rule_skips={},
+        vacuous_methods={},
+        acknowledged_vacuous={},
+        mocks={},
+        config={"files": ["src/Foo.sol"]},
+    )
+    base.update(overrides)
+    return base  # type: ignore[return-value]
+
+
+class TestStateDigest:
+    """The validation stamps must cover everything the agent can mutate after
+    stamping: the prover config, the mocks, and the acknowledgment ledger."""
+
+    def test_config_change_changes_digest(self):
+        assert state_digest(_digest_state()) != state_digest(
+            _digest_state(config={"files": ["src/Foo.sol"], "optimistic_fallback": True})
+        )
+
+    def test_mock_change_changes_digest(self):
+        assert state_digest(_digest_state()) != state_digest(
+            _digest_state(mocks={"certora/mocks/x/M.sol": "contract M {}"})
+        )
+
+    def test_acknowledgment_changes_digest(self):
+        assert state_digest(_digest_state()) != state_digest(
+            _digest_state(acknowledged_vacuous={DEPOSIT: "{}"})
+        )
+
+    def test_vacuous_verdicts_do_not_change_digest(self):
+        """Verdicts are prover observations, not agent edits: the stamp is
+        granted in the same Command that records them, so including them would
+        make every stamp instantly stale."""
+        assert state_digest(_digest_state()) == state_digest(
+            _digest_state(vacuous_methods={DEPOSIT: "diagnosis"})
+        )
+
+    def test_absent_and_empty_extras_hash_identically(self):
+        """Back-compat: flows without the source-mode state keys (natreq) and
+        checkpoints predating them must produce the pre-field digest."""
+        bare = {
+            "curr_spec": "rule r { assert true; }",
+            "skipped": [],
+            "property_rules": [],
+            "validations": {},
+            "required_validations": [],
+        }
+        assert state_digest(bare) == state_digest(  # type: ignore[arg-type]
+            _digest_state(config={}, mocks={}, acknowledged_vacuous={})
+        )
+
+
+class TestStampStalenessAfterSetupEdit:
+    """End-to-end: a PROVER stamp obtained before an edit_config / write_mock
+    call must not survive it — the persisted conf/mocks were never verified."""
+
+    def _scenario(self, certora_prover: ProverMock, *responses: ProverToolResponse):
+        prover_tool = certora_prover(responses)
+        return Scenario(
+            StateWithSkips,
+            prover_tool,
+            ConfigEditTool.as_tool("edit_config"),
+            WriteMockTool.bind("autospec_test").as_tool("write_mock"),
+            _result_tool,
+        ).init(
+            curr_spec=_SPEC,
+            skipped=[],
+            property_rules=[],
+            validations={},
+            required_validations=[VALIDATION_KEY],
+            rule_skips={},
+            vacuous_methods={},
+            acknowledged_vacuous={},
+            mocks={},
+            config={"files": ["src/Foo.sol"]},
+        )
+
+    @pytest.mark.asyncio
+    async def test_stamp_survives_without_edits(self, certora_prover: ProverMock):
+        scenario = self._scenario(
+            certora_prover, _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(_verify(), _result("done")).map_run(_result_accepted)
+        assert accepted
+
+    @pytest.mark.asyncio
+    async def test_config_edit_invalidates_stamp(self, certora_prover: ProverMock):
+        scenario = self._scenario(
+            certora_prover, _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            tool_call_raw("edit_config", edits=[
+                {"type": "set_flag", "flag": "optimistic_fallback", "value": True},
+            ]),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert not accepted
+
+    @pytest.mark.asyncio
+    async def test_mock_write_invalidates_stamp(self, certora_prover: ProverMock):
+        scenario = self._scenario(
+            certora_prover, _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            tool_call_raw("write_mock", file_name="M.sol", content="contract M {}"),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert not accepted
+
+    @pytest.mark.asyncio
+    async def test_reverify_after_edit_restores_stamp(self, certora_prover: ProverMock):
+        scenario = self._scenario(
+            certora_prover,
+            _vacuous_report(rule_status={"solvency": True}),
+            _vacuous_report(rule_status={"solvency": True}),
+        )
+        accepted = await scenario.turns(
+            _verify(),
+            tool_call_raw("edit_config", edits=[
+                {"type": "set_flag", "flag": "optimistic_fallback", "value": True},
+            ]),
+            _verify(),
+            _result("done"),
+        ).map_run(_result_accepted)
+        assert accepted
+
+
+# =========================================================================
+# Judge evidence thunk
+# =========================================================================
+
+
+class TestVacuityJudgeEvidence:
+    def test_empty_state_contributes_nothing(self):
+        assert vacuity_judge_evidence({}) == []
+        assert vacuity_judge_evidence(
+            {"vacuous_methods": {}, "rule_skips": {}, "acknowledged_vacuous": {}}
+        ) == []
+
+    def test_all_three_sections_rendered(self):
+        record = json.dumps({
+            "steps_attempted": ["mock", "summary_fix"],
+            "justification": "mock failed to compile; summary fix rejected",
+        })
+        parts = vacuity_judge_evidence({
+            "vacuous_methods": {DEPOSIT: "sanity-failed in 2 of 2 rule(s)"},
+            "rule_skips": {"solvency": "expected CEX per threat model"},
+            "acknowledged_vacuous": {DEPOSIT: record},
+        })
+        assert len(parts) == 3
+        vacuous_part, skips_part, acks_part = (str(x) for x in parts)
+        assert "VACUOUS" in vacuous_part and DEPOSIT in vacuous_part
+        assert "solvency" in skips_part and "expected CEX" in skips_part
+        assert "acknowledge_vacuous_method" in acks_part
+        assert "mock, summary_fix" in acks_part
+        assert "failed to compile" in acks_part
+
+    def test_malformed_ack_record_falls_back_to_raw(self):
+        parts = vacuity_judge_evidence({"acknowledged_vacuous": {DEPOSIT: "not json"}})
+        assert len(parts) == 1
+        assert "not json" in str(parts[0])
diff --git a/tests/test_write_mock.py b/tests/test_write_mock.py
new file mode 100644
index 00000000..0411f4b0
--- /dev/null
+++ b/tests/test_write_mock.py
@@ -0,0 +1,162 @@
+"""
+Tests for the write_mock tool and the state-held mock lifecycle: mocks are
+recorded in graph state under a per-generation namespace (never written to the
+shared project tree during generation), materialized on disk only for the
+duration of a prover run, and persisted by the artifact store for completed
+generations so cache replay works from a fresh checkout.
+"""
+import pytest
+
+from langgraph.graph import MessagesState
+
+from composer.prover.core import ProverOptions, ProverReport
+from composer.spec.cvl_generation import GeneratedCVL
+from composer.spec.source.artifacts import ComponentSpec, ProverArtifactStore
+from composer.spec.source.author import WriteMockTool
+from composer.spec.source.prover import ProverStateExtra, get_prover_tool
+
+from graphcore.testing import Scenario, ToolCallDict, tool_call_raw
+
+pytestmark = pytest.mark.asyncio
+
+
+_CONTENT = "// SPDX-License-Identifier: MIT\ncontract MockOracle { function price() external pure returns (uint256) { return 1; } }\n"
+_NAMESPACE = "autospec_oracle"
+_MOCK_PATH = f"certora/mocks/{_NAMESPACE}/MockOracle.sol"
+
+
+class MockTestState(MessagesState, ProverStateExtra):
+    pass
+
+
+_WRITE = "write_mock"
+
+
+def _scenario():
+    return Scenario(MockTestState, WriteMockTool.bind(_NAMESPACE).as_tool(_WRITE)).init(
+        config={}, rule_skips={}, mocks={},
+    )
+
+
+def _write(file_name: str, content: str = _CONTENT) -> ToolCallDict:
+    return tool_call_raw(_WRITE, file_name=file_name, content=content)
+
+
+# =========================================================================
+# State updates (no disk writes during generation)
+# =========================================================================
+
+
+async def test_records_mock_in_state_under_namespace(tmp_path, monkeypatch):
+    monkeypatch.chdir(tmp_path)  # would expose any accidental relative-path disk write
+    mocks = await _scenario().turn(_write("MockOracle.sol")).map_run(lambda st: st["mocks"])
+    assert mocks == {_MOCK_PATH: _CONTENT}
+    # Nothing lands on the shared tree at write time.
+    assert not (tmp_path / "certora").exists()
+
+
+async def test_response_names_path_and_edit_config():
+    msg = await _scenario().turn(_write("MockOracle.sol")).run_last_single_tool(_WRITE)
+    assert _MOCK_PATH in msg
+    assert "edit_config" in msg
+
+
+async def test_overwrite_replaces_state_entry():
+    mocks = await _scenario().turns(
+        _write("M.sol", "// v1"),
+        _write("M.sol", "// v2"),
+    ).map_run(lambda st: st["mocks"])
+    assert mocks == {f"certora/mocks/{_NAMESPACE}/M.sol": "// v2"}
+
+
+async def test_rejects_directories_and_traversal():
+    for bad in ("sub/Evil.sol", "../Evil.sol", "..", "/Evil.sol", "certora/mocks/Evil.sol"):
+        mocks = await _scenario().turn(_write(bad)).map_run(lambda st: st["mocks"])
+        assert mocks == {}
+
+
+async def test_rejects_non_solidity():
+    mocks = await _scenario().turn(_write("notes.txt", "hi")).map_run(lambda st: st["mocks"])
+    assert mocks == {}
+
+
+# =========================================================================
+# Materialization around prover runs
+# =========================================================================
+
+
+async def test_mocks_materialized_only_during_prover_run(tmp_path, monkeypatch, fake_llm):
+    """The state-held mock must exist on disk while run_prover executes (the
+    prover compiles from the real tree) and be gone afterwards (a gave-up
+    generation must not leave stray sources)."""
+    target = tmp_path / _MOCK_PATH
+    seen: list[bool] = []
+
+    async def observing_prover(*args, **kwargs):
+        seen.append(target.read_text() == _CONTENT if target.exists() else False)
+        return ProverReport(rule_status={"r": True}, result_str="ok", link="local://x")
+
+    monkeypatch.setattr("composer.spec.source.prover.run_prover", observing_prover)
+    monkeypatch.setattr(
+        "composer.spec.source.prover.get_stream_writer", lambda: (lambda _: None)
+    )
+    prover_tool = get_prover_tool(
+        prover_opts=ProverOptions(), llm=fake_llm,
+        main_contract="Dummy", project_root=str(tmp_path),
+    )
+    from composer.spec.source.prover import StateWithSkips
+    await Scenario(StateWithSkips, prover_tool).init(
+        curr_spec="rule r { assert true; }",
+        skipped=[], property_rules=[], validations={}, required_validations=[],
+        rule_skips={}, vacuous_methods={}, acknowledged_vacuous={},
+        mocks={_MOCK_PATH: _CONTENT},
+        config={"files": ["src/Foo.sol", _MOCK_PATH]},
+    ).turn(tool_call_raw("verify_spec", rules=None)).map_run(lambda st: st)
+    assert seen == [True]
+    assert not target.exists()
+    # The namespace dirs created for the run are cleaned up too.
+    assert not (tmp_path / "certora" / "mocks").exists()
+
+
+async def test_materialization_preserves_other_generations_dirs(tmp_path):
+    """Cleanup only removes the dirs this generation emptied: a concurrent
+    generation's still-materialized mocks (and the shared mocks root holding
+    them) must survive."""
+    from composer.spec.source.prover import materialized_mocks
+
+    other = tmp_path / "certora" / "mocks" / "other_ns" / "Keep.sol"
+    other.parent.mkdir(parents=True)
+    other.write_text("// keep")
+    with materialized_mocks(str(tmp_path), {_MOCK_PATH: _CONTENT}):
+        assert (tmp_path / _MOCK_PATH).read_text() == _CONTENT
+    assert not (tmp_path / "certora" / "mocks" / _NAMESPACE).exists()
+    assert other.read_text() == "// keep"
+
+
+# =========================================================================
+# Artifact-store persistence (cache replay from a fresh checkout)
+# =========================================================================
+
+
+def _generated(mocks: dict[str, str]) -> GeneratedCVL:
+    return GeneratedCVL(
+        commentary="c", cvl="rule r { assert true; }",
+        config={"files": ["src/Foo.sol", *mocks]},
+        mocks=mocks,
+    )
+
+
+async def test_artifact_store_persists_mocks(tmp_path):
+    store = ProverArtifactStore(str(tmp_path), "Dummy")
+    store.write_generated_spec(ComponentSpec("oracle"), _generated({_MOCK_PATH: _CONTENT}))
+    assert (tmp_path / _MOCK_PATH).read_text() == _CONTENT
+    # The conf referencing the mock is written alongside it.
+    conf = (tmp_path / "certora" / "confs" / "autospec_oracle.conf").read_text()
+    assert _MOCK_PATH in conf
+
+
+async def test_artifact_store_rejects_out_of_tree_mock_paths(tmp_path):
+    store = ProverArtifactStore(str(tmp_path), "Dummy")
+    for bad in ("src/Evil.sol", "certora/mocks/../../Evil.sol", "/abs/Evil.sol"):
+        with pytest.raises(AssertionError):
+            store.write_generated_spec(ComponentSpec("oracle"), _generated({bad: "x"}))