From 22bf34ea9aaadee0f86b8710bc90a3959b69e0ab Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Fri, 3 Jul 2026 21:13:51 +0300
Subject: [PATCH 01/13] Add main-contract augmentation harness models,
 generation, and autosetup verify-target

New MainHarnessPlan (unstructured-slot getters + helper decompositions) on the
state-analysis result, generate_main_harness() (VFS-confined to
certora/harnesses, validated <Main>Harness identifier), and
SystemDescriptionHarnessed.main_harness with verify_contract_name/path
accessors. run_and_apply_part1 writes the harness to disk and
run_autosetup_phase targets it when present. All new model fields are
optional-with-default so cached pre-change JSON still validates.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/harness.py               | 285 +++++++++++++++++-
 .../main_harness_generation_prompt.j2         |  64 ++++
 composer/templates/state_analysis.j2          |  29 +-
 3 files changed, 368 insertions(+), 10 deletions(-)
 create mode 100644 composer/templates/main_harness_generation_prompt.j2

diff --git a/composer/spec/source/harness.py b/composer/spec/source/harness.py
index c98ac4e..efe7d76 100644
--- a/composer/spec/source/harness.py
+++ b/composer/spec/source/harness.py
@@ -81,6 +81,65 @@ class HarnessedContract(ClosureContractBase):
     harness_definition : HarnessDef | None
     path: str
 
+class UnstructuredSlotSpec(BaseModel):
+    """
+    A piece of main-contract state living in "unstructured" storage (assembly
+    sload/sstore, `StorageSlot`, ERC-7201 namespaces, constant keccak slots)
+    with no public getter, to be exposed via a harness getter.
+    """
+    getter_name: str = Field(description="The name of the external view getter the harness should expose for this slot")
+    slot_derivation: str = Field(description=(
+        "How the storage slot is derived: the keccak preimage or namespace string "
+        "(e.g. `keccak256(\"river.state.balance\") - 1` or the ERC-7201 namespace id)"
+    ))
+    value_type: str = Field(description="The Solidity type of the value read from the slot (e.g. `uint256`, `address`)")
+    rationale: str = Field(description="One line: why verification needs to observe this state")
+
+class HelperDecomposition(BaseModel):
+    """
+    A monolithic external function to be decomposed into thin external wrappers
+    around the existing internal helpers it calls.
+    """
+    target_function: str = Field(description="The signature/name of the monolithic external function being decomposed")
+    helpers: dict[str, str] = Field(description=(
+        "The thin external wrappers to expose: a map from wrapper name to a one-line "
+        "behavioral contract of the internal step it wraps"
+    ))
+    rationale: str = Field(description="One line: why verification needs the decomposed entry points")
+
+class MainHarnessPlan(BaseModel):
+    """
+    The plan for the main-contract augmentation harness: getters for unstructured
+    storage plus helper decompositions of monolithic functions. Purely additive —
+    the harness never changes or duplicates protocol behavior.
+    """
+    unstructured_slots: list[UnstructuredSlotSpec] = Field(description="The unstructured-storage getters to expose (may be empty)")
+    decompositions: list[HelperDecomposition] = Field(description="The monolithic-function decompositions to expose (may be empty)")
+
+    def api_lines(self) -> list[str]:
+        """Prompt-facing one-liners describing the harness API, for downstream
+        property-generation/judge prompts."""
+        lines: list[str] = []
+        for s in self.unstructured_slots:
+            lines.append(
+                f"`{s.getter_name}()` returns (`{s.value_type}`) — reads the storage slot "
+                f"derived from {s.slot_derivation}. {s.rationale}"
+            )
+        for d in self.decompositions:
+            for (name, contract) in d.helpers.items():
+                lines.append(
+                    f"`{name}` — {contract} (thin external wrapper over a step of `{d.target_function}`)"
+                )
+        return lines
+
+class MainHarnessView(BaseModel):
+    """Prompt-facing view of the main-contract augmentation harness, rendered by
+    `harnessed_application_context.j2` so downstream agents see the harness API."""
+    name: SolidityIdentifier
+    path: str
+    harness_of: SolidityIdentifier
+    api: list[str]
+
 class ExternalInterface(BaseModel):
     """
     An external actor interacted through an interface which is NOT included in the transitive closure
@@ -103,12 +162,20 @@ class AgentSystemDescription(SystemDescriptionBase[ClosureContract]):
     """
     The result of your analysis
     """
+    # Optional-with-default so cached pre-change analyses still validate.
+    main_contract_harness: MainHarnessPlan | None = Field(default=None, description=(
+        "The main-contract augmentation harness plan, if the main contract has "
+        "unstructured storage without getters and/or monolithic external functions "
+        "worth decomposing (null otherwise)"
+    ))
 
     def needs_harnessing(self) -> bool:
+        # Only gates the *external* N-instance harnessing; the main-contract
+        # augmentation harness is generated separately (see generate_main_harness).
         return any([
             c.num_instances for c in self.transitive_closure
         ])
-    
+
 class LocatedClosureContract(ClosureContract):
     path: str
 
@@ -116,7 +183,41 @@ class LocatedSystemDescription(SystemDescriptionBase[LocatedClosureContract]):
     pass
 
 class SystemDescriptionHarnessed(SystemDescriptionBase[HarnessedContract]):
-    pass
+    # Both optional-with-default so cached pre-change descriptions still validate.
+    # ``main_harness`` is the generated augmentation harness (the verify target when
+    # present); ``main_harness_plan`` is the analysis plan it was generated from,
+    # kept so downstream prompts can describe the harness API.
+    main_harness: HarnessedContract | None = None
+    main_harness_plan: MainHarnessPlan | None = None
+
+    def verify_contract_name(self, default_name: str) -> str:
+        """The contract identifier the prover verifies: the main-harness identifier
+        when an augmentation harness exists, ``default_name`` otherwise."""
+        if self.main_harness is not None:
+            return self.main_harness.solidity_identifier
+        return default_name
+
+    def verify_contract_path(self, default_path: str) -> str:
+        """The source file the prover verifies, following ``verify_contract_name``."""
+        if self.main_harness is not None:
+            return self.main_harness.path
+        return default_path
+
+    def main_harness_api(self) -> list[str] | None:
+        """Prompt-facing one-liners for the harness API (None when no harness)."""
+        if self.main_harness is None or self.main_harness_plan is None:
+            return None
+        return self.main_harness_plan.api_lines()
+
+    def main_harness_view(self) -> MainHarnessView | None:
+        if self.main_harness is None or self.main_harness.harness_definition is None:
+            return None
+        return MainHarnessView(
+            name=self.main_harness.solidity_identifier,
+            path=self.main_harness.path,
+            harness_of=self.main_harness.harness_definition.harness_of,
+            api=self.main_harness_api() or [],
+        )
 
 class HarnessAnalysisParams(TypedDict):
     contract_name: str
@@ -170,6 +271,10 @@ def result_validator(
         for c in res.transitive_closure:
             if c.solidity_identifier not in contract_lkp:
                 return f"Contract {c.solidity_identifier} in the interaction closure doesn't appear in the application description"
+        if res.main_contract_harness is not None and \
+                not res.main_contract_harness.unstructured_slots and \
+                not res.main_contract_harness.decompositions:
+            return "main_contract_harness was proposed but contains no getters and no decompositions; deliver null instead"
         return None
 
     d = bind_standard(
@@ -370,6 +475,127 @@ def result_validator(
     await child.cache_put(to_ret)
     return to_ret
 
+class MainHarnessAgentResult(BaseModel):
+    """
+    The result of your main-contract harness generation
+    """
+    path: str = Field(description="The relative path to the generated harness file")
+    harness_name: SolidityIdentifier = Field(description="The Solidity identifier of the harness contract defined in the file")
+
+class MainHarnessResult(MainHarnessAgentResult):
+    source: str
+
+class MainHarnessGenParams(TypedDict):
+    contract_name: str
+    relative_path: str
+    harness_name: str
+    plan: MainHarnessPlan
+
+_MainHarnessGenerationPrompt = TypedTemplate[MainHarnessGenParams]("main_harness_generation_prompt.j2")
+
+def main_harness_generation_key(
+    plan: MainHarnessPlan,
+    contract_name: str,
+) -> CacheKey[SystemDescriptionHarnessed, MainHarnessResult]:
+    return CacheKey[SystemDescriptionHarnessed, MainHarnessResult](
+        "main-harness-" + string_hash(plan.model_dump_json() + "\x00" + contract_name)
+    )
+
+async def generate_main_harness(
+    context: WorkflowContext[SystemDescriptionHarnessed],
+    env: ServiceHost,
+    source: SourceCode,
+    application: SourceApplication,
+    plan: MainHarnessPlan
+) -> MainHarnessResult:
+    """Generate the main-contract augmentation harness `<Main>Harness is <Main>`:
+    external view getters for unstructured storage plus thin external wrappers
+    decomposing monolithic functions. Same VFS confinement as
+    ``generate_harnesses`` (writes only under ``certora/harnesses``)."""
+    child = await context.child(
+        main_harness_generation_key(plan, source.contract_name), plan.model_dump()
+    )
+    if (cached := await child.cache_get(MainHarnessResult)) is not None:
+        return cached
+
+    tool_conf = VFSToolConfig(
+        fs_layer=source.project_root,
+        immutable=False,
+        put_doc_extra="You may only write into the `certora/harnesses` directory",
+        forbidden_write="^(?!certora/harnesses)",
+        forbidden_read=source.forbidden_read
+    )
+
+    class GenerationState(MessagesState, VFSState):
+        result: NotRequired[MainHarnessAgentResult]
+
+    class GenerationInput(FlowInput, VFSState):
+        pass
+
+    v_tools, mat = vfs_tools(tool_conf, GenerationState)
+
+    expected_name = f"{source.contract_name}Harness"
+
+    bound_template = _MainHarnessGenerationPrompt.bind({
+        "contract_name": source.contract_name,
+        "relative_path": source.relative_path,
+        "harness_name": expected_name,
+        "plan": plan
+    })
+
+    def result_validator(
+        s: GenerationState,
+        res: MainHarnessAgentResult,
+        tid: str
+    ) -> str | None:
+        if res.harness_name != expected_name:
+            return f"Harness contract must be named {expected_name}, got {res.harness_name}"
+        if mat.get(s, res.path) is None:
+            return f"Delivered harness {res.harness_name} at {res.path}, but it doesn't exist on the VFS"
+        return None
+
+    result_tool = result_tool_generator(
+        "result",
+        MainHarnessAgentResult,
+        "Signal the completion of your workflow",
+        validator=(GenerationState, result_validator)
+    )
+
+    g = env.builder_lite().with_input(
+        GenerationInput
+    ).with_state(
+        GenerationState
+    ).with_output_key(
+        "result"
+    ).inject(
+        lambda g: bound_template.render_to(g.with_initial_prompt_template)
+    ).with_sys_prompt_template(
+        "harness_generation_system_prompt.j2"
+    ).with_tools(
+        v_tools + [result_tool]
+    ).with_default_summarizer().compile_async()
+
+    res_state = await run_to_completion(
+        graph=g,
+        input=GenerationInput(input=[], vfs={}),
+        context=None,
+        description="Main Harness Generation",
+        recursion_limit=child.recursion_limit,
+        thread_id=child.thread_id
+    )
+
+    assert "result" in res_state
+    gen = res_state["result"]
+    source_code = mat.get(res_state, gen.path)
+    assert source_code is not None, gen.path
+    to_ret = MainHarnessResult(
+        path=gen.path,
+        harness_name=gen.harness_name,
+        source=source_code.decode("utf-8")
+    )
+    await child.cache_put(to_ret)
+    return to_ret
+
 def _multi_replace(
     s: list[SolidityIdentifier],
     patch: dict[SolidityIdentifier, list[SolidityIdentifier]]
@@ -494,6 +720,33 @@ async def run_setup_part1(
                 ) for c in located_desc.transitive_closure
             ]
         )
+
+    if analysis_results.main_contract_harness is not None:
+        main_harness = await generate_main_harness(
+            context=setup_ctx,
+            env=env,
+            source=source,
+            application=application_desc,
+            plan=analysis_results.main_contract_harness
+        )
+        # The harness extends the main contract, so it carries the main contract's
+        # (already harness-patched) link fields.
+        main_links = next(
+            (c.link_fields for c in harnessed_system.transitive_closure
+             if c.solidity_identifier == source.contract_name),
+            []
+        )
+        harnessed_system.main_harness = HarnessedContract(
+            solidity_identifier=main_harness.harness_name,
+            link_fields=main_links,
+            harness_definition=HarnessDef(
+                harness_of=source.contract_name,
+                harness_source=main_harness.source,
+            ),
+            path=main_harness.path
+        )
+        harnessed_system.main_harness_plan = analysis_results.main_contract_harness
+
     await setup_ctx.cache_put(harnessed_system)
     return harnessed_system
 
@@ -504,7 +757,10 @@ async def run_and_apply_part1(
     application_desc: SourceApplication
 ) -> SystemDescriptionHarnessed:
     res = await run_setup_part1(context, source, env, application_desc)
-    for c in res.transitive_closure:
+    to_write = list(res.transitive_closure)
+    if res.main_harness is not None:
+        to_write.append(res.main_harness)
+    for c in to_write:
         if c.harness_definition is not None:
             tgt = Path(source.project_root) / c.path
             tgt.parent.mkdir(parents=True, exist_ok=True)
@@ -544,14 +800,19 @@ async def run_harness_creation(
 def autosetup_key(
     app: SourceApplication,
     prover_opts: ProverOptions,
+    verify_contract: str | None = None,
 ) -> CacheKey[ContractSetup, SetupSuccess]:
     """Cache key for the AutoSetup phase. Includes ``prover_opts`` so cloud and
     local configurations never collide (the old composite ``config_key`` omitted
     them, which could reuse a stale config across modes)."""
+    payload = app.model_dump_json() + "\x00" + "\x00".join(prover_opts.extra_args)
+    # The verified contract participates in the key only when it deviates from
+    # the default (a main-contract augmentation harness), so cache entries from
+    # before harness support stay valid for harness-free runs.
+    if verify_contract is not None:
+        payload += "\x00verify=" + verify_contract
     return CacheKey[ContractSetup, SetupSuccess](
-        "autosetup-" + string_hash(
-            app.model_dump_json() + "\x00" + "\x00".join(prover_opts.extra_args)
-        )
+        "autosetup-" + string_hash(payload)
     )
 
 
@@ -567,9 +828,15 @@ async def run_autosetup_phase(
     having run first: it reads the transitive-closure file paths from disk.
 
     Cache hits are guarded by the on-disk existence of ``summaries_path``."""
+    # When a main-contract augmentation harness exists, the harness *is* the
+    # verified contract: it becomes AutoSetup's target (the original main
+    # contract enters the scene through inheritance, not as its own instance).
+    verify_harness = (
+        sys_desc.main_harness.solidity_identifier if sys_desc.main_harness is not None else None
+    )
     config_ctxt = context.child(config_key)
     cache = await config_ctxt.child(
-        autosetup_key(application_desc, prover_opts),
+        autosetup_key(application_desc, prover_opts, verify_harness),
         application_desc.model_dump(),
     )
     if (cached := await cache.cache_get(SetupSuccess)) is not None:
