Add findings to the report by naftali-g · Pull Request #80 · Certora/AutoProver

naftali-g · 2026-07-16T13:42:28Z

No description provided.

jtoman · 2026-07-16T17:32:05Z

+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":


absolutely no reason to quote this type annotation. a little curious you have the "positional only" marker here but I'm not mad about it.

jtoman · 2026-07-16T17:33:06Z

+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:


what expensive reasoning? the cex analysis in cex_analysis_raw or whatever it is is single shot llm call?

jtoman · 2026-07-16T17:34:28Z

+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).


I... don't think this is true? if you write an invariant test or a fuzz test, it's worth an explanation of why that invariant failure happened or why the fuzz test parameters chosen were problematic right? But for v1 this is fine, but I just want to make sure we don't buy this reasoning and avoid revisiting this for foundry in the future.

jtoman · 2026-07-16T17:35:03Z

+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).


I'm sure I'll understand this more as I read the rest of the file, but having read it without further context, this last sentence is unintelligible.

jtoman · 2026-07-16T17:35:31Z

+        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.")


"tl;dr" really?

jtoman · 2026-07-16T17:54:20Z

    prover_runs: list[RunView]
    rule_counts: list[ChipView]
    group_counts: list[ChipView]
+    findings: list[FindingView]


jtoman · 2026-07-16T17:56:05Z

+# 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).


oh THIS is where the length caps come from? But ... wait what API are we targeting here?

jtoman · 2026-07-16T17:57:00Z

+    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.")


this looks super similar to the fields found in the findings.py FindingDraft schema, common basemodel class?

jtoman · 2026-07-16T18:56:58Z

+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.


I strongly suspect we'll someday want to use the agentic handler for the cex in autoprover, so make sure we're not baking in an assumption about always using the TrivialFanoutCexHandler here.

That said, why not use the BaseStore version? seems like we'd want to save this sort of thing?

jtoman · 2026-07-16T18:59:43Z

+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.


if we expect informational to never be the correct output, why even include it in the output schema?

This also suggests we shouldn't let the agent choose this, but pick the two axes on this matrix?

jtoman

all of this looks much, much better. One major question about the grouping/granularity of saving/restoring CEX. Sorry I didn't notice it before...

jtoman · 2026-08-03T21:15:09Z

+            # which one actually broke — that is the LLM's job, not ours to pre-guess.
+            props = props_by_ref.get(rule.ref, [])
+            # A rule's properties may share a group (some may be in none); dedupe by slug, first-seen order.
+            rule_groups = list({g.slug: g for p in props if (g := group_by_key.get(p.key)) is not None}.values())


jtoman · 2026-08-03T21:16:00Z

+            props = props_by_ref.get(rule.ref, [])
+            # A rule's properties may share a group (some may be in none); dedupe by slug, first-seen order.
+            rule_groups = list({g.slug: g for p in props if (g := group_by_key.get(p.key)) is not None}.values())
            user = load_jinja_template(


strong preference for you to move this our TypedTemplate mechanism, it will let you automatically get template fuzz testing (among other things).

jtoman · 2026-08-03T21:18:20Z

-            attack_path=draft.attack_path,
-            assumptions_and_uncertainties=draft.assumptions_and_uncertainties,
-            proof_of_concept=_trim(ev.counterexample) if ev else None,
+            **{f: getattr(draft, f) for f in AuthoredContent.model_fields},


what on god's green earth???

**AuthoredContent.model_dump(draft) would also work (probably), but I'm not sure its that much more readable/less gross. Whatever.

jtoman · 2026-08-03T21:21:05Z

+        await self.store.aput(
+            self.namespace,
+            rule_name,
+            CexAnalysis(analysis=analysis, counterexample=counterexample).model_dump(mode="json"),
+        )


Wait. I didn't notice this in the last round: this keys on the path.rule. But for a parametric rule like:

run whatever(method f) { ... }

that's just whatever. The f instantiation is part of the RulePath method (or contract if it exists too). Keying on rule alone might be what you want, but it means the last CEX within any rule gets stored, and all the others get silently overwritten...

jtoman · 2026-08-03T21:21:52Z

-        # final-iteration analysis to the report's findings synthesizer. None -> the finding degrades
-        # to property/group text.
-        rec = self._analysis_store.get(rule_name)
+        # final-iteration analysis to the findings synthesizer. None -> the finding degrades to


ditto here; do we want one finding per rule? What if a rule is broken for different reasons across different instantiations?

add findings to the report

e4f01f2

naftali-g requested a review from jtoman July 16, 2026 13:43

jtoman requested changes Jul 16, 2026

View reviewed changes

naftali-g added 3 commits August 2, 2026 11:29

CR

704dd74

remove most sherlock mentions

09f31bc

simplify and review

3d9cb13

naftali-g requested a review from jtoman August 2, 2026 09:54

more CR

d554d56

jtoman reviewed Aug 3, 2026

View reviewed changes

Uh oh!

Conversation

naftali-g commented Jul 16, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jtoman left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants