Add findings to the report

composer/pipeline/core.py

@@ -36,7 +36,7 @@
 from composer.spec.util import string_hash
 from composer.input.files import Document
 from composer.spec.source.report.build import build_report
-from composer.spec.source.report.collect import ReportComponentInput, Verdict
+from composer.spec.source.report.collect import ReportComponentInput, RuleEvidence, Verdict
 from composer.spec.source.report.schema import RuleName, ReportBackend
 from composer.spec.source.report import build as report_build
 from composer.spec.source.task_ids import SYSTEM_ANALYSIS_TASK_ID, REPORT_TASK_ID
@@ -55,7 +55,7 @@ class Formalizer[FormT: BackendResult](ABC):
     state — never set post-hoc. `FormT: ReportableResult` is what makes the report a core step."""
     formalized_type: type[FormT]
     backend_tag: ReportBackend
-    
+
     @abstractmethod
     async def formalize(
         self,
@@ -77,6 +77,11 @@ async def fetch_verdicts(self, inp: ReportComponentInput[FormT]) -> dict[RuleNam
         off-thread. Foundry: read straight off inp.formalized.result."""
         ...
 
+    async def fetch_evidence(self, link: str | None, rule_name: str) -> RuleEvidence | None:
+        """Per-violated-rule evidence for findings synthesis — the prover returns its captured
+        counterexample analysis for `rule_name`. Default: none (backend produces no findings)."""
+        return None
+
     async def finalize(self, outcomes: list[ComponentOutcome[FormT]], run: PipelineRun) -> None:
         """Emit any backend-specific run-level artifacts from the full outcome set (prover:
         components_to_prover_runs.json). Default: none."""
@@ -209,7 +214,7 @@ async def _run(batch: _Batch) -> ComponentOutcome[FormT]:
                 await child.cache_put(result)
         else:
             result = cached_result
-        
+
         outcome: Delivered[FormT] | GaveUp = (
             result if isinstance(result, GaveUp)
             else Delivered(result, backend.artifact_store.write_artifact(result_key, result))
@@ -239,6 +244,8 @@ async def _run(batch: _Batch) -> ComponentOutcome[FormT]:
             job=lambda: build_report(
                 contract_name=source.contract_name, backend=formalizer.backend_tag,
                 components=inputs, llm=run.env.llm_lite(), fetch_verdicts=formalizer.fetch_verdicts,
+                findings_llm=run.env.llm_heavy(),
+                fetch_evidence=formalizer.fetch_evidence,
             ),
             task_info=TaskInfo(REPORT_TASK_ID, label="Report Extraction", phase=backend.core_phases["report"])
         )

composer/spec/source/autoprove_common.py

@@ -20,6 +20,7 @@
 )
 from composer.pipeline.cli import cli_pipeline, user_ns
 from composer.spec.source.pipeline import ProverBackend, GeneratedCVL
+from composer.spec.source.cex_capture import CexAnalysisStore
 from composer.prover.core import make_prover_options
 from composer.spec.source.source_env import build_source_env
 from composer.spec.source.artifacts import ProverArtifactStore
@@ -144,7 +145,8 @@ async def callback(
             )
             backend = ProverBackend(
                 ProverArtifactStore(staged.source.project_root, staged.source.contract_name),
-                make_prover_options(cloud=args.cloud)
+                make_prover_options(cloud=args.cloud),
+                CexAnalysisStore(),
             )
             return await cont(source_env, backend)
     yield callback

composer/spec/source/cex_capture.py

@@ -0,0 +1,40 @@
+"""Run-scoped capture of per-rule counterexample analysis.
+
+The autoprove prover tool already runs an LLM analysis of every violated rule during the run
+(``TrivialFanoutCexHandler`` -> ``analyze_cex_raw``); that text is otherwise consumed only as agent
+feedback and discarded. This in-memory, run-scoped store captures it keyed by rule name
+(last-write-wins across prover iterations) so the report phase can reshape the *final* iteration's
+analysis into a finding without re-reasoning about the counterexample.
+
+In-memory is sufficient: the report phase runs in the same process as formalization within
+``composer.pipeline.core.run_pipeline``. A ``BaseStore``-backed variant (cf.
+``composer.prover.report_store``) would be the resume-safe upgrade.
+"""
+from dataclasses import dataclass
+
+
+@dataclass(frozen=True)
+class CexAnalysis:
+    """One rule's captured counterexample analysis: the root-cause / fix explanation and, when
+    available, the counterexample call-trace dump it was derived from."""
+    analysis: str
+    counterexample: str | None = None
+
+
+class CexAnalysisStore:
+    """In-memory ``{rule name -> CexAnalysis}``, last-write-wins. Written by the prover tool's
+    callbacks as analysis completes each iteration; read by the report's findings synthesizer.
+
+    A violated rule that remains violated to the end was analyzed on the final prover run, so
+    last-write-wins holds its final-iteration analysis; a rule fixed before the end is GOOD in the
+    report and its (stale) analysis is simply never looked up."""
+
+    def __init__(self) -> None:
+        self._by_rule: dict[str, CexAnalysis] = {}
+
+    def record(self, rule_name: str, analysis: str, counterexample: str | None = None) -> None:
+        """Store one rule's analysis under ``rule_name``."""
+        self._by_rule[rule_name] = CexAnalysis(analysis=analysis, counterexample=counterexample)
+
+    def get(self, rule_name: str) -> CexAnalysis | None:
+        return self._by_rule.get(rule_name)

composer/spec/source/pipeline.py

@@ -46,8 +46,9 @@
 from composer.spec.source.author import batch_cvl_generation
 from composer.spec.source.artifacts import ProverArtifactStore, ComponentSpec, InvariantSpec
 from composer.spec.source.report_prover import make_prover_fetcher
-from composer.spec.source.report.collect import ReportComponentInput, Verdict, VerdictFetcher
+from composer.spec.source.report.collect import ReportComponentInput, RuleEvidence, Verdict, VerdictFetcher
 from composer.spec.source.report.schema import RuleName