@@ -582,8 +849,8 @@ async def run_autosetup_phase(
 
     setup_result = await run_autosetup(
         Path(source.project_root),
-        source.relative_path,
-        source.contract_name,
+        sys_desc.verify_contract_path(source.relative_path),
+        sys_desc.verify_contract_name(source.contract_name),
         prover_opts,
         *extra_files,
     )
diff --git a/composer/templates/main_harness_generation_prompt.j2 b/composer/templates/main_harness_generation_prompt.j2
new file mode 100644
index 0000000..d613a59
--- /dev/null
+++ b/composer/templates/main_harness_generation_prompt.j2
@@ -0,0 +1,64 @@
+<background>
+You are assisting in the setup of a formal verification project using the Certora Prover.
+</background>
+
+<task>
+The contract {{ contract_name }} (located at `{{ relative_path }}`) is being verified. A prior analysis
+determined that some of its state and/or entry points cannot be observed through its external interface,
+which prevents verification properties from being written about them.
+
+You must write a single "augmentation harness": a contract declared as
+`contract {{ harness_name }} is {{ contract_name }}` which exposes the required verification API
+*without* changing or duplicating any behavior of {{ contract_name }}.
+
+The harness must contain exactly the following, and nothing else:
+{% if plan.unstructured_slots %}
+
+## Storage getters
+
+For each entry below, add an `external view` getter that reads the *exact* storage slot used by the contract:
+{% for s in plan.unstructured_slots %}
+* `{{ s.getter_name }}` returning `{{ s.value_type }}` — slot derivation: {{ s.slot_derivation }}. Rationale: {{ s.rationale }}
+{% endfor %}
+
+Implementation constraints for getters:
+* Read the slot with inline assembly (an `sload` of a precomputed `constant` slot value), or, when the
+  contract accesses the slot through an internal storage-library getter, call that internal getter instead.
+* Precompute the slot constant *exactly* as the contract derives it (e.g. `keccak256("...") - 1`, the
+  ERC-7201 formula, etc.); consult the contract source and do NOT re-derive it differently.
+{% endif %}
+{% if plan.decompositions %}
+
+## Helper wrappers
+{% for d in plan.decompositions %}
+
+The function `{{ d.target_function }}` should be decomposed ({{ d.rationale }}) via the following thin external wrappers:
+{% for (name, contract) in d.helpers.items() %}
+* `{{ name }}`: {{ contract }}
+{% endfor %}
+{% endfor %}
+
+Implementation constraints for wrappers:
+* Each wrapper must be a *thin* `external` function that simply calls the corresponding existing
+  `internal`/`private` function of {{ contract_name }} (forwarding arguments and returning its result).
+{% endif %}
+
+Hard rules:
+* Do NOT duplicate any logic from {{ contract_name }}: getters only read state, wrappers only delegate to
+  existing internal functions.
+* Do NOT change any behavior of {{ contract_name }}: do not override any of its existing external/public functions.
+* Do NOT declare any state variables in the harness (no shadowing, no new state).
+* The harness must compile. Import {{ contract_name }} using the relative path of the target file, i.e.
+  `import "{{ relative_path }}";` — do NOT try to use imports with `..`. Add only the code necessary to satisfy
+  the Solidity compiler/typechecker (e.g., code to invoke the parent contract's constructor).
+
+Place the generated file at `certora/harnesses/{{ harness_name }}.sol` on the VFS using the `put_file` tool.
+The contract identifier MUST be exactly `{{ harness_name }}`.
+
+**Important**: Prior executions of this workflow may mean the harness already exists on the VFS. So long as
+the file exists with an implementation that satisfies the above instructions, you *may* deliver it unchanged.
+
+Once the harness has been generated, call the `result` tool with the relative path to the generated file and
+the contract identifier `{{ harness_name }}`. Your result will be validated; repair any issues and re-invoke
+the result tool upon rejection.
+</task>
diff --git a/composer/templates/state_analysis.j2 b/composer/templates/state_analysis.j2
index ca40a80..e2e7a64 100644
--- a/composer/templates/state_analysis.j2
+++ b/composer/templates/state_analysis.j2
@@ -177,10 +177,36 @@ Use your memory tool to record the results of this analysis at `/memories/extern
 
 ## Step 6
 
+Analyze the implementation of {{ contract_name }} itself (the *main* contract being verified) to determine
+whether it needs an "augmentation harness". Verification properties can only observe the contract through its
+external interface, so flag the following:
+
+a. State that is accessed via inline assembly `sload`/`sstore`, the `StorageSlot` library, ERC-7201
+   namespaced storage, or constant keccak-derived slots, and which has *no* public getter.
+   NB: CVL *CAN* compute keccak-derived storage slots (they are compile-time constants and `keccak256` is
+   built into CVL) and hook them directly; a harness getter is still preferred because it makes the
+   resulting rules dramatically more readable.
+b. Monolithic external functions that are long sequences of internal-helper calls. Decomposing such a
+   function into thin external wrappers around its existing internal helpers lets properties target each
+   step in isolation.
+
+If either applies, propose a "main contract harness plan" (the `main_contract_harness` field of your result):
+* For each flagged storage location: the desired getter name, the slot derivation (the keccak preimage or
+  namespace string), the Solidity type of the value read from the slot, and a one-line rationale.
+* For each monolithic function: the thin helper wrappers to expose (name plus a one-line behavioral contract
+  for each) and a rationale.
+
+If neither applies, leave `main_contract_harness` null. Do NOT propose getters for state that already has a
+public getter, and do NOT propose helpers that would duplicate logic rather than wrap existing internal functions.
+
+Use your memory tool to record the results of this analysis at `/memories/main_harness.md`
+
+## Step 7
+
 Output the results of your findings using the provided `result` tool, reading in information from your memory
 if needed.
 
-Your results consists of four parts:
+Your results consists of five parts:
 1. A natural language description of the non-trivial state of the {{ contract_name }}
 2. A list of "interface interactions", consisting of:
    a. The name of the external actor
@@ -190,6 +216,7 @@ Your results consists of four parts:
    b. A list of "link fields" used to connect this contract with others in this interaction closure
    c. the number of instances needed to model a non-trivial state if the contract is `MULTIPLE` or `DYNAMIC` (null if inapplicable)
 4. A list of contracts classified at ERC20
+5. The main contract harness plan from step 6 (null if no augmentation is needed)
 
 <state>
   You will execute this task across multiple iterations with the provided tools; you should take your time and work methodically.

From 7a94dac81a75a22a60cc6c972834959bb3510fd9 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Fri, 3 Jul 2026 21:35:35 +0300
Subject: [PATCH 02/13] WIP: thread verify-target and harness API through
 pipeline (interrupted)

Partial verify-target threading from an interrupted run; next commit
audits, completes, and tests this work.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/feedback.py                | 12 +++++++-
 composer/spec/source/artifacts.py        | 20 ++++++++++---
 composer/spec/source/author.py           | 38 +++++++++++++++++++++---
 composer/spec/source/common_pipeline.py  |  9 ++++--
 composer/spec/source/pipeline.py         | 20 +++++++++++--
 composer/spec/source/prover.py           |  2 ++
 composer/spec/source/report/collect.py   |  9 ++++--
 composer/spec/source/struct_invariant.py | 16 ++++++++--
 8 files changed, 108 insertions(+), 18 deletions(-)

diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py
index 5f64d7b..5bde355 100644
--- a/composer/spec/feedback.py
+++ b/composer/spec/feedback.py
@@ -41,11 +41,17 @@ class FeedbackInherentParams(TypedDict):
     #   ``existing``   — pre-existing codebase being verified as-is; target
     #                    has real immutable source.
     sort: Sort
+    # One-liners describing the main-contract augmentation harness API. Only the
+    # source-mode (autoprove) flow supplies this; the other flows have no harness.
+    harness_api: NotRequired[list[str] | None]
 
 FeedbackTemplate = TypedTemplate[FeedbackInherentParams]("property_judge_prompt.j2")
 
 class JudgeSystemParams(TypedDict):
     sort: Sort
+    # True when the run verifies through a main-contract augmentation harness;
+    # gates the harness-aware wording (the template defaults it to false).
+    harness_augmentation: NotRequired[bool]
 
 # Judge system prompt, shared between the natspec and source-mode flows. The fs
 # primitives are always documented; ``sort`` drives the rest (the template
@@ -61,10 +67,14 @@ def property_feedback_judge(
     *,
     extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None,
     system_prompt: TemplateInstantiation | None = None,
+    harness_augmentation: bool = False,
 ) -> FeedbackToolContext:
 
     if system_prompt is None:
-        system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort})
+        system_prompt = FeedbackSystemTemplate.bind({
+            "sort": env.sort,
+            "harness_augmentation": harness_augmentation,
+        })
 
     builder = env.builder_heavy().with_tools(
         env.all_tools
diff --git a/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py
index ae46480..74fa14d 100644
--- a/composer/spec/source/artifacts.py
+++ b/composer/spec/source/artifacts.py
@@ -69,9 +69,13 @@ class ProverArtifactStore(ArtifactStore):
     """Persists the autoprove pipeline's outputs under ``certora/`` (plus
     ``.certora_internal/autoProve/`` diagnostics)."""
 
-    def __init__(self, project_root: str, main_contract: str):
+    def __init__(self, project_root: str, main_contract: str, verify_contract: str | None = None):
         super().__init__(project_root)
         self._main_contract = main_contract
+        # The contract identifier the prover verifies: the main-harness identifier
+        # when the run verifies through an augmentation harness, otherwise the main
+        # contract itself.
+        self._verify_contract = verify_contract or main_contract
 
     def _deliverable_dir(self) -> Path:
         return under_project(self._project_root, CERTORA_DIR)
@@ -116,8 +120,8 @@ def _write_conf(
             return
         conf = prover_config_overlay(
             base_config,
-            main_contract=self._main_contract,
-            verify_target=f"{self._main_contract}:{spec_path}",
+            main_contract=self._verify_contract,
+            verify_target=f"{self._verify_contract}:{spec_path}",
         )
         confs_dir = ensure_dir(self._deliverable_dir() / "confs")
         (confs_dir / f"{spec.stem}.conf").write_text(json.dumps(conf, indent=2))
@@ -138,11 +142,19 @@ def write_report(self, report: AutoProverReport) -> None:
         _log.info("autoprove report: wrote %s", out)
 
 
+@dataclass
 class ProverSourceCode(SourceCode):
     """``SourceCode`` that exposes the prover artifact store. Construct this in the
     autoprove entry point; analysis / property-inference passes keep taking plain
     ``SourceCode`` since the store is irrelevant to them."""
 
+    # The contract identifier the prover verifies. Defaults to ``contract_name``;
+    # the staged pipeline overrides it (via ``dataclasses.replace``) when a
+    # main-contract augmentation harness is the verify target.
+    verify_contract: str | None = None
+
     @property
     def artifact_store(self) -> ProverArtifactStore:
-        return ProverArtifactStore(self.project_root, self.contract_name)
+        return ProverArtifactStore(
+            self.project_root, self.contract_name, verify_contract=self.verify_contract,
+        )
diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py
index a7e8df1..3a390a0 100644
--- a/composer/spec/source/author.py
+++ b/composer/spec/source/author.py
@@ -33,8 +33,12 @@
 
 from graphcore.graph import FlowInput
 
+type GiveUpSort = Literal["env_issue", "needs_harness", "prover_limit", "other"]
+
 class SourceAuthorExtra(TypedDict):
     failed: bool | None
+    # Classification recorded by the give_up tool; None until (unless) it is called.
+    give_up_sort: GiveUpSort | None
 
 class SourceCVLGenerationExtra(CVLGenerationExtra, ProverStateExtra, SourceAuthorExtra):
     pass
@@ -47,6 +51,8 @@ class SourceCVLGenerationState(SourceCVLGenerationExtra, MessagesState):
 
 class GaveUp(BaseModel):
     reason: str
+    # Default keeps pre-change cached results deserializing.
+    sort: GiveUpSort = "other"
 
 type BatchGeneratedCVLResult = GeneratedCVL | GaveUp
 
@@ -135,6 +141,16 @@ class GiveUpTool(WithImplementation[Command], WithInjectedId):
     mechanisms to complete your task.
     """
     reason: str = Field(description="The reason for giving up on your task")
+    sort: GiveUpSort = Field(
+        default="other",
+        description=(
+            "Classification of the give-up: `env_issue` when a toolchain/environment "
+            "component is missing or broken; `needs_harness` when the properties require "
+            "observing state or entry points that the contract's external interface (and "
+            "any verification harness) does not expose; `prover_limit` when prover "
+            "timeouts/resource limits defeat every reformulation; `other` for anything else."
+        ),
+    )
 
     @override
     def run(self) -> Command:
@@ -143,6 +159,7 @@ def run(self) -> Command:
             "Accepted",
             failed=True,
             result=self.reason,
+            give_up_sort=self.sort,
         )
 
 class ResourceView(TypedDict):
@@ -157,6 +174,9 @@ class PropertyGenParams(TypedDict):
     resources: list[ResourceView]
     properties: list[PropertyFormulation]
     contract_name: str
+    # One-liners describing the main-contract augmentation harness API
+    # (getters/helpers); None when the run has no main harness.
+    harness_api: list[str] | None
 
 class PropertyGenerationConfig(SummaryConfig[SourceCVLGenerationState]):
     def __init__(self):
@@ -343,10 +363,13 @@ async def batch_cvl_generation(
     description: str,
     source: SourceCode,
     spec_dir: Path,
+    harness_api: list[str] | None = None,
 ) -> 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*.
+    # *harness_api* is the main-contract augmentation harness API (if any); it is
+    # surfaced to both the author and the feedback judge.
     resource_views: list[ResourceView] = [
         {
             "description": r.description,
@@ -359,7 +382,8 @@ async def batch_cvl_generation(
         "resources": resource_views,
         "context": component,
         "properties": props,
-        "contract_name": source.contract_name
+        "contract_name": source.contract_name,
+        "harness_api": harness_api
     })
 
     # use "cache=long" to account for very long prover runs.
@@ -389,8 +413,10 @@ async def batch_cvl_generation(
     feedback_env = property_feedback_judge(
         ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({
             "sort": "existing",
-            "context": component
-        }), props
+            "context": component,
+            "harness_api": harness_api
+        }), props,
+        harness_augmentation=harness_api is not None,
     )
 
     res_state = await run_cvl_generator(
@@ -408,13 +434,17 @@ async def batch_cvl_generation(
             property_rules=[],
             validations={},
             failed=None,
+            give_up_sort=None,
         )
     )
 
     assert "result" in res_state
     assert res_state["failed"] is not None
     if res_state["failed"]:
-        return GaveUp(reason=res_state["result"])
+        return GaveUp(
+            reason=res_state["result"],
+            sort=res_state.get("give_up_sort") or "other",
+        )
     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
diff --git a/composer/spec/source/common_pipeline.py b/composer/spec/source/common_pipeline.py
index dac066d..07d2f95 100644
--- a/composer/spec/source/common_pipeline.py
+++ b/composer/spec/source/common_pipeline.py
@@ -147,13 +147,16 @@ async def generate_all_component_cvl(
     resources: list[CVLResource],
     semaphore: asyncio.Semaphore,
     invariant_result: tuple[list[PropertyFormulation], GeneratedCVL] | None = None,
+    harness_api: list[str] | None = None,
 ) -> AutoProveResult:
     """Phase 6 — per-component CVL generation.
 
     Generates and writes a spec for each extracted batch in parallel
     (semaphore-bounded). ``resources`` is consumed read-only; callers that want
     the structural invariants assumed as preconditions must include
-    ``invariants.spec`` in ``resources`` before calling.
+    ``invariants.spec`` in ``resources`` before calling. ``harness_api`` is the
+    main-contract augmentation harness API (if any), surfaced to the authors
+    and the feedback judge.
     """
     async def _generate_batch(
         task_id: str,
@@ -182,6 +185,7 @@ async def _generate_batch(
                 description=label,
                 source=source_input,
                 spec_dir=SPECS_DIR,
+                harness_api=harness_api,
             ),
             semaphore,
         )
@@ -234,6 +238,7 @@ async def _generate_and_write_batch(
                 props=batch.props,
                 result=result if isinstance(result, GeneratedCVL) else None,
                 run_link=component_runs.get(spec.run_key),
+                gave_up_sort=result.sort if isinstance(result, GaveUp) else None,
             ))
         if invariant_result is not None:
             inv_props, inv_cvl = invariant_result
@@ -270,7 +275,7 @@ async def _generate_and_write_batch(
         if isinstance(result, BaseException):
             failures.append(f"{batch.feat.component.name}: {result}")
         elif isinstance(result, GaveUp):
-            failures.append(f"{batch.feat.component.name}: GAVE_UP: {result.reason}")
+            failures.append(f"{batch.feat.component.name}: GAVE_UP[{result.sort}]: {result.reason}")
 
     return AutoProveResult(
         n_components=len(component_batches),
diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py
index 5799f16..20557c2 100644
--- a/composer/spec/source/pipeline.py
+++ b/composer/spec/source/pipeline.py
@@ -15,6 +15,7 @@
 """
 
 import asyncio
+from dataclasses import replace
 
 from composer.io.multi_job import (
     TaskInfo, HandlerFactory, run_task,
@@ -139,10 +140,20 @@ async def run_autoprove_pipeline(
         components=comp
     )
 
+    # The verified contract, computed ONCE here: the main-harness identifier when
+    # harness creation produced a main-contract augmentation harness, the main
+    # contract itself otherwise. Everything downstream that names a verify target
+    # (prover tool, artifact-store conf dumps) derives from this.
+    verify_contract = sys_desc.verify_contract_name(source_input.contract_name)
+    source_input = replace(source_input, verify_contract=verify_contract)
+    # The harness API one-liners (None when no main harness), surfaced to the
+    # property authors and the feedback judge.
+    harness_api = sys_desc.main_harness_api()
+
     # Prover tool is stateless with respect to setup, so build it now; it is
     # shared by every CVL-generation call below.
     prover_tool = get_prover_tool(
-        env.llm_heavy(), source_input.contract_name,
+        env.llm_heavy(), verify_contract,
         source_input.project_root, prover_opts=prover_opts,
     )
 
@@ -186,7 +197,10 @@ async def stream_invariants():
         return await run_task(
             handler_factory,
             TaskInfo(INVARIANTS_TASK_ID, "Structural Invariants", AutoProvePhase.INVARIANTS),
-            lambda: get_invariant_formulation(ctx, source_input, env, harnessed_app),
+            lambda: get_invariant_formulation(
+                ctx, source_input, env, harnessed_app,
+                main_harness=sys_desc.main_harness_view(),
+            ),
         )
 
     async def stream_bugs():
@@ -255,6 +269,7 @@ async def stream_bugs():
                     description="Structural invariant CVL",
                     source=source_input,
                     spec_dir=SPECS_DIR,
+                    harness_api=harness_api,
                 ),
             )
             if isinstance(inv_cvl_result, GaveUp):
@@ -293,4 +308,5 @@ async def stream_bugs():
         resources=resources,
         semaphore=semaphore,
         invariant_result=invariant_result,
+        harness_api=harness_api,
     )
diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py
index c88490a..9e39380 100644
--- a/composer/spec/source/prover.py
+++ b/composer/spec/source/prover.py
@@ -50,6 +50,8 @@ 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.
+    ``main_contract`` is the verified contract identifier — the augmentation-harness
+    identifier when the pipeline verifies through a main-contract harness.
     """
     return {
         **base_config,
diff --git a/composer/spec/source/report/collect.py b/composer/spec/source/report/collect.py
index b8bf253..7ac4361 100644
--- a/composer/spec/source/report/collect.py
+++ b/composer/spec/source/report/collect.py
@@ -39,12 +39,15 @@ class ReportComponentInput[R: ReportableResult]:
     of the file the units live in (``autospec_<slug>.spec`` / ``invariants.spec`` / a ``.t.sol``) —
     the unit-identity fallback when a verdict carries no source location. ``result`` is the in-memory
     generation outcome, or ``None`` when the component gave up / crashed (no units formalized).
-    ``run_link`` is this component's verification-run link, if any (prover URL / local dir)."""
+    ``run_link`` is this component's verification-run link, if any (prover URL / local dir).
+    ``gave_up_sort`` is the author's give-up classification when ``result`` is ``None`` because
+    the component gave up (``None`` for crashes / backends that don't classify give-ups)."""
     name: ComponentName
     unit_file: str
     props: list[PropertyFormulation]
     result: R | None
     run_link: str | None
+    gave_up_sort: str | None = None
 
 
 @dataclass(frozen=True)
@@ -111,7 +114,9 @@ async def collect[R: ReportableResult](
     for inp, verdicts in zip(inputs, verdict_maps):
         if inp.result is None:
             # Gave up or crashed: the whole component is a formalization gap.
-            gave_up.append(GaveUpComponent(component=inp.name, properties=inp.props))
+            gave_up.append(GaveUpComponent(
+                component=inp.name, properties=inp.props, give_up_sort=inp.gave_up_sort,
+            ))
             continue
         res = inp.result
         skip_reasons = {s.property_title: s.reason for s in res.skipped}
diff --git a/composer/spec/source/struct_invariant.py b/composer/spec/source/struct_invariant.py
index 630286c..908c95d 100644
--- a/composer/spec/source/struct_invariant.py
+++ b/composer/spec/source/struct_invariant.py
@@ -24,6 +24,7 @@
 from composer.spec.graph_builder import bind_standard, run_to_completion
 from composer.spec.context import WorkflowContext, SourceCode, CacheKey, InvJudge
 from composer.spec.service_host import ServiceHost
+from composer.spec.source.harness import MainHarnessView
 from composer.spec.system_model import HarnessedApplication
 from composer.spec.gen_types import TypedTemplate
 from composer.spec.util import uniq_thread_id
@@ -80,6 +81,9 @@ def _merge_invariant_feedback(
 class InvariantParams(TypedDict):
     context: HarnessedApplication
     contract_spec: SourceCode
+    # The main-contract augmentation harness (rendered by
+    # harnessed_application_context.j2); None when the run has no main harness.
+    main_harness: MainHarnessView | None
 
 _typed_invariant_prompt = TypedTemplate[InvariantParams]("structural_invariant_prompt.j2")
 
@@ -87,7 +91,9 @@ async def get_invariant_formulation(
     ctx: WorkflowContext[None],
     source: SourceCode,
     env: ServiceHost,
-    app: HarnessedApplication
+    app: HarnessedApplication,
+    *,
+    main_harness: MainHarnessView | None = None,
 ) -> Invariants:
     """Run the structural invariant formulation agent.
 
@@ -98,7 +104,10 @@ async def get_invariant_formulation(
     Args:
         ctx: Workflow context for threading, memory, and checkpointing.
         source: Source code metadata (used for template rendering).
-        source_tools: Builder with fs_tools for source code reading.
+        env: Service host providing the LLM builder and source tools.
+        main_harness: The main-contract augmentation harness view (if any),
+            rendered into the application context so proposed invariants can
+            reference the harness getters/helpers.
 
     Returns:
         Validated structural invariants.
@@ -199,7 +208,8 @@ async def run(self) -> Command:
 
     bound_template = _typed_invariant_prompt.bind({
         "context": app,
-        "contract_spec": source
+        "contract_spec": source,
+        "main_harness": main_harness
     })
 
     graph = bind_standard(

From 14690d79a82687619c6e84ad680abd84d4df70f9 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Fri, 3 Jul 2026 21:42:22 +0300
Subject: [PATCH 03/13] Complete give-up-sort threading into the report schema
 and HTML render

GaveUpComponent carries the author's give-up classification (optional-with-
default so persisted pre-change reports still validate) and the report
renders it as a tag next to the component heading.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/report/schema.py       | 4 ++++
 composer/templates/autoprove_report.html.j2 | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/composer/spec/source/report/schema.py b/composer/spec/source/report/schema.py
index 3fb6a4f..68d5edb 100644
--- a/composer/spec/source/report/schema.py
+++ b/composer/spec/source/report/schema.py
@@ -120,6 +120,10 @@ class GaveUpComponent(BaseModel):
     crashed), so none of its inferred properties were formalized. No per-property reason."""
     component: ComponentName
     properties: list[PropertyFormulation]
+    # The author's give-up classification (env_issue / needs_harness / prover_limit / other);
+    # None for crashes and for backends that don't classify give-ups. Optional-with-default
+    # so persisted pre-change reports still validate.
+    give_up_sort: str | None = None
 
 
 class PropertyGroup(BaseModel):
diff --git a/composer/templates/autoprove_report.html.j2 b/composer/templates/autoprove_report.html.j2
index 894c6c9..4864cbf 100644
--- a/composer/templates/autoprove_report.html.j2
+++ b/composer/templates/autoprove_report.html.j2
@@ -298,7 +298,7 @@ footer.report-foot {
   {%- if gave_up %}
   <h3>Components that gave up ({{ gave_up | length }})</h3>
   {%- for gc in gave_up %}
-  <h4>{{ gc.component }}</h4>
+  <h4>{{ gc.component }}{% if gc.give_up_sort %} <span class="sort-tag">{{ gc.give_up_sort }}</span>{% endif %}</h4>
   <ul class="claims">
     {%- for p in gc.properties %}<li><span class="sort-tag">{{ p.sort }}</span> {{ p.description }}</li>{% endfor %}
   </ul>

From 4e62f302c32e002919fccfc6c37058cb28f83b10 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Fri, 3 Jul 2026 21:43:39 +0300
Subject: [PATCH 04/13] Surface the main-harness verification API in author,
 judge, and invariant prompts

The generation and judge prompts render the harness_api one-liners as a
verification_harness section (with the rule that "state is inaccessible" is
not a valid skip when a harness getter exposes it), and
harnessed_application_context.j2 renders the main-harness view for the
structural-invariant flow. All blocks are guarded so harness-free runs render
unchanged.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .../templates/harnessed_application_context.j2   |  9 +++++++++
 composer/templates/property_generation_prompt.j2 | 16 ++++++++++++++++
 composer/templates/property_judge_prompt.j2      | 15 +++++++++++++++
 3 files changed, 40 insertions(+)

diff --git a/composer/templates/harnessed_application_context.j2 b/composer/templates/harnessed_application_context.j2
index 6ffc272..e15e0fd 100644
--- a/composer/templates/harnessed_application_context.j2
+++ b/composer/templates/harnessed_application_context.j2
@@ -8,3 +8,12 @@ This contract component is modelled using the following concrete "harnesses":
 {% endfor %}
 {% endif %}
 {% endcall %}
+{% if main_harness %}
+
+The main contract `{{ main_harness.harness_of }}` is verified through the augmentation harness
+`{{ main_harness.name }}` (located at `{{ main_harness.path }}`), which extends it with the following
+verification API — usable in rules/invariants like any other external function of the contract:
+{% for line in main_harness.api %}
+* {{ line }}
+{% endfor %}
+{% endif %}
diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2
index d96585c..5330999 100644
--- a/composer/templates/property_generation_prompt.j2
+++ b/composer/templates/property_generation_prompt.j2
@@ -161,6 +161,22 @@ You may also make use of the following CVL resources, available as CVL files.
 {% endfor %}
 {% endif %}
 
+{% if harness_api %}
+<verification_harness>
+The contract is verified through an augmentation harness that extends {{ contract_name }} with the
+following verification API (external view getters over otherwise-unobservable storage, and thin external
+wrappers around internal steps of monolithic functions). You may — and should — use these getters/helpers
+directly in your rules and invariants, exactly like any other external function of the contract:
+
+{% for line in harness_api %}
+* {{ line }}
+{% endfor %}
+
+Because this API exists, "the state is inaccessible / has no public getter" is NOT a valid reason to skip
+a property when a harness getter above exposes that state.
+</verification_harness>
+{% endif %}
+
 <state>
 Use the available memory tools to track your progress through this algorithm, any important lessons about CVL you may have learned,
 or any other significant, relevant information to this task. In particular, be sure to update your memory before calling the prover to summarize
diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2
index 537b2af..3462452 100644
--- a/composer/templates/property_judge_prompt.j2
+++ b/composer/templates/property_judge_prompt.j2
@@ -219,6 +219,21 @@ this specification.
 </application>
 {% endif %}
 
+{% if harness_api %}
+<verification_harness>
+The contract is verified through an augmentation harness exposing the following verification API
+(external view getters over otherwise-unobservable storage, and thin external wrappers around internal
+steps of monolithic functions). The author may use these getters/helpers directly in rules and invariants:
+
+{% for line in harness_api %}
+* {{ line }}
+{% endfor %}
+
+When evaluating skips under Criteria 7: "the state is inaccessible / has no public getter" is NOT a valid
+skip justification when a harness getter above exposes that state.
+</verification_harness>
+{% endif %}
+
 <guidance>
 <hard_requirement>
 Do not provide ANY feedback except for the 7 criteria above.

From ec218deb600f845dd24a779a56e853ec25c1db16 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Fri, 3 Jul 2026 21:46:36 +0300
Subject: [PATCH 05/13] Test the main-harness models, verify-target accessors,
 and prompt rendering

Pydantic cache back-compat (pre-change JSON without the new optional fields
still validates), verify_contract_name/path threading accessors, api_lines/
main_harness_view helpers, GiveUp sort default, and render coverage for the
new/changed templates with and without a harness.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 tests/test_main_harness.py | 253 +++++++++++++++++++++++++++++++++++++
 1 file changed, 253 insertions(+)
 create mode 100644 tests/test_main_harness.py

diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
new file mode 100644
index 0000000..e7d717c
--- /dev/null
+++ b/tests/test_main_harness.py
@@ -0,0 +1,253 @@
+"""Tests for the main-contract augmentation harness (composer.spec.source.harness).
+
+Covers the pure pieces — pydantic cache back-compat (pre-change JSON without the
+new optional fields must still validate), the `verify_contract_name`/`verify_contract_path`
+accessors that thread the verify target through the pipeline, the prompt-facing
+`api_lines`/`main_harness_view` helpers, the `GiveUpTool` sort classification defaults,
+and rendering of the new/changed templates. No LLM / no prover / no DB.
+"""
+
+import pytest
+
+from composer.spec.source.author import GaveUp
+from composer.spec.source.harness import (
+    AgentSystemDescription,
+    HarnessDef,
+    HarnessedContract,
+    HelperDecomposition,
+    MainHarnessPlan,
+    MainHarnessView,
+    SystemDescriptionHarnessed,
+    UnstructuredSlotSpec,
+)
+from composer.spec.source.report.schema import GaveUpComponent
+from composer.spec.system_model import HarnessedApplication, SourceApplication
+from composer.templates.loader import load_jinja_template
+
+
+# ---------------------------------------------------------------------------
+# Builders
+# ---------------------------------------------------------------------------
+
+def _base_description_fields() -> dict:
+    """The pre-change wire shape shared by both system-description models."""
+    return {
+        "non_trivial_state": "some non-trivial state",
+        "transitive_closure": [],
+        "erc20_contracts": [],
+        "external_interfaces": [],
+    }
+
+
+def _plan() -> MainHarnessPlan:
+    return MainHarnessPlan(
+        unstructured_slots=[
+            UnstructuredSlotSpec(
+                getter_name="getVersionSlot",
+                slot_derivation='keccak256("river.state.version") - 1',
+                value_type="uint256",
+                rationale="version invariants need to observe it",
+            )
+        ],
+        decompositions=[
+            HelperDecomposition(
+                target_function="depositAndTransfer(address)",
+                helpers={"helperDeposit": "performs the deposit accounting step"},
+                rationale="each step must be verifiable in isolation",
+            )
+        ],
+    )
+
+
+def _main_harness_contract() -> HarnessedContract:
+    return HarnessedContract(
+        solidity_identifier="RiverHarness",
+        link_fields=[],
+        harness_definition=HarnessDef(
+            harness_of="River",
+            harness_source="contract RiverHarness is River {}",
+        ),
+        path="certora/harnesses/RiverHarness.sol",
+    )
+
+
+# ---------------------------------------------------------------------------
+# Pydantic cache back-compat: pre-change JSON (no new fields) still validates
+# ---------------------------------------------------------------------------
+
+def test_agent_system_description_backcompat():
+    desc = AgentSystemDescription.model_validate({
+        **_base_description_fields(),
+        "transitive_closure": [
+            {"solidity_identifier": "Token", "link_fields": [], "num_instances": None}
+        ],
+    })
+    assert desc.main_contract_harness is None
+    assert not desc.needs_harnessing()
+
+
+def test_system_description_harnessed_backcompat():
+    desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
+    assert desc.main_harness is None
+    assert desc.main_harness_plan is None
+    assert desc.main_harness_api() is None
+    assert desc.main_harness_view() is None
+
+
+def test_gave_up_backcompat_defaults_sort_other():
+    gave_up = GaveUp.model_validate({"reason": "no solc"})
+    assert gave_up.sort == "other"
+
+
+def test_gave_up_component_backcompat():
+    gc = GaveUpComponent.model_validate({"component": "Vault", "properties": []})
+    assert gc.give_up_sort is None
+
+
+# ---------------------------------------------------------------------------
+# Verify-target accessors
+# ---------------------------------------------------------------------------
+
+def test_verify_contract_name_defaults_to_main_contract():
+    desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
+    assert desc.verify_contract_name("River") == "River"
+    assert desc.verify_contract_path("src/River.sol") == "src/River.sol"
+
+
+def test_verify_contract_name_prefers_main_harness():
+    desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
+    desc.main_harness = _main_harness_contract()
+    desc.main_harness_plan = _plan()
+    assert desc.verify_contract_name("River") == "RiverHarness"
+    assert desc.verify_contract_path("src/River.sol") == "certora/harnesses/RiverHarness.sol"
+
+
+def test_main_harness_api_and_view():
+    desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
+    desc.main_harness = _main_harness_contract()
+    desc.main_harness_plan = _plan()
+
+    api = desc.main_harness_api()
+    assert api is not None
+    # One line per getter, one per helper wrapper.
+    assert len(api) == 2
+    assert any("getVersionSlot" in line for line in api)
+    assert any("helperDeposit" in line for line in api)
+
+    view = desc.main_harness_view()
+    assert view is not None
+    assert view.name == "RiverHarness"
+    assert view.harness_of == "River"
+    assert view.api == api
+
+
+def test_classifier_rejects_empty_harness_plan():
+    # An all-empty plan should be delivered as null; mirror the validator's check.
+    plan = MainHarnessPlan(unstructured_slots=[], decompositions=[])
+    assert not plan.unstructured_slots and not plan.decompositions
+    assert plan.api_lines() == []
+
+
+# ---------------------------------------------------------------------------
+# Template rendering
+# ---------------------------------------------------------------------------
+
+class _Prop:
+    sort = "safety"
+    title = "version_is_monotone"
+    description = "the version never decreases"
+
+
+class _Spec:
+    contract_name = "River"
+    relative_path = "src/River.sol"
+
+
+def test_main_harness_generation_prompt_renders():
+    out = load_jinja_template(
+        "main_harness_generation_prompt.j2",
+        contract_name="River",
+        relative_path="src/River.sol",
+        harness_name="RiverHarness",
+        plan=_plan(),
+    )
+    assert "contract RiverHarness is River" in out
+    assert "getVersionSlot" in out
+    assert "helperDeposit" in out
+    assert "certora/harnesses/RiverHarness.sol" in out
+
+
+def test_state_analysis_renders_main_harness_step():
+    app = SourceApplication(application_type="Staking", description="desc", components=[])
+    out = load_jinja_template(
+        "state_analysis.j2",
+        contract_name="River",
+        relative_path="src/River.sol",
+        context=app,
+    )
+    assert "main_contract_harness" in out
+    assert "ERC-7201" in out
+
+
+@pytest.mark.parametrize("with_api", [True, False])
+def test_property_generation_prompt_harness_api(with_api: bool):
+    api = _plan().api_lines() if with_api else None
+    out = load_jinja_template(
+        "property_generation_prompt.j2",
+        properties=[_Prop()],
+        contract_name="River",
+        resources=[],
+        context=None,
+        harness_api=api,
+    )
+    assert ("<verification_harness>" in out) == with_api
+    assert ("getVersionSlot" in out) == with_api
+
+
+def test_property_judge_prompt_harness_api():
+    out = load_jinja_template(
+        "property_judge_prompt.j2",
+        properties=[_Prop()],
+        sort="existing",
+        context=None,
+        harness_api=_plan().api_lines(),
+    )
+    assert "<verification_harness>" in out
+    assert "getVersionSlot" in out
+    # Binding without harness_api at all (the NotRequired key) renders harness-free.
+    out = load_jinja_template(
+        "property_judge_prompt.j2",
+        properties=[_Prop()],
+        sort="existing",
+        context=None,
+    )
+    assert "<verification_harness>" not in out
+
+
+def test_judge_system_prompt_accepts_harness_augmentation_flag():
+    # This PR only plumbs the variable; the gated wording lands separately. The
+    # template must render regardless of the flag's value.
+    for flag in (True, False):
+        out = load_jinja_template(
+            "property_judge_system_prompt.j2", sort="existing", harness_augmentation=flag,
+        )
+        assert out
+
+
+@pytest.mark.parametrize("with_harness", [True, False])
+def test_structural_invariant_prompt_main_harness(with_harness: bool):
+    view = MainHarnessView(
+        name="RiverHarness",
+        path="certora/harnesses/RiverHarness.sol",
+        harness_of="River",
+        api=_plan().api_lines(),
+    ) if with_harness else None
+    app = HarnessedApplication(application_type="Staking", description="desc", components=[])
+    out = load_jinja_template(
+        "structural_invariant_prompt.j2",
+        context=app,
+        contract_spec=_Spec(),
+        main_harness=view,
+    )
+    assert ("RiverHarness" in out) == with_harness
+    assert ("getVersionSlot" in out) == with_harness

From e9e2d5a178a2085034dc5a0eee608163b60781c4 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Fri, 3 Jul 2026 21:59:23 +0300
Subject: [PATCH 06/13] Confine main-harness delivery path and unit-test the
 classifier's empty-plan rejection

Review fixes: the generation result validator now rejects deliveries outside
certora/harnesses/ (VFS write confinement only blocks writes, so a pre-existing
project file could otherwise pass as the harness), and the empty-plan check is
extracted to a pure module-level function so the test exercises the real
validator logic instead of restating it.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/harness.py | 27 +++++++++++++++++++++++----
 tests/test_main_harness.py      | 23 +++++++++++++++++++----
 2 files changed, 42 insertions(+), 8 deletions(-)

diff --git a/composer/spec/source/harness.py b/composer/spec/source/harness.py
index efe7d76..51e305c 100644
--- a/composer/spec/source/harness.py
+++ b/composer/spec/source/harness.py
@@ -132,6 +132,25 @@ def api_lines(self) -> list[str]:
                 )
         return lines
 
+def empty_main_harness_plan_error(plan: MainHarnessPlan | None) -> str | None:
+    """The classifier must deliver ``null`` rather than an all-empty plan.
+    Module-level (not inlined in the agent's result validator) so the rejection
+    is unit-testable without running the agent."""
+    if plan is not None and \
+            not plan.unstructured_slots and \
+            not plan.decompositions:
+        return "main_contract_harness was proposed but contains no getters and no decompositions; deliver null instead"
+    return None
+
+def main_harness_path_error(path: str) -> str | None:
+    """The delivered harness must live under ``certora/harnesses/``. The VFS
+    write confinement only blocks *writes* outside that directory; without this
+    check the agent could deliver a pre-existing project file (e.g. a protocol
+    source) as the "generated" harness. Module-level for unit-testability."""
+    if not path.startswith("certora/harnesses/"):
+        return f"Delivered harness at {path}, but the harness must be a new file under `certora/harnesses/`"
+    return None
+
 class MainHarnessView(BaseModel):
     """Prompt-facing view of the main-contract augmentation harness, rendered by
     `harnessed_application_context.j2` so downstream agents see the harness API."""
@@ -271,10 +290,8 @@ def result_validator(
         for c in res.transitive_closure:
             if c.solidity_identifier not in contract_lkp:
                 return f"Contract {c.solidity_identifier} in the interaction closure doesn't appear in the application description"
-        if res.main_contract_harness is not None and \
-                not res.main_contract_harness.unstructured_slots and \
-                not res.main_contract_harness.decompositions:
-            return "main_contract_harness was proposed but contains no getters and no decompositions; deliver null instead"
+        if (plan_error := empty_main_harness_plan_error(res.main_contract_harness)) is not None:
+            return plan_error
         return None
 
     d = bind_standard(
@@ -550,6 +567,8 @@ def result_validator(
     ) -> str | None:
         if res.harness_name != expected_name:
             return f"Harness contract must be named {expected_name}, got {res.harness_name}"
+        if (path_error := main_harness_path_error(res.path)) is not None:
+            return path_error
         if mat.get(s, res.path) is None:
             return f"Delivered harness {res.harness_name} at {res.path}, but it doesn't exist on the VFS"
         return None
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index e7d717c..98ca24b 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -19,6 +19,8 @@
     MainHarnessView,
     SystemDescriptionHarnessed,
     UnstructuredSlotSpec,
+    empty_main_harness_plan_error,
+    main_harness_path_error,
 )
 from composer.spec.source.report.schema import GaveUpComponent
 from composer.spec.system_model import HarnessedApplication, SourceApplication
@@ -142,10 +144,23 @@ def test_main_harness_api_and_view():
 
 
 def test_classifier_rejects_empty_harness_plan():
-    # An all-empty plan should be delivered as null; mirror the validator's check.
-    plan = MainHarnessPlan(unstructured_slots=[], decompositions=[])
-    assert not plan.unstructured_slots and not plan.decompositions
-    assert plan.api_lines() == []
+    # An all-empty plan should be delivered as null; this is the exact check the
+    # classifier's result validator runs.
+    err = empty_main_harness_plan_error(MainHarnessPlan(unstructured_slots=[], decompositions=[]))
+    assert err is not None
+    assert "deliver null" in err
+    # A null plan and a non-empty plan both pass.
+    assert empty_main_harness_plan_error(None) is None
+    assert empty_main_harness_plan_error(_plan()) is None
+
+
+def test_main_harness_delivery_confined_to_harness_dir():
+    # The generation validator must reject deliveries outside certora/harnesses/
+    # (write confinement alone doesn't stop delivering a pre-existing project file).
+    assert main_harness_path_error("certora/harnesses/RiverHarness.sol") is None
+    err = main_harness_path_error("src/River.sol")
+    assert err is not None
+    assert "certora/harnesses" in err
 
 
 # ---------------------------------------------------------------------------

From cef0de3f371cc63abc5bfc8a2c99b151b7888497 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 02:47:14 +0300
Subject: [PATCH 07/13] Add soundness guardrails for harness helpers to author,
 judge, and shared context

The harness is the verified contract, so helper wrappers participate in
parametric rules and invariant preservation while exposing transitions
unreachable in production. The author prompt now explains this, gives the
concrete filtered/f.selector exclusion idiom against the rendered harness API
list (preferred over require-weakening for helper-only counterexamples), and
bans harness helpers as satisfy/liveness/reachability witnesses. The judge
prompt mirrors all three, plus the filter-legitimacy taxonomy: a filtered
block is legitimate iff every excluded method is a documented harness helper
or covered by a recorded vacuity acknowledgment; anything else is suspect.
The shared harnessed context carries the same caveat for the invariant
formulator. Render tests assert each guardrail appears exactly when the
harness API is bound.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .../harnessed_application_context.j2          |  5 ++++
 .../templates/property_generation_prompt.j2   | 25 +++++++++++++++++++
 composer/templates/property_judge_prompt.j2   | 17 +++++++++++++
 tests/test_main_harness.py                    | 14 +++++++++++
 4 files changed, 61 insertions(+)

diff --git a/composer/templates/harnessed_application_context.j2 b/composer/templates/harnessed_application_context.j2
index e15e0fd..fc54aa3 100644
--- a/composer/templates/harnessed_application_context.j2
+++ b/composer/templates/harnessed_application_context.j2
@@ -16,4 +16,9 @@ verification API — usable in rules/invariants like any other external function
 {% for line in main_harness.api %}
 * {{ line }}
 {% endfor %}
+
+Since the harness is the verified contract, these methods also participate in parametric rules and
+invariant preservation. The helper wrappers expose internal steps as standalone transitions that are NOT
+reachable in production; do not treat a helper-only transition as evidence about production behavior, and
+never use a helper as the witness of a reachability/`satisfy` claim.
 {% endif %}
diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2
index 5330999..d6a10ab 100644
--- a/composer/templates/property_generation_prompt.j2
+++ b/composer/templates/property_generation_prompt.j2
@@ -174,6 +174,31 @@ directly in your rules and invariants, exactly like any other external function
 
 Because this API exists, "the state is inaccessible / has no public getter" is NOT a valid reason to skip
 a property when a harness getter above exposes that state.
+
+Because the harness is the *verified* contract, the harness API above also participates in parametric
+rules (`method f`) and in invariant preservation checks. The helper wrappers expose internal mid-states
+as standalone transitions that are NOT reachable in the production contract (in production those steps
+only execute inside their monolithic caller). Follow these rules:
+
+* If a parametric rule or invariant fails and the counterexample's only state-changing step is a harness
+  helper wrapper, the failure may be a harness artifact rather than a real violation. Assess whether the
+  violating transition is reachable through {{ contract_name }}'s production external interface. If it is
+  not, exclude the helper from that rule/invariant with a documented `filtered` block instead of weakening
+  the property with `require` statements. The idiom (the parametric method's contract is always the
+  verified harness here, so `f.selector` is the discriminator; combine exclusions with `&&`):
+
+  ```
+  invariant total_matches_sum()
+      ...
+      filtered { f -> f.selector != sig:helperStep(address).selector }
+  ```
+
+  Only filter methods that appear in the harness API list above, and add a comment on the `filtered`
+  block naming each excluded method as a documented harness helper. The storage getters are `view`
+  functions: they cannot change state and never need filtering.
+* HARD RULE: never use a harness helper wrapper as the witness of a `satisfy`, liveness, or reachability
+  claim. A state reachable only through a helper proves nothing about the production contract — the
+  witness must go through {{ contract_name }}'s real external interface.
 </verification_harness>
 {% endif %}
 
diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2
index 3462452..1316ab8 100644
--- a/composer/templates/property_judge_prompt.j2
+++ b/composer/templates/property_judge_prompt.j2
@@ -231,6 +231,23 @@ steps of monolithic functions). The author may use these getters/helpers directl
 
 When evaluating skips under Criteria 7: "the state is inaccessible / has no public getter" is NOT a valid
 skip justification when a harness getter above exposes that state.
+
+Because the harness is the *verified* contract, its helper wrappers also participate in parametric rules
+and invariant preservation, and they expose transitions that are NOT reachable in production (in production
+those steps only execute inside their monolithic caller). Enforce the following, as part of the criteria
+above:
+
+* Reject any `satisfy`/liveness/reachability claim whose witness runs through a harness helper wrapper: a
+  state reachable only via a helper proves nothing about the production contract. Demand a witness through
+  the production external interface.
+* If the author weakened a property (added `require`s, weakened an assertion) in response to a
+  counterexample whose only state-changing step was a harness helper, reject the weakening: the correct
+  response to a helper-only, production-unreachable counterexample is a documented `filtered` exclusion of
+  that helper, not a weaker property.
+* Filter legitimacy: a `filtered` block is legitimate if and only if every method it excludes is either
+  (i) a documented harness helper from the API list above (the filter should carry a comment naming it), or
+  (ii) covered by a recorded vacuity acknowledgment. Any other exclusion is suspect — treat it as
+  potentially hiding a real counterexample and demand the author justify or remove it.
 </verification_harness>
 {% endif %}
 
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index 98ca24b..171e4b5 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -217,6 +217,11 @@ def test_property_generation_prompt_harness_api(with_api: bool):
     )
     assert ("<verification_harness>" in out) == with_api
     assert ("getVersionSlot" in out) == with_api
+    # Soundness guardrails render exactly when the harness API does: parametric
+    # participation, the filtered-exclusion idiom, and the satisfy-witness ban.
+    assert ("NOT reachable in the production contract" in out) == with_api
+    assert ("filtered { f -> f.selector != sig:" in out) == with_api
+    assert ("never use a harness helper wrapper as the witness" in out) == with_api
 
 
 def test_property_judge_prompt_harness_api():
@@ -229,6 +234,12 @@ def test_property_judge_prompt_harness_api():
     )
     assert "<verification_harness>" in out
     assert "getVersionSlot" in out
+    # The judge mirrors the author guardrails: helper-witnessed satisfy claims,
+    # harness-artifact-driven weakenings, and the filter-legitimacy taxonomy
+    # (documented harness helper OR recorded vacuity acknowledgment).
+    assert "witness runs through a harness helper wrapper" in out
+    assert "reject the weakening" in out
+    assert "recorded vacuity acknowledgment" in out
     # Binding without harness_api at all (the NotRequired key) renders harness-free.
     out = load_jinja_template(
         "property_judge_prompt.j2",
@@ -266,3 +277,6 @@ def test_structural_invariant_prompt_main_harness(with_harness: bool):
     )
     assert ("RiverHarness" in out) == with_harness
     assert ("getVersionSlot" in out) == with_harness
+    # The shared harnessed context carries the parametric/witness caveat, so the
+    # invariant formulator sees the same soundness guardrails as the CVL author.
+    assert ("never use a helper as the witness" in out) == with_harness

From 05a542983a5d64d51594d0630f84383d520c66e9 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 02:49:26 +0300
Subject: [PATCH 08/13] Thread harness_augmentation into both judge template
 binds
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

property_feedback_judge now injects its harness_augmentation parameter into
the task-prompt bind as well as the system-prompt bind, via a shared
_bind_harness_augmentation helper, so the Criteria 7 gate (which reads the
identically-named task-prompt variable) can never disagree with the system
prompt's harness-aware wording. The mirror NotRequired field on
JudgeSystemParams goes away — the function parameter is the single source of
the flag. Render test asserts the flag reaches both binds for both values.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/feedback.py  | 33 ++++++++++++++++++++++++---------
 tests/test_main_harness.py | 28 ++++++++++++++++++++++++++++
 2 files changed, 52 insertions(+), 9 deletions(-)

diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py
index 5bde355..a03cab1 100644
--- a/composer/spec/feedback.py
+++ b/composer/spec/feedback.py
@@ -49,9 +49,6 @@ class FeedbackInherentParams(TypedDict):
 
 class JudgeSystemParams(TypedDict):
     sort: Sort
-    # True when the run verifies through a main-contract augmentation harness;
-    # gates the harness-aware wording (the template defaults it to false).
-    harness_augmentation: NotRequired[bool]
 
 # Judge system prompt, shared between the natspec and source-mode flows. The fs
 # primitives are always documented; ``sort`` drives the rest (the template
@@ -59,22 +56,37 @@ class JudgeSystemParams(TypedDict):
 # ``sort == "existing"``, the only mode that wires those tools).
 FeedbackSystemTemplate = TypedTemplate[JudgeSystemParams]("property_judge_system_prompt.j2")
 
+
+def _bind_harness_augmentation(
+    prompt: TemplateInstantiation, harness_augmentation: bool
+) -> TemplateInstantiation:
+    """Inject the ``harness_augmentation`` flag into an already-instantiated template bind.
+
+    Both judge templates gate their harness-skip policy on this variable; injecting it
+    from the single ``property_feedback_judge`` parameter into BOTH binds is what keeps
+    the system prompt and Criteria 7 in agreement. The templates' ``default(false)`` is
+    a render fail-safe only, never the mechanism that decides the value.
+    """
+    return TemplateInstantiation(
+        prompt.template,
+        {**prompt.args, "harness_augmentation": harness_augmentation},
+    )
+
+
 def property_feedback_judge(
     ctx: WorkflowContext[CVLJudge],
     env: ServiceHost,
     prompt: InjectedTemplate[Properties] | TemplateInstantiation,
     props: list[PropertyFormulation],
     *,
+    harness_augmentation: bool = False,
     extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None,
     system_prompt: TemplateInstantiation | None = None,
-    harness_augmentation: bool = False,
 ) -> FeedbackToolContext:
 
     if system_prompt is None:
-        system_prompt = FeedbackSystemTemplate.bind({
-            "sort": env.sort,
-            "harness_augmentation": harness_augmentation,
-        })
+        system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort})
+    system_prompt = _bind_harness_augmentation(system_prompt, harness_augmentation)
 
     builder = env.builder_heavy().with_tools(
         env.all_tools
@@ -98,7 +110,10 @@ def did_rough_draft_read(s: ST, _) -> str | None:
 
     mem = ctx.get_memory_tool()
 
-    final_prompt = prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props})
+    final_prompt = _bind_harness_augmentation(
+        prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props}),
+        harness_augmentation,
+    )
 
     workflow = bind_standard(
         builder, ST, validator=did_rough_draft_read
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index 171e4b5..eaa946a 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -260,6 +260,34 @@ def test_judge_system_prompt_accepts_harness_augmentation_flag():
         assert out
 
 
+@pytest.mark.parametrize("flag", [True, False])
+def test_harness_augmentation_reaches_both_judge_binds(flag: bool):
+    # property_feedback_judge threads its harness_augmentation parameter into BOTH
+    # template binds via _bind_harness_augmentation; the task-prompt gate (Criteria 7)
+    # reads the identically-named variable, so the two prompts cannot disagree.
+    from composer.spec.feedback import (
+        FeedbackSystemTemplate, FeedbackTemplate, Properties, _bind_harness_augmentation,
+    )
+
+    # System-prompt bind (as property_feedback_judge builds it).
+    sys_bind = _bind_harness_augmentation(
+        FeedbackSystemTemplate.bind({"sort": "existing"}), flag,
+    )
+    assert sys_bind.args["harness_augmentation"] is flag
+    assert sys_bind.render_to(load_jinja_template)
+
+    # Task-prompt bind, through the exact InjectedTemplate path batch_cvl_generation uses.
+    task_bind = _bind_harness_augmentation(
+        FeedbackTemplate.bind({
+            "sort": "existing", "context": None, "harness_api": _plan().api_lines() if flag else None,
+        }).depends(Properties).inject({"properties": [_Prop()]}),
+        flag,
+    )
+    assert task_bind.args["harness_augmentation"] is flag
+    assert task_bind.args["properties"]
+    assert task_bind.render_to(load_jinja_template)
+
+
 @pytest.mark.parametrize("with_harness", [True, False])
 def test_structural_invariant_prompt_main_harness(with_harness: bool):
     view = MainHarnessView(

From 25d93023ca92afc45c3a26ee23302d5b10d21975 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 02:52:52 +0300
Subject: [PATCH 09/13] Fall back to the raw contract when the augmentation
 harness fails AutoSetup

run_autosetup_phase now attempts AutoSetup per verify target (each target
under its own cache key): if the generated main-contract harness fails
compilation/setup, the phase logs the failure, clears main_harness and
main_harness_plan on the system description (so verify_contract_name,
verify_contract_path, main_harness_api, and main_harness_view all revert to
the raw contract), records the downgrade in the new main_harness_fallback
field for the report, and retries against the raw main contract. Only a
raw-contract failure hard-fails the run. Failures are never cached, so a
rerun retries the harness before falling back again.

The pipeline now computes the verify target, harness API, and prover tool
AFTER the AutoSetup join, so a fallback is reflected in the prover tool,
conf dumps, and author/judge prompts. The invariant formulator, which runs
concurrently with AutoSetup, intentionally keeps the pre-fallback harness
view; harness-only invariants then fail formalization downstream under the
post-fallback state.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/harness.py  | 116 +++++++++++++++++--------
 composer/spec/source/pipeline.py |  42 +++++----
 tests/test_main_harness.py       | 143 +++++++++++++++++++++++++++++++
 3 files changed, 247 insertions(+), 54 deletions(-)

diff --git a/composer/spec/source/harness.py b/composer/spec/source/harness.py
index 51e305c..85d6be0 100644
--- a/composer/spec/source/harness.py
+++ b/composer/spec/source/harness.py
@@ -208,6 +208,11 @@ class SystemDescriptionHarnessed(SystemDescriptionBase[HarnessedContract]):
     # kept so downstream prompts can describe the harness API.
     main_harness: HarnessedContract | None = None
     main_harness_plan: MainHarnessPlan | None = None
+    # Human-readable reason when the generated harness failed AutoSetup and the run
+    # fell back to verifying the raw main contract (see ``run_autosetup_phase``).
+    # Set in-run only, never cached: the description is cached before AutoSetup runs,
+    # so a rerun retries the harness before falling back again.
+    main_harness_fallback: str | None = None
 
     def verify_contract_name(self, default_name: str) -> str:
         """The contract identifier the prover verifies: the main-harness identifier
@@ -846,53 +851,90 @@ async def run_autosetup_phase(
     return the compilation config + summaries. Depends on harness creation
     having run first: it reads the transitive-closure file paths from disk.
 
+    When a main-contract augmentation harness exists, the harness *is* the
+    verified contract: it becomes AutoSetup's target (the original main
+    contract enters the scene through inheritance, not as its own instance).
+    If AutoSetup fails on the harness, the phase falls back to the raw main
+    contract instead of hard-failing the run: it clears ``main_harness`` /
+    ``main_harness_plan`` on ``sys_desc`` (so every verify-target and prompt
+    accessor reverts automatically — the pipeline computes the verify target
+    after this phase) and records the downgrade in ``main_harness_fallback``
+    for the report. Failures are never cached, so a rerun retries the harness
+    before falling back again.
+
     Cache hits are guarded by the on-disk existence of ``summaries_path``."""
-    # When a main-contract augmentation harness exists, the harness *is* the
-    # verified contract: it becomes AutoSetup's target (the original main
-    # contract enters the scene through inheritance, not as its own instance).
-    verify_harness = (
-        sys_desc.main_harness.solidity_identifier if sys_desc.main_harness is not None else None
-    )
     config_ctxt = context.child(config_key)
-    cache = await config_ctxt.child(
-        autosetup_key(application_desc, prover_opts, verify_harness),
-        application_desc.model_dump(),
-    )
-    if (cached := await cache.cache_get(SetupSuccess)) is not None:
-        if under_project(source.project_root, certora_relative_to_project(cached.summaries_path)).exists():
-            return cached
 
     extra_files = [
         c.path for c in sys_desc.transitive_closure if c.solidity_identifier != source.contract_name
     ]
 
-    setup_result = await run_autosetup(
-        Path(source.project_root),
-        sys_desc.verify_contract_path(source.relative_path),
-        sys_desc.verify_contract_name(source.contract_name),
-        prover_opts,
-        *extra_files,
-    )
+    async def attempt(verify: HarnessedContract | None) -> SetupSuccess | SetupFailure:
+        """One AutoSetup attempt: against the augmentation harness when ``verify``
+        is given, the raw main contract otherwise. Each target caches under its
+        own key (``autosetup_key``'s verify component), so a fallback result can
+        never be replayed as a harness result or vice versa."""
+        cache = await config_ctxt.child(
+            autosetup_key(
+                application_desc, prover_opts,
+                verify.solidity_identifier if verify is not None else None,
+            ),
+            application_desc.model_dump(),
+        )
+        if (cached := await cache.cache_get(SetupSuccess)) is not None:
+            if under_project(source.project_root, certora_relative_to_project(cached.summaries_path)).exists():
+                return cached
+
+        setup_result = await run_autosetup(
+            Path(source.project_root),
+            verify.path if verify is not None else source.relative_path,
+            verify.solidity_identifier if verify is not None else source.contract_name,
+            prover_opts,
+            *extra_files,
+        )
+
+        if isinstance(setup_result, SetupFailure):
+            return setup_result
+
+        # AutoSetup runs as a subprocess; its LLM token usage never reaches composer's
+        # UsageCallback. Fold the counts it wrote to disk into the run summary so they
+        # land in token_usage.json, the run tag, and the end-of-run table. No task_id:
+        # the active task is already AUTOSETUP_TASK_ID, so this attributes to the
+        # autosetup phase. Guarded — read_autosetup_usage returns [] if absent. This is
+        # only reached on a cache miss (cache hits return above), so usage spent in this
+        # process's autosetup run is counted exactly once.
+        summary = get_run_summary()
+        for usage in read_autosetup_usage(Path(source.project_root)):
+            summary.record_token_usage(usage)
+        # Likewise fold AutoSetup's subprocess prover runtime (prover-reported, cache hits
+        # excluded) into the run's prover_usage under the active AUTOSETUP_TASK_ID. None if
+        # absent — guarded so missing external usage can't break the phase.
+        if (autosetup_prover_ms := read_autosetup_prover_usage(Path(source.project_root))) is not None:
+            summary.record_prover_runtime(autosetup_prover_ms)
+
+        await cache.cache_put(setup_result)
+        return setup_result
+
+    main_harness = sys_desc.main_harness
+    setup_result = await attempt(main_harness)
+
+    if isinstance(setup_result, SetupFailure) and main_harness is not None:
+        # Raw-contract fallback: a broken generated harness (classifier false
+        # positive, bad import/constructor/solc detail) must not kill a run that
+        # succeeds on the raw contract.
+        reason = (
+            f"AutoSetup failed for the augmentation harness {main_harness.solidity_identifier}; "
+            f"verification fell back to the raw contract {source.contract_name}. "
+            f"Error: {setup_result.error}"
+        )
+        _logger.warning("%s\nProc stderr:\n%s", reason, setup_result.stderr)
+        sys_desc.main_harness = None
+        sys_desc.main_harness_plan = None
+        sys_desc.main_harness_fallback = reason
+        setup_result = await attempt(None)
 
     if isinstance(setup_result, SetupFailure):
         raise RuntimeError(f"Auto setup failed: {setup_result.error}\nProc stderr:\n{setup_result.stderr}")
 
-    # AutoSetup runs as a subprocess; its LLM token usage never reaches composer's
-    # UsageCallback. Fold the counts it wrote to disk into the run summary so they
-    # land in token_usage.json, the run tag, and the end-of-run table. No task_id:
-    # the active task is already AUTOSETUP_TASK_ID, so this attributes to the
-    # autosetup phase. Guarded — read_autosetup_usage returns [] if absent. This is
-    # only reached on a cache miss (cache hits return above), so usage spent in this
-    # process's autosetup run is counted exactly once.
-    summary = get_run_summary()
-    for usage in read_autosetup_usage(Path(source.project_root)):
-        summary.record_token_usage(usage)
-    # Likewise fold AutoSetup's subprocess prover runtime (prover-reported, cache hits
-    # excluded) into the run's prover_usage under the active AUTOSETUP_TASK_ID. None if
-    # absent — guarded so missing external usage can't break the phase.
-    if (autosetup_prover_ms := read_autosetup_prover_usage(Path(source.project_root))) is not None:
-        summary.record_prover_runtime(autosetup_prover_ms)
-
-    await cache.cache_put(setup_result)
     return setup_result
 
diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py
index 20557c2..ad4e618 100644
--- a/composer/spec/source/pipeline.py
+++ b/composer/spec/source/pipeline.py
@@ -140,22 +140,13 @@ async def run_autoprove_pipeline(
         components=comp
     )
 
-    # The verified contract, computed ONCE here: the main-harness identifier when
-    # harness creation produced a main-contract augmentation harness, the main
-    # contract itself otherwise. Everything downstream that names a verify target
-    # (prover tool, artifact-store conf dumps) derives from this.
-    verify_contract = sys_desc.verify_contract_name(source_input.contract_name)
-    source_input = replace(source_input, verify_contract=verify_contract)
-    # The harness API one-liners (None when no main harness), surfaced to the
-    # property authors and the feedback judge.
-    harness_api = sys_desc.main_harness_api()
-
-    # Prover tool is stateless with respect to setup, so build it now; it is
-    # shared by every CVL-generation call below.
-    prover_tool = get_prover_tool(
-        env.llm_heavy(), verify_contract,
-        source_input.project_root, prover_opts=prover_opts,
-    )
+    # Captured before the parallel phase below: the invariant formulator runs
+    # concurrently with AutoSetup, so it intentionally sees the pre-fallback
+    # harness view. If AutoSetup falls back to the raw contract mid-flight,
+    # invariants formulated over harness getters simply fail formalization
+    # downstream, where the post-fallback state (computed after the join)
+    # governs the verify target and prompts.
+    pre_fallback_harness_view = sys_desc.main_harness_view()
 
     # ------------------------------------------------------------------
     # Phase 3 (parallel branches, joined below):
@@ -199,7 +190,7 @@ async def stream_invariants():
             TaskInfo(INVARIANTS_TASK_ID, "Structural Invariants", AutoProvePhase.INVARIANTS),
             lambda: get_invariant_formulation(
                 ctx, source_input, env, harnessed_app,
-                main_harness=sys_desc.main_harness_view(),
+                main_harness=pre_fallback_harness_view,
             ),
         )
 
@@ -225,6 +216,23 @@ async def stream_bugs():
     if not component_batches:
         raise ValueError("No properties extracted from any component.")
 
+    # The verified contract, computed ONCE here — after AutoSetup, so a raw-contract
+    # fallback (which clears sys_desc.main_harness) is already reflected: the
+    # main-harness identifier when the augmentation harness survived AutoSetup, the
+    # main contract itself otherwise. Everything downstream that names a verify
+    # target (prover tool, artifact-store conf dumps) derives from this.
+    verify_contract = sys_desc.verify_contract_name(source_input.contract_name)
+    source_input = replace(source_input, verify_contract=verify_contract)
+    # The harness API one-liners (None when no main harness), surfaced to the
+    # property authors and the feedback judge.
+    harness_api = sys_desc.main_harness_api()
+
+    # The prover tool is shared by every CVL-generation call below.
+    prover_tool = get_prover_tool(
+        env.llm_heavy(), verify_contract,
+        source_input.project_root, prover_opts=prover_opts,
+    )
+
     store = source_input.artifact_store
 
     # In-memory invariant result (props + GeneratedCVL), threaded into the report phase below.
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index eaa946a..7e67991 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -288,6 +288,149 @@ def test_harness_augmentation_reaches_both_judge_binds(flag: bool):
     assert task_bind.render_to(load_jinja_template)
 
 
+# ---------------------------------------------------------------------------
+# Raw-contract fallback when the harness fails AutoSetup
+# ---------------------------------------------------------------------------
+
+def _fallback_fixture(tmp_path):
+    """A WorkflowContext (in-memory store), a SourceCode rooted at tmp_path, and a
+    harnessed system description, for driving run_autosetup_phase directly."""
+    from typing import Any, cast
+    from langgraph.store.memory import InMemoryStore
+    from composer.spec.context import SourceCode, WorkflowContext
+
+    ctx = WorkflowContext.create(
+        services=cast(Any, None),
+        thread_id="fallback-test",
+        store=InMemoryStore(),
+        recursion_limit=25,
+        cache_namespace=("fallback-test",),
+    )
+    source = SourceCode(
+        content=cast(Any, None),
+        project_root=str(tmp_path),
+        contract_name="River",
+        relative_path="src/River.sol",
+        forbidden_read="^$",
+    )
+    desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
+    desc.main_harness = _main_harness_contract()
+    desc.main_harness_plan = _plan()
+    return ctx, source, desc
+
+
+def _fake_autosetup(fail_for: set[str], calls: list[tuple[str, str]]):
+    from composer.spec.source.autosetup import SetupFailure, SetupSuccess
+
+    async def fake(project_root, relative_path, main_contract, prover_opts, *extra_files):
+        calls.append((relative_path, main_contract))
+        if main_contract in fail_for:
+            return SetupFailure(error=f"solc boom for {main_contract}", stderr="stderr text")
+        return SetupSuccess(
+            prover_config={"files": []},
+            summaries_path=f"certora/summaries/summaries-{main_contract}.spec",
+            user_types=[],
+        )
+
+    return fake
+
+
+@pytest.mark.asyncio
+async def test_autosetup_falls_back_to_raw_contract(tmp_path, monkeypatch):
+    import composer.spec.source.harness as harness_mod
+    from composer.prover.core import ProverOptions
+    from composer.spec.system_model import SourceApplication as App
+
+    ctx, source, desc = _fallback_fixture(tmp_path)
+    calls: list[tuple[str, str]] = []
+    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup({"RiverHarness"}, calls))
+
+    app = App(application_type="Staking", description="desc", components=[])
+    result = await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
+
+    # Harness attempt first, then the raw contract.
+    assert calls == [
+        ("certora/harnesses/RiverHarness.sol", "RiverHarness"),
+        ("src/River.sol", "River"),
+    ]
+    assert result.summaries_path.endswith("summaries-River.spec")
+    # The fallback clears the harness so every verify-target/prompt accessor reverts,
+    # and records the downgrade for the report.
+    assert desc.main_harness is None
+    assert desc.main_harness_plan is None
+    assert desc.verify_contract_name("River") == "River"
+    assert desc.main_harness_api() is None
+    assert desc.main_harness_fallback is not None
+    assert "RiverHarness" in desc.main_harness_fallback
+    assert "solc boom for RiverHarness" in desc.main_harness_fallback
+
+
+@pytest.mark.asyncio
+async def test_autosetup_harness_success_keeps_harness(tmp_path, monkeypatch):
+    import composer.spec.source.harness as harness_mod
+    from composer.prover.core import ProverOptions
+    from composer.spec.system_model import SourceApplication as App
+
+    ctx, source, desc = _fallback_fixture(tmp_path)
+    calls: list[tuple[str, str]] = []
+    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup(set(), calls))
+
+    app = App(application_type="Staking", description="desc", components=[])
+    result = await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
+
+    assert calls == [("certora/harnesses/RiverHarness.sol", "RiverHarness")]
+    assert result.summaries_path.endswith("summaries-RiverHarness.spec")
+    assert desc.main_harness is not None
+    assert desc.main_harness_fallback is None
+
+
+@pytest.mark.asyncio
+async def test_autosetup_raw_failure_still_raises(tmp_path, monkeypatch):
+    import composer.spec.source.harness as harness_mod
+    from composer.prover.core import ProverOptions
+    from composer.spec.system_model import SourceApplication as App
+
+    ctx, source, desc = _fallback_fixture(tmp_path)
+    # No harness: a raw-contract failure has nothing to fall back to.
+    desc.main_harness = None
+    desc.main_harness_plan = None
+    calls: list[tuple[str, str]] = []
+    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup({"River"}, calls))
+
+    app = App(application_type="Staking", description="desc", components=[])
+    with pytest.raises(RuntimeError, match="Auto setup failed"):
+        await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
+    assert calls == [("src/River.sol", "River")]
+
+
+@pytest.mark.asyncio
+async def test_autosetup_fallback_failure_raises_too(tmp_path, monkeypatch):
+    import composer.spec.source.harness as harness_mod
+    from composer.prover.core import ProverOptions
+    from composer.spec.system_model import SourceApplication as App
+
+    ctx, source, desc = _fallback_fixture(tmp_path)
+    calls: list[tuple[str, str]] = []
+    monkeypatch.setattr(
+        harness_mod, "run_autosetup", _fake_autosetup({"River", "RiverHarness"}, calls),
+    )
+
+    app = App(application_type="Staking", description="desc", components=[])
+    with pytest.raises(RuntimeError, match="Auto setup failed"):
+        await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
+    # Both attempts ran; the downgrade was still recorded before the final failure.
+    assert calls == [
+        ("certora/harnesses/RiverHarness.sol", "RiverHarness"),
+        ("src/River.sol", "River"),
+    ]
+    assert desc.main_harness_fallback is not None
+
+
+def test_system_description_fallback_field_backcompat():
+    desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
+    assert desc.main_harness_fallback is None
+
+
 @pytest.mark.parametrize("with_harness", [True, False])
 def test_structural_invariant_prompt_main_harness(with_harness: bool):
     view = MainHarnessView(

From e613d3691675e89b35396808c7418d488cdbb92a Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 02:55:57 +0300
Subject: [PATCH 10/13] Disclose the augmentation harness (and any fallback) in
 the report

AutoProverReport gains optional-with-default harness metadata: a
HarnessDisclosure (harness name/path, the protocol contract it extends, and
the getter/wrapper API lines) set when verification ran through a
main-contract augmentation harness, and main_harness_fallback carrying the
downgrade reason when the generated harness failed AutoSetup and the run
reverted to the raw contract. build_report and generate_all_component_cvl
thread both from the pipeline (post-fallback view), and the HTML render shows
a "Verified via" meta row, a "Verification harness" section listing the added
API, and a fallback warning. Persisted pre-change reports still validate.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/common_pipeline.py     |  9 ++-
 composer/spec/source/pipeline.py            | 14 ++++
 composer/spec/source/report/build.py        | 13 +++-
 composer/spec/source/report/schema.py       | 19 ++++++
 composer/templates/autoprove_report.html.j2 | 21 ++++++
 tests/test_autoprove_report.py              | 72 ++++++++++++++++++++-
 6 files changed, 144 insertions(+), 4 deletions(-)

diff --git a/composer/spec/source/common_pipeline.py b/composer/spec/source/common_pipeline.py
index 07d2f95..971dea9 100644
--- a/composer/spec/source/common_pipeline.py
+++ b/composer/spec/source/common_pipeline.py
@@ -31,6 +31,7 @@
 from composer.spec.source.report import build as report_build
 from composer.spec.source.report.build import build_report
 from composer.spec.source.report.collect import ReportComponentInput
+from composer.spec.source.report.schema import HarnessDisclosure
 from composer.spec.source.report_prover import make_prover_fetcher
 
 _log = logging.getLogger(__name__)
@@ -148,6 +149,8 @@ async def generate_all_component_cvl(
     semaphore: asyncio.Semaphore,
     invariant_result: tuple[list[PropertyFormulation], GeneratedCVL] | None = None,
     harness_api: list[str] | None = None,
+    main_harness: HarnessDisclosure | None = None,
+    main_harness_fallback: str | None = None,
 ) -> AutoProveResult:
     """Phase 6 — per-component CVL generation.
 
@@ -156,7 +159,9 @@ async def generate_all_component_cvl(
     the structural invariants assumed as preconditions must include
     ``invariants.spec`` in ``resources`` before calling. ``harness_api`` is the
     main-contract augmentation harness API (if any), surfaced to the authors
-    and the feedback judge.
+    and the feedback judge. ``main_harness`` / ``main_harness_fallback`` are the
+    report's harness disclosure: the augmentation harness verification ran
+    against, or the reason the run fell back to the raw contract.
     """
     async def _generate_batch(
         task_id: str,
@@ -259,6 +264,8 @@ async def _generate_and_write_batch(
                 components=report_components,
                 llm=env.llm_lite(),
                 fetch_verdicts=make_prover_fetcher(),
+                main_harness=main_harness,
+                main_harness_fallback=main_harness_fallback,
             ),
         )
         if report is not None:
diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py
index ad4e618..750852b 100644
--- a/composer/spec/source/pipeline.py
+++ b/composer/spec/source/pipeline.py
@@ -44,6 +44,7 @@
 from composer.spec.source.author import batch_cvl_generation, GaveUp
 from composer.spec.source.artifacts import InvariantSpec, ProverSourceCode
 from composer.spec.source.common_pipeline import extract_all_components, generate_all_component_cvl, AutoProveResult
+from composer.spec.source.report.schema import HarnessDisclosure
 from composer.spec.source.task_ids import (
     SYSTEM_ANALYSIS_TASK_ID, HARNESS_TASK_ID, AUTOSETUP_TASK_ID,
     SUMMARIES_TASK_ID, INVARIANTS_TASK_ID, INVARIANT_CVL_TASK_ID,
@@ -227,6 +228,17 @@ async def stream_bugs():
     # property authors and the feedback judge.
     harness_api = sys_desc.main_harness_api()
 
+    # Report disclosure: which augmentation harness verification ran against
+    # (post-fallback view), so the report never overstates what was directly
+    # verified.
+    harness_view = sys_desc.main_harness_view()
+    main_harness_disclosure = HarnessDisclosure(
+        name=harness_view.name,
+        path=harness_view.path,
+        harness_of=harness_view.harness_of,
+        api=harness_view.api,
+    ) if harness_view is not None else None
+
     # The prover tool is shared by every CVL-generation call below.
     prover_tool = get_prover_tool(
         env.llm_heavy(), verify_contract,
@@ -317,4 +329,6 @@ async def stream_bugs():
         semaphore=semaphore,
         invariant_result=invariant_result,
         harness_api=harness_api,
+        main_harness=main_harness_disclosure,
+        main_harness_fallback=sys_desc.main_harness_fallback,
     )
diff --git a/composer/spec/source/report/build.py b/composer/spec/source/report/build.py
index ab8d2fc..a0f25f7 100644
--- a/composer/spec/source/report/build.py
+++ b/composer/spec/source/report/build.py
@@ -20,7 +20,7 @@
     build_fallback_grouping, build_groups, call_grouping_llm,
 )
 from composer.spec.source.report.schema import (
-    AutoProverReport, Outcome, PropertyKey, ReportBackend, RuleRef,
+    AutoProverReport, HarnessDisclosure, Outcome, PropertyKey, ReportBackend, RuleRef,
 )
 
 _log = logging.getLogger(__name__)
@@ -42,8 +42,15 @@ async def build_report[R: ReportableResult](
     components: list[ReportComponentInput[R]],
     llm: BaseChatModel,
     fetch_verdicts: VerdictFetcher[R],
+    main_harness: HarnessDisclosure | None = None,
+    main_harness_fallback: str | None = None,
 ) -> AutoProverReport:
-    """Build and return the in-memory `AutoProverReport`. Persistence is the caller's job."""
+    """Build and return the in-memory `AutoProverReport`. Persistence is the caller's job.
+
+    ``main_harness`` discloses that verification ran through an augmentation harness;
+    ``main_harness_fallback`` discloses that a generated harness failed AutoSetup and
+    the run reverted to the raw contract. Both default to None for backends without
+    harness support."""
     properties, rules, skipped, gave_up, dropped = await collect(
         components, fetch_verdicts=fetch_verdicts
     )
@@ -95,5 +102,7 @@ async def build_report[R: ReportableResult](
         skipped=skipped,
         gave_up_components=gave_up,
         coverage=coverage,
+        main_harness=main_harness,
+        main_harness_fallback=main_harness_fallback,
     )
     return report
diff --git a/composer/spec/source/report/schema.py b/composer/spec/source/report/schema.py
index 68d5edb..a348d9c 100644
--- a/composer/spec/source/report/schema.py
+++ b/composer/spec/source/report/schema.py
@@ -155,6 +155,19 @@ class CoverageReport(BaseModel):
     warnings: list[str] = Field(default_factory=list)
 
 
+class HarnessDisclosure(BaseModel):
+    """Disclosure that verification ran against a main-contract augmentation harness rather than
+    the protocol contract directly. ``name``/``path`` identify the harness contract (the persisted
+    conf's verify target); ``harness_of`` is the protocol contract it extends (the report's primary
+    ``contract_name``); ``api`` lists the getters/wrappers the harness adds (the prompt-facing
+    one-liners), so a report consumer can reconcile the conf's contract name with the report's and
+    see exactly which entry points were added for verification."""
+    name: str
+    path: str
+    harness_of: str
+    api: list[str] = Field(default_factory=list)
+
+
 type ReportBackend = Literal["prover", "foundry"]
 """Which pipeline produced this report. Provenance only — every backend fills the same fields;
 this tag just lets the renderer pick the right outcome labels ("Verified" vs "Successful test")
@@ -176,3 +189,9 @@ class AutoProverReport(BaseModel):
     skipped: list[SkippedClaim] = Field(default_factory=list)
     gave_up_components: list[GaveUpComponent] = Field(default_factory=list)
     coverage: CoverageReport
+    #: Present when verification ran through a main-contract augmentation harness.
+    #: Optional-with-default so persisted pre-change reports still validate.
+    main_harness: HarnessDisclosure | None = None
+    #: Set when a generated augmentation harness failed AutoSetup and the run fell back to
+    #: verifying the raw contract — the downgrade is disclosed rather than silent.
+    main_harness_fallback: str | None = None
diff --git a/composer/templates/autoprove_report.html.j2 b/composer/templates/autoprove_report.html.j2
index 4864cbf..b7d2727 100644
--- a/composer/templates/autoprove_report.html.j2
+++ b/composer/templates/autoprove_report.html.j2
@@ -216,6 +216,9 @@ footer.report-foot {
   </div>
   <dl class="meta-grid">
     <dt>Contract</dt><dd>{{ report.contract_name }}</dd>
+    {%- if report.main_harness %}
+    <dt>Verified via</dt><dd>{{ report.main_harness.name }} (augmentation harness extending {{ report.main_harness.harness_of }})</dd>
+    {%- endif %}
     <dt>Run timestamp</dt><dd>{{ report.run_timestamp_utc or "—" }}</dd>
     {%- if has_links %}
     <dt>Prover runs</dt>
@@ -247,6 +250,24 @@ footer.report-foot {
 </div>
 {%- endif %}
 
+{%- if report.main_harness_fallback %}
+<div class="warnings"><strong>Harness fallback:</strong> {{ report.main_harness_fallback }}</div>
+{%- endif %}
+
+{%- if report.main_harness %}
+<section class="gaps">
+  <h2>Verification harness</h2>
+  <p>Verification ran against <code>{{ report.main_harness.name }}</code>
+  (<code>{{ report.main_harness.path }}</code>), an augmentation harness extending
+  <code>{{ report.main_harness.harness_of }}</code> with the following verification-only
+  getters/wrappers. Universal claims proven over the harness also hold for
+  <code>{{ report.main_harness.harness_of }}</code>; the added entry points exist only for verification.</p>
+  <ul class="claims">
+    {%- for line in report.main_harness.api %}<li>{{ line }}</li>{% endfor %}
+  </ul>
+</section>
+{%- endif %}
+
 {%- for g in groups %}
 <section class="prop" id="{{ g.slug }}">
   <h2><span class="id">{{ g.slug }}</span> {{ g.title }} <span class="badge badge-{{ g.kind }}">{{ g.label }}</span></h2>
diff --git a/tests/test_autoprove_report.py b/tests/test_autoprove_report.py
index b16f271..2934453 100644
--- a/tests/test_autoprove_report.py
+++ b/tests/test_autoprove_report.py
@@ -33,7 +33,7 @@
 from composer.spec.source.report.render import render_html
 from composer.spec.source.report.schema import (
     AutoProverReport, CoverageReport, FormalizedProperty, GaveUpComponent, GroupStatus,
-    Outcome, PropertyGroup, RuleVerdict, SkippedClaim,
+    HarnessDisclosure, Outcome, PropertyGroup, RuleVerdict, SkippedClaim,
 )
 from composer.spec.source.report_prover import make_prover_fetcher
 
@@ -423,6 +423,52 @@ def test_render_html_omits_link_column_without_links():
     assert "Prover runs" not in h
 
 
+def _harness_disclosure() -> HarnessDisclosure:
+    return HarnessDisclosure(
+        name="CounterHarness",
+        path="certora/harnesses/CounterHarness.sol",
+        harness_of="Counter",
+        api=["`getShadowSlot()` returns (`uint256`) — reads the shadow slot"],
+    )
+
+
+def test_render_html_discloses_main_harness():
+    report = _mini_report().model_copy(update={"main_harness": _harness_disclosure()})
+    h = render_html(report)
+    assert "Verification harness" in h
+    assert "CounterHarness" in h
+    assert "certora/harnesses/CounterHarness.sol" in h
+    assert "getShadowSlot" in h
+    # Header meta row reconciles the conf's verify target with the report's contract.
+    assert "Verified via" in h
+    assert "augmentation harness extending" in h
+
+
+def test_render_html_omits_harness_section_without_harness():
+    h = render_html(_mini_report())
+    assert "Verification harness" not in h
+    assert "Verified via" not in h
+    assert "Harness fallback" not in h
+
+
+def test_render_html_discloses_harness_fallback():
+    report = _mini_report().model_copy(update={
+        "main_harness_fallback": "AutoSetup failed for the augmentation harness CounterHarness",
+    })
+    h = render_html(report)
+    assert "Harness fallback:" in h
+    assert "AutoSetup failed for the augmentation harness CounterHarness" in h
+
+
+def test_report_schema_harness_fields_backcompat():
+    # A persisted pre-change report (no harness keys) still validates, with both
+    # disclosure fields defaulting to None.
+    dumped = _mini_report().model_dump(exclude={"main_harness", "main_harness_fallback"})
+    reloaded = AutoProverReport.model_validate(dumped)
+    assert reloaded.main_harness is None
+    assert reloaded.main_harness_fallback is None
+
+
 # ---------------------------------------------------------------------------
 # build orchestrator (async)
 # ---------------------------------------------------------------------------
@@ -454,6 +500,30 @@ async def test_build_groups_properties(tmp_path):
     assert [g.slug for g in report.groups] == ["g"]
     assert {p.title for p in report.properties} == {"p1", "p2"}
     assert report.coverage.property_coverage_complete is True
+    # Without a harness the disclosure fields stay None.
+    assert report.main_harness is None
+    assert report.main_harness_fallback is None
+
+
+@pytest.mark.asyncio
+async def test_build_threads_harness_disclosure(tmp_path):
+    gen = _gen({"p1": ["r1"]})
+    fetch = _fetcher({"L1": [_fake_check("r1", NodeStatus.VERIFIED)]})
+    llm = _GroupingStubModel(result=GroupingResult(groups=[PropertyGroupDraft(
+        slug="g", title="G", description="d", members=[("C", "p1")])]))
+
+    report = await build.build_report(
+        contract_name="Counter",
+        backend="prover",
+        components=[_input("C", "autospec_C.spec", [_prop("p1", "d1")], gen)],
+        llm=llm, fetch_verdicts=fetch,
+        main_harness=_harness_disclosure(),
+        main_harness_fallback="fell back",
+    )
+
+    assert report.main_harness is not None
+    assert report.main_harness.name == "CounterHarness"
+    assert report.main_harness_fallback == "fell back"
 
 
 @pytest.mark.asyncio

From 5735392bdedc87aca6950fb1d71d5f2b9986a7db Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 02:57:00 +0300
Subject: [PATCH 11/13] Drop dead ProverArtifactStore field; require
 source-cited slot derivations
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

ProverArtifactStore only ever consumed main_contract as the verify-target
default, so the stored _main_contract attribute goes away. The state-analysis
step 6 (and the UnstructuredSlotSpec schema) now require the slot derivation
to quote the exact source expression with a file:line citation rather than a
paraphrase — a mis-transcribed slot constant compiles fine and silently
verifies storage the contract never touches.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/artifacts.py    | 4 ++--
 composer/spec/source/harness.py      | 6 ++++--
 composer/templates/state_analysis.j2 | 4 ++++
 tests/test_main_harness.py           | 3 +++
 4 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py
index 74fa14d..72ff010 100644
--- a/composer/spec/source/artifacts.py
+++ b/composer/spec/source/artifacts.py
@@ -71,10 +71,10 @@ class ProverArtifactStore(ArtifactStore):
 
     def __init__(self, project_root: str, main_contract: str, verify_contract: str | None = None):
         super().__init__(project_root)
-        self._main_contract = main_contract
         # The contract identifier the prover verifies: the main-harness identifier
         # when the run verifies through an augmentation harness, otherwise the main
-        # contract itself.
+        # contract itself. ``main_contract`` (the protocol name) only serves as that
+        # default — the store's outputs (conf dumps) all name the verify target.
         self._verify_contract = verify_contract or main_contract
 
     def _deliverable_dir(self) -> Path:
diff --git a/composer/spec/source/harness.py b/composer/spec/source/harness.py
index 85d6be0..fdfa5c6 100644
--- a/composer/spec/source/harness.py
+++ b/composer/spec/source/harness.py
@@ -89,8 +89,10 @@ class UnstructuredSlotSpec(BaseModel):
     """
     getter_name: str = Field(description="The name of the external view getter the harness should expose for this slot")
     slot_derivation: str = Field(description=(
-        "How the storage slot is derived: the keccak preimage or namespace string "
-        "(e.g. `keccak256(\"river.state.balance\") - 1` or the ERC-7201 namespace id)"
+        "How the storage slot is derived: quote the exact source expression computing "
+        "the slot, with a file:line citation — never a paraphrase "
+        "(e.g. `keccak256(\"river.state.balance\") - 1` — src/State.sol:42, or the "
+        "ERC-7201 namespace id as written in the source)"
     ))
     value_type: str = Field(description="The Solidity type of the value read from the slot (e.g. `uint256`, `address`)")
     rationale: str = Field(description="One line: why verification needs to observe this state")
diff --git a/composer/templates/state_analysis.j2 b/composer/templates/state_analysis.j2
index e2e7a64..b305466 100644
--- a/composer/templates/state_analysis.j2
+++ b/composer/templates/state_analysis.j2
@@ -193,6 +193,10 @@ b. Monolithic external functions that are long sequences of internal-helper call
 If either applies, propose a "main contract harness plan" (the `main_contract_harness` field of your result):
 * For each flagged storage location: the desired getter name, the slot derivation (the keccak preimage or
   namespace string), the Solidity type of the value read from the slot, and a one-line rationale.
+  **IMPORTANT**: the slot derivation must QUOTE the exact source expression that derives the slot, with a
+  `file:line` citation (e.g. `keccak256("river.state.balance") - 1` — src/State.sol:42) — never a paraphrase
+  or a re-derivation from memory. A mis-transcribed slot constant compiles fine and silently "verifies"
+  properties about storage the contract never touches.
 * For each monolithic function: the thin helper wrappers to expose (name plus a one-line behavioral contract
   for each) and a rationale.
 
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index 7e67991..de0ee28 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -202,6 +202,9 @@ def test_state_analysis_renders_main_harness_step():
     )
     assert "main_contract_harness" in out
     assert "ERC-7201" in out
