diff --git a/composer/pipeline/core.py b/composer/pipeline/core.py
index 97ce1b0b..3b174c14 100644
--- a/composer/pipeline/core.py
+++ b/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"])
)
diff --git a/composer/spec/source/autoprove_common.py b/composer/spec/source/autoprove_common.py
index 24eb0a7e..ce819aad 100644
--- a/composer/spec/source/autoprove_common.py
+++ b/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
diff --git a/composer/spec/source/cex_capture.py b/composer/spec/source/cex_capture.py
new file mode 100644
index 00000000..ab3d3400
--- /dev/null
+++ b/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)
diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py
index c6ac5120..a58bbb1d 100644
--- a/composer/spec/source/pipeline.py
+++ b/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:
diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py
index f6715372..e46f2382 100644
--- a/composer/spec/source/prover.py
+++ b/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)
)
diff --git a/composer/spec/source/report/build.py b/composer/spec/source/report/build.py
index 70f1ec64..b7ef76e4 100644
--- a/composer/spec/source/report/build.py
+++ b/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
diff --git a/composer/spec/source/report/collect.py b/composer/spec/source/report/collect.py
index ddff5b8e..071a3a19 100644
--- a/composer/spec/source/report/collect.py
+++ b/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]],
*,
diff --git a/composer/spec/source/report/findings.py b/composer/spec/source/report/findings.py
new file mode 100644
index 00000000..46340d13
--- /dev/null
+++ b/composer/spec/source/report/findings.py
@@ -0,0 +1,153 @@
+"""Synthesize Sherlock-``IssueIn``-shaped findings from violated rules.
+
+For each violated rule (a `RuleVerdict` with ``outcome == Outcome.BAD``) this reshapes the
+counterexample analysis the run already produced — looked up via the backend `EvidenceFetcher` — into
+a `Finding`. One structured LLM call per violation, fed the *distilled* analysis rather than the raw
+counterexample, so the expensive counterexample reasoning is not repeated. Best-effort per finding:
+any failure drops that one finding, never the report.
+
+v1 scope: prover-only (a foundry BAD is an author-declared demonstration, not a discovered bug).
+Severity is LLM-assigned from the default Sherlock rubric via the Impact × Likelihood matrix in the
+system template. ``IssueIn.locations`` is not produced here — a run knows only local paths and CVL-spec
+lines, so the submission layer reconstructs source locations from the engagement scope + counterexample
+(the accurate report-time locator is on ``FindingProvenance``: rule name, spec file, prover-run link).
+"""
+import asyncio
+import logging
+from typing import Literal
+
+from langchain_core.language_models.chat_models import BaseChatModel
+from langchain_core.messages import HumanMessage, SystemMessage
+from pydantic import BaseModel, Field
+
+from composer.templates.loader import load_jinja_template
+from composer.spec.source.report.collect import EvidenceFetcher, RuleEvidence
+from composer.spec.source.report.schema import (
+ Finding, FindingProvenance, FormalizedProperty, IssueContent, Outcome,
+ PropertyGroup, PropertyKey, ReportBackend, RuleRef, RuleVerdict,
+)
+
+_log = logging.getLogger(__name__)
+
+Severity = Literal["critical", "high", "medium", "low", "informational"]
+
+#: Bound the counterexample we inline (as prompt input and as ``proof_of_concept``).
+_MAX_CEX_CHARS = 8000
+
+
+class FindingDraft(BaseModel):
+ """The LLM-authored prose + severity for one finding. Code fills locations / PoC / references /
+ provenance around it. Mirrors the Sherlock ``IssueContent`` (minus the machine-filled fields)."""
+ title: str = Field(max_length=200, description="One-line, issue-specific title.")
+ severity: Severity = Field(description="critical | high | medium | low | informational.")
+ severity_reasoning: str = Field(
+ max_length=4000,
+ description="1-3 sentences: the Impact tier, the Likelihood tier, and the matrix cell they select.",
+ )
+ summary: str = Field(max_length=2000, description="1-3 sentence tl;dr.")
+ description: str = Field(max_length=50000, description="Full technical description grounded in the counterexample.")
+ impact: str = Field(max_length=20000, description="Concrete consequence if exploited.")
+ attack_path: str | None = Field(default=None, max_length=20000, description="Step-by-step exploit path, or null.")
+ assumptions_and_uncertainties: str | None = Field(default=None, max_length=10000, description="Assumptions / uncertainties, or null.")
+
+
+async def build_findings(
+ *,
+ contract_name: str,
+ backend: ReportBackend,
+ rules: list[RuleVerdict],
+ properties: list[FormalizedProperty],
+ groups: list[PropertyGroup],
+ fetch_evidence: EvidenceFetcher | None,
+ llm: BaseChatModel,
+) -> list[Finding]:
+ """One `Finding` per violated rule (concurrent, best-effort). Returns ``[]`` for a non-prover
+ backend or when nothing is violated."""
+ if backend != "prover":
+ return []
+ bad = [r for r in rules if r.outcome == Outcome.BAD]
+ if not bad:
+ return []
+
+ # Reverse index a violated rule -> the properties it breaks -> their audit group (for prose context).
+ props_by_ref: dict[RuleRef, list[FormalizedProperty]] = {}
+ for p in properties:
+ for ref in p.rule_refs:
+ props_by_ref.setdefault(ref, []).append(p)
+ group_by_key: dict[PropertyKey, PropertyGroup] = {}
+ for g in groups:
+ for k in g.members:
+ group_by_key.setdefault(k, g)
+
+ system = load_jinja_template("autoprove_report_findings_system.j2")
+ bound = llm.with_structured_output(FindingDraft)
+
+ async def _one(rule: RuleVerdict) -> Finding | None:
+ try:
+ ev = await fetch_evidence(rule.prover_link, rule.name) if fetch_evidence else None
+ prop = _pick_property(props_by_ref.get(rule.ref, []))
+ group = group_by_key.get(prop.key) if prop else None
+ user = load_jinja_template(
+ "autoprove_report_findings_prompt.j2",
+ contract_name=contract_name,
+ rule_name=rule.name,
+ property_title=prop.title if prop else None,
+ property_description=prop.description if prop else None,
+ property_sort=prop.sort if prop else None,
+ group_title=group.title if group else None,
+ group_description=group.description if group else None,
+ analysis=ev.analysis if ev else None,
+ counterexample=_trim(ev.counterexample) if ev else None,
+ )
+ draft = await bound.ainvoke([SystemMessage(system), HumanMessage(user)])
+ assert isinstance(draft, FindingDraft)
+ return _compose(rule, draft, ev, group_slug=group.slug if group else None)
+ except Exception: # noqa: BLE001 — one finding failing must never fail the report
+ _log.warning("report: finding synthesis failed for rule %r; skipping", rule.name, exc_info=True)
+ return None
+
+ findings = await asyncio.gather(*[_one(r) for r in bad])
+ return [f for f in findings if f is not None]
+
+
+def _pick_property(props: list[FormalizedProperty]) -> FormalizedProperty | None:
+ """A violated rule may formalize several properties; pick a stable representative (first by
+ title) to describe the finding. They describe the same violation, so the choice affects only
+ which prose seeds the write-up."""
+ return sorted(props, key=lambda p: p.title)[0] if props else None
+
+
+def _trim(text: str | None) -> str | None:
+ if not text:
+ return None
+ return text if len(text) <= _MAX_CEX_CHARS else text[:_MAX_CEX_CHARS] + "\n…(truncated)"
+
+
+def _compose(
+ rule: RuleVerdict,
+ draft: FindingDraft,
+ ev: RuleEvidence | None,
+ *,
+ group_slug: str | None,
+) -> Finding:
+ return Finding(
+ title=draft.title,
+ severity=draft.severity,
+ content=IssueContent(
+ summary=draft.summary,
+ description=draft.description,
+ impact=draft.impact,
+ attack_path=draft.attack_path,
+ assumptions_and_uncertainties=draft.assumptions_and_uncertainties,
+ proof_of_concept=_trim(ev.counterexample) if ev else None,
+ references=[rule.prover_link] if rule.prover_link else None,
+ ),
+ provenance=FindingProvenance(
+ rule_name=rule.name,
+ spec_file=rule.spec_file,
+ outcome=rule.outcome,
+ group_slug=group_slug,
+ prover_link=rule.prover_link,
+ severity_reasoning=draft.severity_reasoning,
+ ),
+ )
diff --git a/composer/spec/source/report/render.py b/composer/spec/source/report/render.py
index 25986c51..0e197ea6 100644
--- a/composer/spec/source/report/render.py
+++ b/composer/spec/source/report/render.py
@@ -26,8 +26,8 @@
from composer.spec.gen_types import TypedTemplate
from composer.templates.loader import load_jinja_template
from composer.spec.source.report.schema import (
- AutoProverReport, CoverageReport, FormalizedProperty, GaveUpComponent, GroupStatus, Outcome,
- PropertyGroup, PropertyKey, ReportBackend, RuleRef, RuleVerdict, SkippedClaim,
+ AutoProverReport, CoverageReport, Finding, FormalizedProperty, GaveUpComponent, GroupStatus,
+ Outcome, PropertyGroup, PropertyKey, ReportBackend, RuleRef, RuleVerdict, SkippedClaim,
)
@@ -45,6 +45,14 @@
GroupStatus.PARTIAL: "warn",
GroupStatus.UNKNOWN: "muted",
}
+# Finding severity (default Sherlock rubric) -> CSS badge kind. Unknown/custom severities render muted.
+_SEVERITY_KIND: dict[str, str] = {
+ "critical": "bad",
+ "high": "bad",
+ "medium": "warn",
+ "low": "info",
+ "informational": "muted",
+}
# Per-backend human labels: the data carries the neutral `Outcome`; these turn it into the words an
# auditor reads ("Verified" for a proof, "Successful test" for a forge run).
@@ -134,6 +142,20 @@ class GroupView(TypedDict):
rows: list[RowView]
+class FindingView(TypedDict):
+ title: str
+ severity: str
+ severity_kind: str
+ severity_reasoning: str | None
+ summary: str
+ impact: str
+ description: str
+ attack_path: str | None
+ link: LinkView
+ rule_name: str | None
+ spec_file: str | None
+
+
class ReportTemplateParams(TypedDict):
"""The full, typed context of ``autoprove_report.html.j2``."""
report: AutoProverReport
@@ -143,6 +165,7 @@ class ReportTemplateParams(TypedDict):
prover_runs: list[RunView]
rule_counts: list[ChipView]
group_counts: list[ChipView]
+ findings: list[FindingView]
groups: list[GroupView]
skipped: list[SkippedClaim]
gave_up: list[GaveUpComponent]
@@ -227,6 +250,25 @@ def _group_view(
}
+def _finding_view(f: Finding) -> FindingView:
+ """Project a `Finding` into the template shape: the Sherlock fields the page shows, plus a
+ severity->CSS kind and the prover-run link pulled from provenance."""
+ prov = f.provenance
+ return {
+ "title": f.title,
+ "severity": f.severity,
+ "severity_kind": _SEVERITY_KIND.get(f.severity.lower(), "muted"),
+ "severity_reasoning": prov.severity_reasoning if prov else None,
+ "summary": f.content.summary,
+ "impact": f.content.impact,
+ "description": f.content.description,
+ "attack_path": f.content.attack_path,
+ "link": _link_view(prov.prover_link if prov else None),
+ "rule_name": prov.rule_name if prov else None,
+ "spec_file": prov.spec_file if prov else None,
+ }
+
+
def _build_context(report: AutoProverReport) -> ReportTemplateParams:
props_by_key = {p.key: p for p in report.properties}
rules_by_ref = {r.ref: r for r in report.rules}
@@ -244,6 +286,7 @@ def _build_context(report: AutoProverReport) -> ReportTemplateParams:
],
"rule_counts": _outcome_counts([r.outcome for r in report.rules], unit_labels),
"group_counts": _group_counts([g.status for g in report.groups], group_labels),
+ "findings": [_finding_view(f) for f in report.findings],
"groups": [
_group_view(g, props_by_key, rules_by_ref, unit_labels, group_labels)
for g in report.groups
diff --git a/composer/spec/source/report/schema.py b/composer/spec/source/report/schema.py
index a791ac7e..450b6999 100644
--- a/composer/spec/source/report/schema.py
+++ b/composer/spec/source/report/schema.py
@@ -157,6 +157,55 @@ class CoverageReport(BaseModel):
for a report.json it reads cold."""
+# ---------------------------------------------------------------------------
+# Findings — violated rules surfaced as audit issues.
+#
+# `Finding` carries the Sherlock Audit Engine "Submit Issue" fields (schema ``IssueIn``,
+# POST /v1/engagements/{id}/issues) that a run can populate at report time: ``title``, ``severity``,
+# and the ``content`` prose. One finding is emitted per violated rule (a `RuleVerdict` with
+# ``outcome == Outcome.BAD``); its prose is synthesized from the rule's counterexample analysis and
+# the property/group it breaks (see ``report/findings.py``). Sherlock length caps are mirrored but
+# not enforced (report.json is lenient — the submission endpoint is the validating gate).
+#
+# ``IssueIn.locations`` is deliberately NOT carried here: a run only knows local paths and CVL-spec
+# lines, not the source ``{owner}/{repo}`` / file / line a Sherlock location needs, so the submission
+# layer reconstructs locations from the engagement scope + the counterexample. The accurate
+# report-time locator lives in ``provenance`` (rule name, spec file, prover-run link).
+# ---------------------------------------------------------------------------
+
+class IssueContent(BaseModel):
+ """A finding's free-text sections — the ``IssueIn.content`` shape."""
+ summary: str = Field(max_length=2000, description="Short tl;dr of the finding, in one to three sentences.")
+ description: str = Field(max_length=50000, description="Full technical description of the vulnerability and how it manifests.")
+ impact: str = Field(max_length=20000, description="Concrete consequence if exploited (funds at risk, DoS, data exposure, ...).")
+ attack_path: str | None = Field(default=None, max_length=20000, description="Step-by-step exploit path, if applicable.")
+ assumptions_and_uncertainties: str | None = Field(default=None, max_length=10000, description="Assumptions relied on and anything the submitter is unsure about.")
+ proof_of_concept: str | None = Field(default=None, max_length=65536, description="Executable PoC, or the prover counterexample demonstrating the issue.")
+ references: list[str] | None = Field(default=None, description="Supporting links (e.g. the prover run).")
+
+
+class FindingProvenance(BaseModel):
+ """Report-only trace from a finding back to the verdict/property that produced it. NOT part of
+ the Sherlock ``IssueIn`` payload — a submitter drops it."""
+ rule_name: RuleName
+ spec_file: str
+ outcome: Outcome
+ group_slug: str | None = None
+ prover_link: str | None = None
+ #: The finding-synthesis LLM's justification for the assigned severity (Impact × Likelihood).
+ severity_reasoning: str | None = None
+
+
+class Finding(BaseModel):
+ """A violated rule rendered as an audit issue. ``title``/``severity``/``content`` are the Sherlock
+ ``IssueIn`` fields a run can fill at report time; ``provenance`` is report-only. ``IssueIn.locations``
+ is added by the submission layer (see the module comment), not stored here."""
+ title: str = Field(max_length=200, description="One-line title of the finding.")
+ severity: str = Field(description="Severity tier. Default rubric: critical / high / medium / low / informational.")
+ content: IssueContent
+ provenance: FindingProvenance | None = None
+
+
class AutoProverReport(BaseModel):
"""Top-level report document — written to ``certora/ap_report/report.json``."""
schema_version: Literal["3.0"] = "3.0"
@@ -172,3 +221,7 @@ class AutoProverReport(BaseModel):
skipped: list[SkippedClaim] = Field(default_factory=list)
gave_up_components: list[GaveUpComponent] = Field(default_factory=list)
coverage: CoverageReport
+ #: Violated rules surfaced as Sherlock-``IssueIn``-shaped audit issues (one per BAD rule; empty
+ #: when nothing is violated, when synthesis was unavailable, or for a non-prover backend). Prose
+ #: is synthesized at report time — see ``report/findings.py``.
+ findings: list[Finding] = Field(default_factory=list)
diff --git a/composer/templates/autoprove_report.html.j2 b/composer/templates/autoprove_report.html.j2
index 894c6c9c..311b2fa9 100644
--- a/composer/templates/autoprove_report.html.j2
+++ b/composer/templates/autoprove_report.html.j2
@@ -134,6 +134,58 @@ section.prop .desc {
.badge-warn { color: var(--warn-fg); background: var(--warn-bg); }
.badge-info { color: var(--info-fg); background: var(--info-bg); }
.badge-muted { color: var(--muted-fg); background: var(--muted-bg); }
+.findings-head { margin: 20px 0 12px; }
+.findings-head h2 {
+ margin: 0 0 4px;
+ font-size: 18px;
+ font-weight: 600;
+ display: flex;
+ align-items: center;
+ gap: 10px;
+}
+section.finding {
+ background: var(--bg-card);
+ border: 1px solid var(--border);
+ border-left: 3px solid var(--bad-fg);
+ border-radius: 8px;
+ padding: 16px 20px;
+ margin-bottom: 14px;
+}
+section.finding h3 {
+ margin: 0 0 8px;
+ font-size: 15px;
+ font-weight: 600;
+ display: flex;
+ align-items: center;
+ gap: 10px;
+ flex-wrap: wrap;
+}
+.finding-meta {
+ display: flex;
+ flex-wrap: wrap;
+ gap: 12px;
+ align-items: baseline;
+ font-size: 12px;
+ color: var(--muted-fg);
+ margin-bottom: 10px;
+}
+.finding-meta code {
+ font-family: ui-monospace, SFMono-Regular, "SF Mono", Menlo, monospace;
+ font-size: 11.5px;
+ word-break: break-all;
+}
+.finding-meta a { color: var(--link); text-decoration: none; }
+.finding-meta a:hover { text-decoration: underline; }
+.finding-summary { margin: 0 0 12px; }
+dl.finding-body {
+ display: grid;
+ grid-template-columns: max-content 1fr;
+ gap: 6px 16px;
+ margin: 0;
+ font-size: 13px;
+}
+dl.finding-body dt { color: var(--muted-fg); font-weight: 600; }
+dl.finding-body dd { margin: 0; white-space: pre-wrap; }
table.rules {
width: 100%;
border-collapse: collapse;
@@ -247,6 +299,29 @@ footer.report-foot {
{%- endif %}
+{%- if findings %}
+
+ Findings {{ findings | length }}
+ Violated {{ terms.unit_plural }} surfaced as audit issues — fields follow the standard issue-submission format.
+
+{%- for f in findings %}
+
+ {{ f.severity }} {{ f.title }}
+
+ {{ f.summary }}
+
+ {%- if f.severity_reasoning %}- Severity rationale
- {{ f.severity_reasoning }}
{% endif %}
+ - Impact
- {{ f.impact }}
+ - Description
- {{ f.description }}
+ {%- if f.attack_path %}- Attack path
- {{ f.attack_path }}
{% endif %}
+
+
+{%- endfor %}
+{%- endif %}
+
{%- for g in groups %}
{{ g.slug }} {{ g.title }} {{ g.label }}
diff --git a/composer/templates/autoprove_report_findings_prompt.j2 b/composer/templates/autoprove_report_findings_prompt.j2
new file mode 100644
index 00000000..3f4cfb29
--- /dev/null
+++ b/composer/templates/autoprove_report_findings_prompt.j2
@@ -0,0 +1,21 @@
+Contract: {{ contract_name }}
+
+Violated rule: {{ rule_name }}
+{% if property_description -%}
+Property it formalizes ({{ property_sort }}): {{ property_title }}
+ {{ property_description }}
+{% endif -%}
+{% if group_title -%}
+Audit-level claim it belongs to: {{ group_title }}
+ {{ group_description }}
+{% endif %}
+{% if analysis -%}
+The prover's counterexample analysis (root cause + suggested fix), produced during the run:
+{{ analysis }}
+{%- else -%}
+(No counterexample analysis was captured for this rule — reason conservatively from the property.)
+{%- endif %}
+{% if counterexample %}
+Counterexample trace:
+{{ counterexample }}
+{% endif %}
diff --git a/composer/templates/autoprove_report_findings_system.j2 b/composer/templates/autoprove_report_findings_system.j2
new file mode 100644
index 00000000..c4247571
--- /dev/null
+++ b/composer/templates/autoprove_report_findings_system.j2
@@ -0,0 +1,50 @@
+You are a smart-contract security auditor writing up a single, confirmed finding for an audit
+report. A formal-verification rule was VIOLATED: the Certora Prover found a concrete counterexample
+refuting a property the code was expected to satisfy. A violation is hard evidence the property does
+not hold, so treat this as a real, confirmed issue — not a maybe.
+
+You are given the violated rule, the natural-language property it formalizes, the audit-level claim
+(group) it belongs to, the prover's own root-cause analysis of the counterexample, and — when
+available — the counterexample trace itself.
+
+Write the finding as these fields:
+ - title: one line (<= 200 chars), specific to THIS issue — name the broken guarantee, not the rule.
+ - severity: exactly one of `critical`, `high`, `medium`, `low`, `informational`, assigned via the
+ Impact × Likelihood matrix in the SEVERITY CLASSIFICATION section below.
+ - severity_reasoning: 1-3 sentences justifying the severity — state the Impact tier and the
+ Likelihood tier you assessed and the matrix cell they select.
+ - summary: a 1-3 sentence tl;dr.
+ - description: the full technical explanation of the vulnerability and how it manifests, grounded
+ in the supplied analysis and counterexample.
+ - impact: the concrete consequence if exploited.
+ - attack_path: the step-by-step path derived from the counterexample, or null if not applicable.
+ - assumptions_and_uncertainties: anything the finding relies on or you are unsure about, or null.
+
+SEVERITY CLASSIFICATION
+Assess two axes independently, then read the severity off the matrix — do not eyeball it.
+
+Impact — what an attacker gains or users lose when the property break is exploited:
+ - High: direct loss or theft of funds, protocol insolvency, permanent freezing of assets, or
+ unauthorized control of privileged functionality.
+ - Medium: limited, conditional, or recoverable value loss; temporary denial of service; incorrect
+ accounting that does not by itself drain funds.
+ - Low: no funds at risk; a minor or cosmetic deviation from the intended guarantee.
+
+Likelihood — how reachable the counterexample is in practice:
+ - High: exploitable by any actor with no special preconditions or privileged access.
+ - Medium: needs a specific but reachable state, ordering, or non-trivial-yet-feasible setup.
+ - Low: needs privileged access, an unusual configuration, or a narrow / costly window.
+
+ | Likelihood \ Impact | High | Medium | Low |
+ | High | critical | high | medium |
+ | Medium | high | medium | low |
+ | Low | medium | low | low |
+
+Use `informational` ONLY for a property break with no real-world exploit path — a code-quality or
+specification observation, not a vulnerability. A prover counterexample proves the property CAN be
+broken, so never downgrade a genuine break to `informational` just because it looks hard to reach;
+instead lower the Likelihood tier and let the matrix decide.
+
+Ground every claim in the supplied analysis and counterexample. Do NOT invent addresses, values,
+function names, or exploit steps beyond what the material supports; if the material is thin, keep the
+finding modest rather than fabricating specifics. Return output exactly matching the requested schema.
diff --git a/tests/test_autoprove_report.py b/tests/test_autoprove_report.py
index 9849699a..03742296 100644
--- a/tests/test_autoprove_report.py
+++ b/tests/test_autoprove_report.py
@@ -35,10 +35,15 @@
)
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,
+ AutoProverReport, CoverageReport, Finding, FindingProvenance, FormalizedProperty,
+ GaveUpComponent, GroupStatus, IssueContent, Outcome, PropertyGroup,
+ RuleVerdict, SkippedClaim,
)
from composer.spec.source.report_prover import make_prover_fetcher
+from composer.spec.source.report.collect import RuleEvidence
+from composer.spec.source.report.findings import FindingDraft, build_findings
+from composer.spec.source.cex_capture import CexAnalysisStore
+from composer.diagnostics.timing import RunSummary
# ---------------------------------------------------------------------------
@@ -506,3 +511,182 @@ async def test_build_surfaces_skipped_and_gave_up_gaps(tmp_path):
assert [(s.component, s.title) for s in report.skipped] == [("C", "p_skip")]
assert [g.component for g in report.gave_up_components] == ["D"]
assert report.coverage.skipped_count == 1 and report.coverage.gave_up_component_count == 1
+
+
+# ---------------------------------------------------------------------------
+# findings (violated rules -> Sherlock IssueIn shape)
+# ---------------------------------------------------------------------------
+
+class _FindingStubModel(BaseChatModel):
+ """A `BaseChatModel` whose structured-output binding returns a preset `FindingDraft`, so the
+ real `build_findings` (templates + compose) runs without a live model."""
+ draft: FindingDraft
+
+ def with_structured_output(self, schema, **kwargs) -> Runnable: # type: ignore[override]
+ draft = self.draft
+ return RunnableLambda(lambda _messages: draft)
+
+ def _generate(self, messages, stop=None, run_manager=None, **kwargs) -> ChatResult:
+ raise NotImplementedError("stub is structured-output only")
+
+ @property
+ def _llm_type(self) -> str:
+ return "finding-stub"
+
+
+def _draft(severity: str = "high", title: str = "Reentrancy drains vault") -> FindingDraft:
+ return FindingDraft(
+ title=title, severity=severity,
+ severity_reasoning="High impact (fund loss) x Medium likelihood -> high.",
+ summary="s", description="d", impact="funds at risk", attack_path="1..2..3",
+ )
+
+
+def _evidence(by_rule: dict[str, RuleEvidence]):
+ async def fetch(link, rule_name):
+ return by_rule.get(rule_name)
+ return fetch
+
+
+def _finding(severity: str = "high") -> Finding:
+ return Finding(
+ title="Reentrancy drains vault", severity=severity,
+ content=IssueContent(summary="s", description="d", impact="funds at risk",
+ proof_of_concept=""),
+ provenance=FindingProvenance(rule_name="r_bad", spec_file="c.spec", outcome=Outcome.BAD,
+ group_slug="g", prover_link="https://prover.example/run/abc",
+ severity_reasoning="High impact x Medium likelihood -> high."),
+ )
+
+
+@pytest.mark.asyncio
+async def test_build_report_synthesizes_one_finding_per_violation():
+ """Only the violated rule becomes a finding; it carries the LLM severity, the counterexample as
+ proof_of_concept, the run link as a reference, and provenance back to the violated rule. No
+ locations are produced at report time (submission builds those)."""
+ gen = _gen({"p_good": ["r_ok"], "p_bad": ["r_bad"]})
+ fetch = _fetcher({"L1": [
+ _fake_check("r_ok", NodeStatus.VERIFIED, file="autospec_C.spec"),
+ _fake_check("r_bad", NodeStatus.VIOLATED, line=42, file="autospec_C.spec"),
+ ]})
+ grouping = _GroupingStubModel(result=GroupingResult(groups=[PropertyGroupDraft(
+ slug="g", title="G", description="gd", members=[("C", "p_good"), ("C", "p_bad")])]))
+ evidence = _evidence({"r_bad": RuleEvidence(analysis="root cause X", counterexample="")})
+
+ report = await build.build_report(
+ contract_name="Vault", backend="prover",
+ components=[_input("C", "autospec_C.spec",
+ [_prop("p_good", "d"), _prop("p_bad", "d")], gen)],
+ llm=grouping, fetch_verdicts=fetch,
+ findings_llm=_FindingStubModel(draft=_draft()), fetch_evidence=evidence,
+ )
+
+ assert len(report.findings) == 1
+ f = report.findings[0]
+ assert f.severity == "high"
+ assert f.provenance.rule_name == "r_bad" and f.provenance.outcome == Outcome.BAD
+ assert f.provenance.group_slug == "g" and f.provenance.spec_file == "autospec_C.spec"
+ assert not hasattr(f, "locations") # locations are a submission-layer concern, not on the report
+ assert f.content.proof_of_concept == ""
+ assert f.content.references == ["L1"]
+ assert f.provenance.severity_reasoning # the impact x likelihood justification is captured
+
+
+@pytest.mark.asyncio
+async def test_build_report_no_findings_without_findings_llm():
+ """The findings pass is opt-in: omitting ``findings_llm`` leaves findings empty (back-compat)."""
+ gen = _gen({"p_bad": ["r_bad"]})
+ fetch = _fetcher({"L1": [_fake_check("r_bad", NodeStatus.VIOLATED)]})
+ grouping = _GroupingStubModel(result=GroupingResult(groups=[PropertyGroupDraft(
+ slug="g", title="G", description="d", members=[("C", "p_bad")])]))
+ report = await build.build_report(
+ contract_name="C", backend="prover",
+ components=[_input("C", "autospec_C.spec", [_prop("p_bad", "d")], gen)],
+ llm=grouping, fetch_verdicts=fetch,
+ )
+ assert report.findings == []
+
+
+@pytest.mark.asyncio
+async def test_build_findings_degrades_without_evidence():
+ """A violated rule with no captured analysis still yields a finding (from property/group text);
+ proof_of_concept is absent, and the accurate locator (spec_file) rides provenance."""
+ rules = [_rv("c.spec", "r_bad", Outcome.BAD)]
+ props = [_fp("C", "p_bad", [("c.spec", "r_bad")], desc="balances stay solvent")]
+ groups = [_pg("g", [("C", "p_bad")], status=GroupStatus.BAD)]
+ findings = await build_findings(
+ contract_name="Vault", backend="prover", rules=rules, properties=props, groups=groups,
+ fetch_evidence=None, llm=_FindingStubModel(draft=_draft(severity="medium")),
+ )
+ assert len(findings) == 1
+ assert findings[0].severity == "medium"
+ assert findings[0].content.proof_of_concept is None
+ assert findings[0].provenance.spec_file == "c.spec"
+
+
+@pytest.mark.asyncio
+async def test_build_findings_foundry_is_empty():
+ """v1 is prover-only: a foundry BAD (author-declared expected-failure demonstration) is not a
+ discovered vulnerability, so no findings are synthesized."""
+ rules = [_rv("c.t.sol", "t_bad", Outcome.BAD)]
+ findings = await build_findings(
+ contract_name="V", backend="foundry", rules=rules, properties=[], groups=[],
+ fetch_evidence=None, llm=_FindingStubModel(draft=_draft()),
+ )
+ assert findings == []
+
+
+def test_render_html_findings_section():
+ report = _mini_report().model_copy(update={"findings": [_finding()]})
+ h = render_html(report)
+ assert '' in h
+ assert "Reentrancy drains vault" in h
+ assert "badge-bad" in h # high severity
+ assert "r_bad" in h and "c.spec" in h # provenance locator (rule in spec file)
+ assert "Severity rationale" in h and "Medium likelihood" in h
+
+
+def test_render_html_omits_findings_section_when_empty():
+ h = render_html(_mini_report()) # _mini_report has no findings
+ assert '' not in h
+ assert '' not in h
+
+
+def test_report_round_trips_with_findings(tmp_path):
+ report = _mini_report().model_copy(update={"findings": [_finding()]})
+ ProverArtifactStore(str(tmp_path), "Counter").write_report(report)
+
+ out = tmp_path / "certora" / "ap_report" / "report.json"
+ reloaded = AutoProverReport.model_validate_json(out.read_text())
+ assert len(reloaded.findings) == 1
+ assert reloaded.findings[0].content.impact == "funds at risk"
+ assert reloaded.findings[0].provenance.rule_name == "r_bad"
+ assert reloaded.findings[0].provenance.severity_reasoning == "High impact x Medium likelihood -> high."
+ assert not hasattr(reloaded.findings[0], "locations")
+
+
+@pytest.mark.asyncio
+async def test_spec_callbacks_captures_cex_analysis():
+ """The source-pipeline prover callback records each violated rule's analysis into the run-scoped
+ store (under both the bare and pretty-printed rule name) while still emitting the stream event."""
+ from composer.spec.source.prover import _SpecCallbacks
+ from composer.prover.ptypes import RulePath, RuleResult
+
+ store = CexAnalysisStore()
+ events: list = []
+ cb = _SpecCallbacks(events.append, "tc1", cast(RunSummary, SimpleNamespace()), {},
+ analysis_store=store)
+ rule = RuleResult(path=RulePath(rule="no_reentrancy", method="withdraw"),
+ cex_dump="", status="VIOLATED")
+
+ await cb.on_analysis_complete(rule, "root cause: external call before state update")
+
+ # Keyed by the bare rule name (RulePath.rule) — exactly what the report's RuleVerdict.name carries
+ # (POU derives it from the prover tree's context[0]) — so the findings join is an exact match.
+ rec = store.get("no_reentrancy")
+ assert rec is not None and rec.analysis.startswith("root cause")
+ assert rec.counterexample == ""
+ # NOT keyed by the pretty-printed form ("no_reentrancy for withdraw"); the report never looks that up.
+ assert store.get(rule.name) is None
+ # the UI stream event still fires
+ assert any(e.get("type") == "rule_analysis" for e in events)