+from composer.spec.source.cex_capture import CexAnalysisStore
 from composer.spec.source.task_ids import (
     HARNESS_TASK_ID, AUTOSETUP_TASK_ID, SUMMARIES_TASK_ID,
     INVARIANTS_TASK_ID, INVARIANT_CVL_TASK_ID,
@@ -108,6 +109,7 @@ class ProverRunner(Formalizer[GeneratedCVL]):
     _resources: list[CVLResource]
     _invariant: tuple[list[PropertyFormulation], Delivered[GeneratedCVL]] | None
     _fetch: VerdictFetcher[GeneratedCVL]
+    _analysis_store: CexAnalysisStore
 
     @override
     async def formalize(
@@ -148,6 +150,16 @@ async def fetch_verdicts(
     ) -> dict[RuleName, Verdict]:
         return await self._fetch(inp)
 
+    @override
+    async def fetch_evidence(self, link: str | None, rule_name: str) -> RuleEvidence | None:
+        # The run captured each violated rule's counterexample analysis as it happened; hand the
+        # final-iteration analysis to the report's findings synthesizer. None -> the finding degrades
+        # to property/group text.
+        rec = self._analysis_store.get(rule_name)
+        if rec is None:
+            return None
+        return RuleEvidence(analysis=rec.analysis, counterexample=rec.counterexample)
+
     @override
     async def finalize(self, outcomes: list[ComponentOutcome[GeneratedCVL]], run: PipelineRun) -> None:
         # components_to_prover_runs.json: {run_key (slug): prover /output/ link}.
@@ -173,6 +185,7 @@ class ProverPrepared(PreparedSystem[GeneratedCVL]):
     _prover_tool: BaseTool
     _prover_opts: ProverOptions
     _analyzed: SourceApplication
+    _analysis_store: CexAnalysisStore
 
     @override
     async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedCVL]:
@@ -233,7 +246,7 @@ async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedC
         return ProverRunner(
             GeneratedCVL, "prover",
             self._store, self._prover_tool, setup_config.prover_config, resources, invariant,
-            make_prover_fetcher(),
+            make_prover_fetcher(), self._analysis_store,
         )
 
     async def _autosetup(self, run: PipelineRun) -> tuple[SetupSuccess, list[CVLResource]]:
@@ -284,6 +297,7 @@ class ProverBackend:
 
     artifact_store: ProverArtifactStore
     _prover_opts: ProverOptions
+    analysis_store: CexAnalysisStore
 
     async def prepare_system(
         self, analyzed: SourceApplication, run: PipelineRun[AutoProvePhase, None],
@@ -295,12 +309,12 @@ async def prepare_system(
         harnessed = _lift_harnessed(analyzed, sys_desc)
         prover_tool = get_prover_tool(
             run.env.llm_heavy(), run.source.contract_name, run.source.project_root,
-            prover_opts=self._prover_opts,
+            prover_opts=self._prover_opts, analysis_store=self.analysis_store,
         )
         return ProverPrepared(
             main_instance(harnessed, run.source),
             self.artifact_store, sys_desc, harnessed, prover_tool,
-            self._prover_opts, analyzed,
+            self._prover_opts, analyzed, self.analysis_store,
         )
 
     def to_artifact_id(self, c: ContractComponentInstance) -> ComponentSpec:

composer/spec/source/prover.py

@@ -40,6 +40,7 @@
 from graphcore.graph import tool_state_update
 from composer.spec.util import temp_certora_file
 from composer.spec.gen_types import CERTORA_DIR, SPECS_DIR
+from composer.spec.source.cex_capture import CexAnalysisStore
 
 
 _logger = logging.getLogger("composer.prover")
@@ -99,12 +100,14 @@ def __init__(
         tool_call_id: str,
         summary: RunSummary,
         config: dict,
+        analysis_store: CexAnalysisStore | None = None,
     ) -> None:
         super().__init__(writer, tool_call_id)
         self._writer = writer
         self._tool_call_id = tool_call_id
         self._summary = summary
         self._config = config
+        self._analysis_store = analysis_store
         self._started_mono: float | None = None
 
     @override
@@ -158,6 +161,19 @@ async def on_prover_result(self, results: dict[str, RuleResult]) -> None:
             results
         )
 
+    @override
+    async def on_analysis_complete(self, rule: RuleResult, explanation: str) -> None:
+        # Capture the per-rule counterexample analysis (last-write-wins across iterations) so the
+        # report phase can reshape the final iteration's analysis into a finding without re-running
+        # the analysis. Key by the bare rule name (rule.path.rule).
+        # Never let a capture error disturb the run.
+        if self._analysis_store is not None:
+            try:
+                self._analysis_store.record(rule.path.rule, explanation, rule.cex_dump)
+            except Exception:
+                _logger.exception("failed to capture cex analysis for %s", rule.name)
+        await super().on_analysis_complete(rule, explanation)
+
 
 class VerifySpecSchema(BaseModel):
     """
@@ -216,6 +232,7 @@ def get_prover_tool(
     main_contract: str,
     project_root: str,
     prover_opts: ProverOptions,
+    analysis_store: CexAnalysisStore | None = None,
 ) -> BaseTool:
     sem = _prover_sem(prover_opts.cloud)
     stamper = make_validation_stamper(VALIDATION_KEY)
@@ -268,7 +285,8 @@ async def verify_spec(
                             [config_path],
                             tool_call_id,
                             prover_opts,
-                            _SpecCallbacks(get_stream_writer(), tool_call_id, summary, config),
+                            _SpecCallbacks(get_stream_writer(), tool_call_id, summary, config,
+                                           analysis_store=analysis_store),
                             DefaultCexHandler(llm, state, summarization_threshold=10)
                         )
 

composer/spec/source/report/build.py

@@ -13,14 +13,15 @@
 from langchain_core.language_models.chat_models import BaseChatModel
 
 from composer.spec.source.report.collect import (
-    ReportableResult, ReportComponentInput, VerdictFetcher, collect,
+    EvidenceFetcher, ReportableResult, ReportComponentInput, VerdictFetcher, collect,
 )
 from composer.spec.source.report.coverage import ValidationError, validate
+from composer.spec.source.report.findings import build_findings
 from composer.spec.source.report.grouping import (
     build_fallback_grouping, build_groups, call_grouping_llm,
 )
 from composer.spec.source.report.schema import (
-    AutoProverReport, Outcome, PropertyKey, ReportBackend, RuleRef,
+    AutoProverReport, Finding, Outcome, PropertyKey, ReportBackend, RuleRef,
 )
 
 _log = logging.getLogger(__name__)
@@ -42,8 +43,15 @@ async def build_report[R: ReportableResult](
     components: list[ReportComponentInput[R]],
     llm: BaseChatModel,
     fetch_verdicts: VerdictFetcher[R],
+    findings_llm: BaseChatModel | None = None,
+    fetch_evidence: EvidenceFetcher | 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.
+
+    When ``findings_llm`` is supplied, violated rules are additionally synthesized into
+    Sherlock-``IssueIn``-shaped `Finding`s (best-effort; a synthesis failure yields no findings
+    rather than failing the report). ``fetch_evidence`` supplies each violation's captured
+    counterexample analysis; it is optional."""
     properties, rules, skipped, gave_up, dropped = await collect(
         components, fetch_verdicts=fetch_verdicts
     )
@@ -84,6 +92,22 @@ async def build_report[R: ReportableResult](
         )
         coverage.warnings = ["FALLBACK GROUPING APPLIED"] + coverage.warnings
 
+    # Violated rules -> findings. Its own guard: findings synthesis must never fail the report
+    # (the whole phase is also best-effort in the caller, but this keeps a working report even when
+    # only findings break).
+    findings: list[Finding] = []
+    if findings_llm is not None:
+        try:
+            findings = await build_findings(
+                contract_name=contract_name, backend=backend, rules=rules,
+                properties=properties, groups=groups, fetch_evidence=fetch_evidence,
+                llm=findings_llm,
+            )
+        except Exception as e:  # noqa: BLE001
+            if RERAISE_REPORT_FAILURES:
+                raise
+            _log.warning("report: findings synthesis failed (%s); continuing without findings", e)
+
     report = AutoProverReport(
         backend=backend,
         contract_name=contract_name,
@@ -96,5 +120,6 @@ async def build_report[R: ReportableResult](
         skipped=skipped,
         gave_up_components=gave_up,
         coverage=coverage,
+        findings=findings,
     )
     return report

composer/spec/source/report/collect.py

@@ -101,6 +101,25 @@ async def __call__(self, input: ReportComponentInput[R], /) -> dict[RuleName, Ve
         ...
 
 
+@dataclass(frozen=True)
+class RuleEvidence:
+    """Backend-supplied raw material for synthesizing a finding from a violated rule.
+
+    ``analysis`` is the backend's pre-computed root-cause / fix explanation for the violation
+    (prover: the ``analyze_cex_raw`` output captured during the run); ``counterexample`` is a concrete
+    failing trace excerpt (prover: the rule's ``cex_dump``). Both optional — a finding degrades to
+    property/group text when absent."""
+    analysis: str | None = None
+    counterexample: str | None = None
+
+
+class EvidenceFetcher(Protocol):
+    """Backend hook: given a violated rule's run link + name, return its `RuleEvidence` (or ``None``
+    when the backend has none). Prover reads the run-scoped CEX-analysis capture; foundry has none."""
+    async def __call__(self, link: str | None, rule_name: str, /) -> "RuleEvidence | None":
+        ...
+
+
 async def collect[R: ReportableResult](
     inputs: list[ReportComponentInput[R]],
     *,