+    # Slot derivations must be source citations, not paraphrases.
+    assert "QUOTE the exact source expression" in out
+    assert "`file:line` citation" in out
 
 
 @pytest.mark.parametrize("with_api", [True, False])

From 595da5709ca2ff56043fd2bff95efe7ee26aa339 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 03:31:15 +0300
Subject: [PATCH 12/13] Type the main-harness test fixtures so pyright is clean
 on tests too

SolidityIdentifier is a checker-only str subtype, so the fixture literals
need the constructor idiom, and the judge-bind injection needs a real
PropertyFormulation rather than a duck-typed stub.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 tests/test_main_harness.py | 36 ++++++++++++++++++++++--------------
 1 file changed, 22 insertions(+), 14 deletions(-)

diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index de0ee28..0e86b81 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -22,8 +22,13 @@
     empty_main_harness_plan_error,
     main_harness_path_error,
 )
+from composer.spec.prop import PropertyFormulation
 from composer.spec.source.report.schema import GaveUpComponent
-from composer.spec.system_model import HarnessedApplication, SourceApplication
+from composer.spec.system_model import (
+    HarnessedApplication,
+    SolidityIdentifier,
+    SourceApplication,
+)
 from composer.templates.loader import load_jinja_template
 
 
@@ -63,10 +68,10 @@ def _plan() -> MainHarnessPlan:
 
 def _main_harness_contract() -> HarnessedContract:
     return HarnessedContract(
-        solidity_identifier="RiverHarness",
+        solidity_identifier=SolidityIdentifier("RiverHarness"),
         link_fields=[],
         harness_definition=HarnessDef(
-            harness_of="River",
+            harness_of=SolidityIdentifier("River"),
             harness_source="contract RiverHarness is River {}",
         ),
         path="certora/harnesses/RiverHarness.sol",
@@ -167,10 +172,13 @@ def test_main_harness_delivery_confined_to_harness_dir():
 # Template rendering
 # ---------------------------------------------------------------------------
 
-class _Prop:
-    sort = "safety"
-    title = "version_is_monotone"
-    description = "the version never decreases"
+def _prop() -> PropertyFormulation:
+    return PropertyFormulation(
+        title="version_is_monotone",
+        methods="invariant",
+        sort="safety_property",
+        description="the version never decreases",
+    )
 
 
 class _Spec:
@@ -212,7 +220,7 @@ def test_property_generation_prompt_harness_api(with_api: bool):
     api = _plan().api_lines() if with_api else None
     out = load_jinja_template(
         "property_generation_prompt.j2",
-        properties=[_Prop()],
+        properties=[_prop()],
         contract_name="River",
         resources=[],
         context=None,
@@ -230,7 +238,7 @@ def test_property_generation_prompt_harness_api(with_api: bool):
 def test_property_judge_prompt_harness_api():
     out = load_jinja_template(
         "property_judge_prompt.j2",
-        properties=[_Prop()],
+        properties=[_prop()],
         sort="existing",
         context=None,
         harness_api=_plan().api_lines(),
@@ -246,7 +254,7 @@ def test_property_judge_prompt_harness_api():
     # Binding without harness_api at all (the NotRequired key) renders harness-free.
     out = load_jinja_template(
         "property_judge_prompt.j2",
-        properties=[_Prop()],
+        properties=[_prop()],
         sort="existing",
         context=None,
     )
@@ -283,7 +291,7 @@ def test_harness_augmentation_reaches_both_judge_binds(flag: bool):
     task_bind = _bind_harness_augmentation(
         FeedbackTemplate.bind({
             "sort": "existing", "context": None, "harness_api": _plan().api_lines() if flag else None,
-        }).depends(Properties).inject({"properties": [_Prop()]}),
+        }).depends(Properties).inject({"properties": [_prop()]}),
         flag,
     )
     assert task_bind.args["harness_augmentation"] is flag
@@ -312,7 +320,7 @@ def _fallback_fixture(tmp_path):
     source = SourceCode(
         content=cast(Any, None),
         project_root=str(tmp_path),
-        contract_name="River",
+        contract_name=SolidityIdentifier("River"),
         relative_path="src/River.sol",
         forbidden_read="^$",
     )
@@ -437,9 +445,9 @@ def test_system_description_fallback_field_backcompat():
 @pytest.mark.parametrize("with_harness", [True, False])
 def test_structural_invariant_prompt_main_harness(with_harness: bool):
     view = MainHarnessView(
-        name="RiverHarness",
+        name=SolidityIdentifier("RiverHarness"),
         path="certora/harnesses/RiverHarness.sol",
-        harness_of="River",
+        harness_of=SolidityIdentifier("River"),
         api=_plan().api_lines(),
     ) if with_harness else None
     app = HarnessedApplication(application_type="Staking", description="desc", components=[])

From 09ddc2fd29795f2ea6e8f75f29e7da41b901a126 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sat, 4 Jul 2026 18:24:09 +0300
Subject: [PATCH 13/13] Use a neutral contract name in harness examples and
 test fixtures

Illustrative slot derivations and fixtures now use a generic Vault
contract rather than names tied to any specific engagement.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 composer/spec/source/harness.py      |  2 +-
 composer/templates/state_analysis.j2 |  2 +-
 tests/test_main_harness.py           | 86 ++++++++++++++--------------
 3 files changed, 45 insertions(+), 45 deletions(-)

diff --git a/composer/spec/source/harness.py b/composer/spec/source/harness.py
index fdfa5c6..0c94228 100644
--- a/composer/spec/source/harness.py
+++ b/composer/spec/source/harness.py
@@ -91,7 +91,7 @@ class UnstructuredSlotSpec(BaseModel):
     slot_derivation: str = Field(description=(
         "How the storage slot is derived: quote the exact source expression computing "
         "the slot, with a file:line citation — never a paraphrase "
-        "(e.g. `keccak256(\"river.state.balance\") - 1` — src/State.sol:42, or the "
+        "(e.g. `keccak256(\"vault.state.balance\") - 1` — src/State.sol:42, or the "
         "ERC-7201 namespace id as written in the source)"
     ))
     value_type: str = Field(description="The Solidity type of the value read from the slot (e.g. `uint256`, `address`)")
diff --git a/composer/templates/state_analysis.j2 b/composer/templates/state_analysis.j2
index b305466..16c7c47 100644
--- a/composer/templates/state_analysis.j2
+++ b/composer/templates/state_analysis.j2
@@ -194,7 +194,7 @@ If either applies, propose a "main contract harness plan" (the `main_contract_ha
 * For each flagged storage location: the desired getter name, the slot derivation (the keccak preimage or
   namespace string), the Solidity type of the value read from the slot, and a one-line rationale.
   **IMPORTANT**: the slot derivation must QUOTE the exact source expression that derives the slot, with a
-  `file:line` citation (e.g. `keccak256("river.state.balance") - 1` — src/State.sol:42) — never a paraphrase
+  `file:line` citation (e.g. `keccak256("vault.state.balance") - 1` — src/State.sol:42) — never a paraphrase
   or a re-derivation from memory. A mis-transcribed slot constant compiles fine and silently "verifies"
   properties about storage the contract never touches.
 * For each monolithic function: the thin helper wrappers to expose (name plus a one-line behavioral contract
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
index 0e86b81..af33243 100644
--- a/tests/test_main_harness.py
+++ b/tests/test_main_harness.py
@@ -51,7 +51,7 @@ def _plan() -> MainHarnessPlan:
         unstructured_slots=[
             UnstructuredSlotSpec(
                 getter_name="getVersionSlot",
-                slot_derivation='keccak256("river.state.version") - 1',
+                slot_derivation='keccak256("vault.state.version") - 1',
                 value_type="uint256",
                 rationale="version invariants need to observe it",
             )
@@ -68,13 +68,13 @@ def _plan() -> MainHarnessPlan:
 
 def _main_harness_contract() -> HarnessedContract:
     return HarnessedContract(
-        solidity_identifier=SolidityIdentifier("RiverHarness"),
+        solidity_identifier=SolidityIdentifier("VaultHarness"),
         link_fields=[],
         harness_definition=HarnessDef(
-            harness_of=SolidityIdentifier("River"),
-            harness_source="contract RiverHarness is River {}",
+            harness_of=SolidityIdentifier("Vault"),
+            harness_source="contract VaultHarness is Vault {}",
         ),
-        path="certora/harnesses/RiverHarness.sol",
+        path="certora/harnesses/VaultHarness.sol",
     )
 
 
@@ -117,16 +117,16 @@ def test_gave_up_component_backcompat():
 
 def test_verify_contract_name_defaults_to_main_contract():
     desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
-    assert desc.verify_contract_name("River") == "River"
-    assert desc.verify_contract_path("src/River.sol") == "src/River.sol"
+    assert desc.verify_contract_name("Vault") == "Vault"
+    assert desc.verify_contract_path("src/Vault.sol") == "src/Vault.sol"
 
 
 def test_verify_contract_name_prefers_main_harness():
     desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
     desc.main_harness = _main_harness_contract()
     desc.main_harness_plan = _plan()
-    assert desc.verify_contract_name("River") == "RiverHarness"
-    assert desc.verify_contract_path("src/River.sol") == "certora/harnesses/RiverHarness.sol"
+    assert desc.verify_contract_name("Vault") == "VaultHarness"
+    assert desc.verify_contract_path("src/Vault.sol") == "certora/harnesses/VaultHarness.sol"
 
 
 def test_main_harness_api_and_view():
@@ -143,8 +143,8 @@ def test_main_harness_api_and_view():
 
     view = desc.main_harness_view()
     assert view is not None
-    assert view.name == "RiverHarness"
-    assert view.harness_of == "River"
+    assert view.name == "VaultHarness"
+    assert view.harness_of == "Vault"
     assert view.api == api
 
 
@@ -162,8 +162,8 @@ def test_classifier_rejects_empty_harness_plan():
 def test_main_harness_delivery_confined_to_harness_dir():
     # The generation validator must reject deliveries outside certora/harnesses/
     # (write confinement alone doesn't stop delivering a pre-existing project file).
-    assert main_harness_path_error("certora/harnesses/RiverHarness.sol") is None
-    err = main_harness_path_error("src/River.sol")
+    assert main_harness_path_error("certora/harnesses/VaultHarness.sol") is None
+    err = main_harness_path_error("src/Vault.sol")
     assert err is not None
     assert "certora/harnesses" in err
 
@@ -182,30 +182,30 @@ def _prop() -> PropertyFormulation:
 
 
 class _Spec:
-    contract_name = "River"
-    relative_path = "src/River.sol"
+    contract_name = "Vault"
+    relative_path = "src/Vault.sol"
 
 
 def test_main_harness_generation_prompt_renders():
     out = load_jinja_template(
         "main_harness_generation_prompt.j2",
-        contract_name="River",
-        relative_path="src/River.sol",
-        harness_name="RiverHarness",
+        contract_name="Vault",
+        relative_path="src/Vault.sol",
+        harness_name="VaultHarness",
         plan=_plan(),
     )
-    assert "contract RiverHarness is River" in out
+    assert "contract VaultHarness is Vault" in out
     assert "getVersionSlot" in out
     assert "helperDeposit" in out
-    assert "certora/harnesses/RiverHarness.sol" in out
+    assert "certora/harnesses/VaultHarness.sol" in out
 
 
 def test_state_analysis_renders_main_harness_step():
     app = SourceApplication(application_type="Staking", description="desc", components=[])
     out = load_jinja_template(
         "state_analysis.j2",
-        contract_name="River",
-        relative_path="src/River.sol",
+        contract_name="Vault",
+        relative_path="src/Vault.sol",
         context=app,
     )
     assert "main_contract_harness" in out
@@ -221,7 +221,7 @@ def test_property_generation_prompt_harness_api(with_api: bool):
     out = load_jinja_template(
         "property_generation_prompt.j2",
         properties=[_prop()],
-        contract_name="River",
+        contract_name="Vault",
         resources=[],
         context=None,
         harness_api=api,
@@ -320,8 +320,8 @@ def _fallback_fixture(tmp_path):
     source = SourceCode(
         content=cast(Any, None),
         project_root=str(tmp_path),
-        contract_name=SolidityIdentifier("River"),
-        relative_path="src/River.sol",
+        contract_name=SolidityIdentifier("Vault"),
+        relative_path="src/Vault.sol",
         forbidden_read="^$",
     )
     desc = SystemDescriptionHarnessed.model_validate(_base_description_fields())
@@ -354,26 +354,26 @@ async def test_autosetup_falls_back_to_raw_contract(tmp_path, monkeypatch):
 
     ctx, source, desc = _fallback_fixture(tmp_path)
     calls: list[tuple[str, str]] = []
-    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup({"RiverHarness"}, calls))
+    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup({"VaultHarness"}, calls))
 
     app = App(application_type="Staking", description="desc", components=[])
     result = await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
 
     # Harness attempt first, then the raw contract.
     assert calls == [
-        ("certora/harnesses/RiverHarness.sol", "RiverHarness"),
-        ("src/River.sol", "River"),
+        ("certora/harnesses/VaultHarness.sol", "VaultHarness"),
+        ("src/Vault.sol", "Vault"),
     ]
-    assert result.summaries_path.endswith("summaries-River.spec")
+    assert result.summaries_path.endswith("summaries-Vault.spec")
     # The fallback clears the harness so every verify-target/prompt accessor reverts,
     # and records the downgrade for the report.
     assert desc.main_harness is None
     assert desc.main_harness_plan is None
-    assert desc.verify_contract_name("River") == "River"
+    assert desc.verify_contract_name("Vault") == "Vault"
     assert desc.main_harness_api() is None
     assert desc.main_harness_fallback is not None
-    assert "RiverHarness" in desc.main_harness_fallback
-    assert "solc boom for RiverHarness" in desc.main_harness_fallback
+    assert "VaultHarness" in desc.main_harness_fallback
+    assert "solc boom for VaultHarness" in desc.main_harness_fallback
 
 
 @pytest.mark.asyncio
@@ -389,8 +389,8 @@ async def test_autosetup_harness_success_keeps_harness(tmp_path, monkeypatch):
     app = App(application_type="Staking", description="desc", components=[])
     result = await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
 
-    assert calls == [("certora/harnesses/RiverHarness.sol", "RiverHarness")]
-    assert result.summaries_path.endswith("summaries-RiverHarness.spec")
+    assert calls == [("certora/harnesses/VaultHarness.sol", "VaultHarness")]
+    assert result.summaries_path.endswith("summaries-VaultHarness.spec")
     assert desc.main_harness is not None
     assert desc.main_harness_fallback is None
 
@@ -406,12 +406,12 @@ async def test_autosetup_raw_failure_still_raises(tmp_path, monkeypatch):
     desc.main_harness = None
     desc.main_harness_plan = None
     calls: list[tuple[str, str]] = []
-    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup({"River"}, calls))
+    monkeypatch.setattr(harness_mod, "run_autosetup", _fake_autosetup({"Vault"}, calls))
 
     app = App(application_type="Staking", description="desc", components=[])
     with pytest.raises(RuntimeError, match="Auto setup failed"):
         await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
-    assert calls == [("src/River.sol", "River")]
+    assert calls == [("src/Vault.sol", "Vault")]
 
 
 @pytest.mark.asyncio
@@ -423,7 +423,7 @@ async def test_autosetup_fallback_failure_raises_too(tmp_path, monkeypatch):
     ctx, source, desc = _fallback_fixture(tmp_path)
     calls: list[tuple[str, str]] = []
     monkeypatch.setattr(
-        harness_mod, "run_autosetup", _fake_autosetup({"River", "RiverHarness"}, calls),
+        harness_mod, "run_autosetup", _fake_autosetup({"Vault", "VaultHarness"}, calls),
     )
 
     app = App(application_type="Staking", description="desc", components=[])
@@ -431,8 +431,8 @@ async def test_autosetup_fallback_failure_raises_too(tmp_path, monkeypatch):
         await harness_mod.run_autosetup_phase(ctx, source, desc, app, ProverOptions())
     # Both attempts ran; the downgrade was still recorded before the final failure.
     assert calls == [
-        ("certora/harnesses/RiverHarness.sol", "RiverHarness"),
-        ("src/River.sol", "River"),
+        ("certora/harnesses/VaultHarness.sol", "VaultHarness"),
+        ("src/Vault.sol", "Vault"),
     ]
     assert desc.main_harness_fallback is not None
 
@@ -445,9 +445,9 @@ def test_system_description_fallback_field_backcompat():
 @pytest.mark.parametrize("with_harness", [True, False])
 def test_structural_invariant_prompt_main_harness(with_harness: bool):
     view = MainHarnessView(
-        name=SolidityIdentifier("RiverHarness"),
-        path="certora/harnesses/RiverHarness.sol",
-        harness_of=SolidityIdentifier("River"),
+        name=SolidityIdentifier("VaultHarness"),
+        path="certora/harnesses/VaultHarness.sol",
+        harness_of=SolidityIdentifier("Vault"),
         api=_plan().api_lines(),
     ) if with_harness else None
     app = HarnessedApplication(application_type="Staking", description="desc", components=[])
@@ -457,7 +457,7 @@ def test_structural_invariant_prompt_main_harness(with_harness: bool):
         contract_spec=_Spec(),
         main_harness=view,
     )
-    assert ("RiverHarness" in out) == with_harness
+    assert ("VaultHarness" in out) == with_harness
     assert ("getVersionSlot" in out) == with_harness
     # The shared harnessed context carries the parametric/witness caveat, so the
     # invariant formulator sees the same soundness guardrails as the CVL author.