diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py
index 5f64d7b..a03cab1 100644
--- a/composer/spec/feedback.py
+++ b/composer/spec/feedback.py
@@ -41,6 +41,9 @@ 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")
 
@@ -53,18 +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,
 ) -> FeedbackToolContext:
 
     if system_prompt is None:
         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
@@ -88,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/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py
index ae46480..72ff010 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. ``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:
         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..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__)
@@ -147,13 +148,20 @@ 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,
+    main_harness: HarnessDisclosure | None = None,
+    main_harness_fallback: 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. ``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,
@@ -182,6 +190,7 @@ async def _generate_batch(
                 description=label,
                 source=source_input,
                 spec_dir=SPECS_DIR,
+                harness_api=harness_api,
             ),
             semaphore,
         )
@@ -234,6 +243,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
@@ -254,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:
@@ -270,7 +282,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/harness.py b/composer/spec/source/harness.py
index c98ac4e..0c94228 100644
--- a/composer/spec/source/harness.py
+++ b/composer/spec/source/harness.py
@@ -81,6 +81,86 @@ 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: quote the exact source expression computing "
+        "the slot, with a file:line citation — never a paraphrase "
+        "(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`)")
+    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
+
+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."""
+    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 +183,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 +204,46 @@ 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
+    # 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
+        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 +297,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 (plan_error := empty_main_harness_plan_error(res.main_contract_harness)) is not None:
+            return plan_error
         return None
 
     d = bind_standard(
@@ -370,6 +499,129 @@ 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 (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
+
+    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 +746,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 +783,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 +826,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)
     )
 
 
@@ -566,47 +853,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``."""
     config_ctxt = context.child(config_key)
-    cache = await config_ctxt.child(
-        autosetup_key(application_desc, prover_opts),
-        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),
-        source.relative_path,
-        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 5799f16..750852b 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,
@@ -43,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,
@@ -139,12 +141,13 @@ async def run_autoprove_pipeline(
         components=comp
     )
 
-    # 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,
-        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):
@@ -186,7 +189,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=pre_fallback_harness_view,
+            ),
         )
 
     async def stream_bugs():
@@ -211,6 +217,34 @@ 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()
+
+    # 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,
+        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.
@@ -255,6 +289,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 +328,7 @@ async def stream_bugs():
         resources=resources,
         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/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/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/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/report/schema.py b/composer/spec/source/report/schema.py
index 3fb6a4f..a348d9c 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):
@@ -151,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")
@@ -172,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/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(
diff --git a/composer/templates/autoprove_report.html.j2 b/composer/templates/autoprove_report.html.j2
index 894c6c9..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>
@@ -298,7 +319,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>
diff --git a/composer/templates/harnessed_application_context.j2 b/composer/templates/harnessed_application_context.j2
index 6ffc272..fc54aa3 100644
--- a/composer/templates/harnessed_application_context.j2
+++ b/composer/templates/harnessed_application_context.j2
@@ -8,3 +8,17 @@ 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 %}
+
+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/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/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2
index d96585c..d6a10ab 100644
--- a/composer/templates/property_generation_prompt.j2
+++ b/composer/templates/property_generation_prompt.j2
@@ -161,6 +161,47 @@ 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.
+
+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 %}
+
 <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..1316ab8 100644
--- a/composer/templates/property_judge_prompt.j2
+++ b/composer/templates/property_judge_prompt.j2
@@ -219,6 +219,38 @@ 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.
+
+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 %}
+
 <guidance>
 <hard_requirement>
 Do not provide ANY feedback except for the 7 criteria above.
diff --git a/composer/templates/state_analysis.j2 b/composer/templates/state_analysis.j2
index ca40a80..16c7c47 100644
--- a/composer/templates/state_analysis.j2
+++ b/composer/templates/state_analysis.j2
@@ -177,10 +177,40 @@ 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.
+  **IMPORTANT**: the slot derivation must QUOTE the exact source expression that derives the slot, with a
+  `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
+  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 +220,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.
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
diff --git a/tests/test_main_harness.py b/tests/test_main_harness.py
new file mode 100644
index 0000000..af33243
--- /dev/null
+++ b/tests/test_main_harness.py
@@ -0,0 +1,464 @@
+"""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,
+    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,
+    SolidityIdentifier,
+    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("vault.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=SolidityIdentifier("VaultHarness"),
+        link_fields=[],
+        harness_definition=HarnessDef(
+            harness_of=SolidityIdentifier("Vault"),
+            harness_source="contract VaultHarness is Vault {}",
+        ),
+        path="certora/harnesses/VaultHarness.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("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("Vault") == "VaultHarness"
+    assert desc.verify_contract_path("src/Vault.sol") == "certora/harnesses/VaultHarness.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 == "VaultHarness"
+    assert view.harness_of == "Vault"
+    assert view.api == api
+
+
+def test_classifier_rejects_empty_harness_plan():
+    # 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/VaultHarness.sol") is None
+    err = main_harness_path_error("src/Vault.sol")
+    assert err is not None
+    assert "certora/harnesses" in err
+
+
+# ---------------------------------------------------------------------------
+# Template rendering
+# ---------------------------------------------------------------------------
+
+def _prop() -> PropertyFormulation:
+    return PropertyFormulation(
+        title="version_is_monotone",
+        methods="invariant",
+        sort="safety_property",
+        description="the version never decreases",
+    )
+
+
+class _Spec:
+    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="Vault",
+        relative_path="src/Vault.sol",
+        harness_name="VaultHarness",
+        plan=_plan(),
+    )
+    assert "contract VaultHarness is Vault" in out
+    assert "getVersionSlot" in out
+    assert "helperDeposit" 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="Vault",
+        relative_path="src/Vault.sol",
+        context=app,
+    )
+    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])
+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="Vault",
+        resources=[],
+        context=None,
+        harness_api=api,
+    )
+    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():
+    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
+    # 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",
+        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("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)
+
+
+# ---------------------------------------------------------------------------
+# 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=SolidityIdentifier("Vault"),
+        relative_path="src/Vault.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({"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/VaultHarness.sol", "VaultHarness"),
+        ("src/Vault.sol", "Vault"),
+    ]
+    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("Vault") == "Vault"
+    assert desc.main_harness_api() is None
+    assert desc.main_harness_fallback is not None
+    assert "VaultHarness" in desc.main_harness_fallback
+    assert "solc boom for VaultHarness" 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/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
+
+
+@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({"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/Vault.sol", "Vault")]
+
+
+@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({"Vault", "VaultHarness"}, 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/VaultHarness.sol", "VaultHarness"),
+        ("src/Vault.sol", "Vault"),
+    ]
+    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(
+        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=[])
+    out = load_jinja_template(
+        "structural_invariant_prompt.j2",
+        context=app,
+        contract_spec=_Spec(),
+        main_harness=view,
+    )
+    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.
+    assert ("never use a helper as the witness" in out) == with_harness