Add a prioritized run mode by shellygr · Pull Request #200 · Certora/AutoProver

shellygr · 2026-08-31T16:17:08Z

Why

Today there is nono guaranteed correlation between the effort put by the agent and the value of the output. Property inference fans out per
component, every property it invents gets the full CVL authoring + prover + counterexample
treatment, and budget_integration.md already names formalization the dominant cost. That phase
scales with (components x properties), so an inference agent that thinks of forty properties bills
for forty.

What

Today's behaviour becomes run mode comprehensive and stays the default. prioritized ranks every
candidate property across every component once, then spends the run on the highest-contribution
property plus the properties needed to state or discharge it. One property, pursued properly,
instead of everything pursued shallowly.

Concretely, a prioritized batch is the primary property plus at most two dependencies drawn from
its own component. All three are first-class: the feedback judge demands rules for each, they count
in the report, and all of them are skip-protected. The model does not pick the primary. It scores
every candidate and records what each rests on; priority = score + 15 if critical_match is applied
in code, so property_ranking.json and the property the run actually spends itself on are the same
thing by construction.

The insertion point is one seam in composer/pipeline/core.py, between _extract_all and
staged.begin. That is the first and only point where every component's candidates exist together:
inference never sees more than the unit it was given, and the per-component plugin hook cannot
compare across units either.

How it is turned on

--run-mode prioritized, or AUTOPROVER_RUN_MODE=prioritized.

The value rides on PipelineRun, which the driver and the CVL author both already hold, so
run_pipeline and the backend protocols needed no new parameter.

The ranking is not trusted

A single structured call, cached under the properties namespace, validated in Python before anything
acts on it: every candidate ranked exactly once, no invented keys, and every depends_on naming a
property of its own component. An unusable ranking raises rather than falling back to the whole
candidate set, because a silent widening would spend exactly what this mode exists to save. The
failure is cheap anyway, since nothing has been formalized yet.

The author may not walk away

Two escape hatches would each be a total loss when the run is one property, so both tighten:
record_skip refuses the focus properties, and give_up rejects an exhausted stop until the
prover has actually been run a few times, with the attempts enumerated.

Two escapes are deliberate, and both are the difference between a gate and a deadlock:

sort='environment' is never gated. A missing certoraRun or solc produces no prover run at
all, so a bare attempt floor would be unsatisfiable and would hold the agent against its recursion
limit instead of letting it report a broken toolchain.
The budget monitor's wrap-up lifts the skip protection. Its order is "delete what does not work,
skip the rest, publish", which is exactly what the protection forbids.

The floor counts verify_spec tool calls rather than prover_history. prover_history only grows
when the prover returns a report, and verify_spec returns early with a bare string when the spec
will not type-check, which is the failure most worth escalating through.

The output says what it did not look at

A prioritized report.json would otherwise be indistinguishable from a contract with three
properties. So report.json carries run_mode and the deprioritized properties with their scores
and rationales, coverage carries a deprioritized_count and a warning, the full ranking is written
to property_ranking.json, and job_info.json records the mode on every path including a crash.

What does not get cheaper

prepare_formalization is untouched, so the harness lift,
AutoSetup, custom summaries, structural invariants and the invariant CVL/prover loop cost exactly
what they cost today, as does per-component property inference (it has to run before anything can be
ranked). The saving is the formalization fan-out, which is the dominant cost. Two more caveats: in
--cloud mode components already verify in parallel, so the wall-clock win is smaller than the money
win, and a GaveUp is never cached, so a prioritized run against a genuinely unprovable property is
the worst case for this design.

Scope

Prover flow only. The foundry and rust-app entry points keep their own parsers and do not expose the
flag, because the focus protections live in the CVL author: a prioritized foundry run would get the
narrowing without the discipline, which is the worst of both.

Also in here

FINAL_PROPERTIES_KEY now forks on the mode. Its leaf was fixed apart from the threat-model,
interactive and extra-context parameters, so a prioritized run would have overwritten a
comprehensive run's record for the same component with its one-property batch, and an offline walker
would have read the pruned list as if it were everything inference found.

Testing

tests/test_prioritize.py covers the validation and the cut, including that a supporting property
from another component is rejected and that the selection can never return an empty batch list (the
driver raises on that). tests/test_focus_exits.py covers the gate and the skip protection on
both binding paths, since the author reaches its skip tools either through skip_tools directly
or through property_tools, and a protection on only one is silently bypassable. Driver-level tests
in tests/test_pipeline_staged_formalizer.py prove one batch reaches formalization, that begin
still runs once beforehand, and that the ranker never runs in comprehensive mode.

pytest -m "not expensive": 1126 passed. pyright: 0 errors. The 21 errors in the suite are a local
pgvector testcontainer that will not stay up; they are in test_rag_db / test_indexed_tool and
predate this branch.

Not validated here

The ranker's judgement. The mechanism is tested; whether it picks the right property is what the
first real runs are for, and property_ranking.json is the artifact to read when checking that.

An AutoProver run does the same amount of work regardless of how much the answer is worth. Property inference fans out per component, and every property it invents then gets the full CVL authoring, prover and counterexample treatment. Formalization is usually the dominant cost, and it scales with (components x properties). This adds a second run mode. `comprehensive` is today's behaviour and stays the default. `prioritized` ranks every candidate property across every component once, then spends the run on the highest-contribution property plus the properties needed to state or discharge it. The mode rides on `PipelineRun`, which the driver and the CVL author both already hold, so nothing else needed a new parameter. `--run-mode` sets it, and so does `AUTOPROVER_RUN_MODE`, which means the cloud can turn it on by adding one variable to the Batch job. That is the same route `AUTOPROVER_GLOBAL_PROVER_TIMEOUT` already takes. Ranking is a single structured call between extraction and formalization, cached under the properties namespace. Its output is validated before anything acts on it: every candidate ranked exactly once, primary and supporting all from one component, supporting capped and deduplicated. An unusable ranking raises rather than falling back to the whole set, since a silent widening would spend exactly what the mode exists to save. The author's exits tighten around the focus. `record_skip` refuses the focus properties, and `give_up` rejects an exhausted stop until the prover has actually been run. Two escapes are deliberate. A `sort='environment'` stop is never gated, because a missing certoraRun produces no prover run at all and a bare floor would be unsatisfiable. And the budget monitor's wrap-up lifts the skip protection, since the order it gives requires the skips that protection forbids. The give-up floor counts verify_spec tool calls rather than prover_history. That list only grows when the prover returns a report, and a spec that will not type-check never gets one. The output says what it did not look at. report.json carries run_mode and the deprioritized properties with their scores and rationales, coverage carries the deprioritized count, the full ranking goes to property_ranking.json, and job_info.json records the mode on every path. Scope is the prover flow. The foundry and rust-app entry points do not expose the flag, since the focus protections live in the CVL author. Also forks FINAL_PROPERTIES_KEY on the mode: a prioritized run would otherwise overwrite a comprehensive run's record for the same component with its pruned batch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Four fixes from review, and one deliberate non-change. The ranking model no longer states which property the run pursues. Nothing forced `primary` to be the top of `ranked`, so property_ranking.json could rank A first while the run went after D, with nothing to catch it. Rather than define a priority formula, tell the model to sort by it and then check the arithmetic, the formula lives in code and code does the picking. `primary` and `supporting` come off the schema; each ranked property carries `depends_on` instead, so the winner's dependencies are available without a second call. The artifact and the run's actual subject are now the same thing by construction. Validation got smaller in the process. A cache hit could smuggle a retired focus past every protection. FORMALIZATION_KEY is derived from the property list, so a pruned batch usually forks the cache, but not when the focus is the component's whole list, which a single-property component always is. A replay never runs the author's tools, so the gated give_up and the skip protection do not apply to it, and a prioritized run could return a comprehensive result that had skipped the one property it existed to establish. A hit that does not map every focus property, or that retired one, is now treated as a miss. cache-autoprove could not find prioritized results, and was already wrong twice over. It rebuilt the formalization key from the raw property-inference output with no plugins argument, while the driver writes it from the post-plugin batch plus the contributing plugin ids. Pruning was a third way to disagree. It now reads FinalProperties, which was written for exactly this and had no reader, and falls back to the old path for records from before that entry existed. Three docstrings pointed at composer.meta.run as the offline walker; that module does not exist, so they now name the one that does. Component labels could still collide. Numbering repeats breaks when a component is itself named `Vault (2)`, and the colliding label resolves a ranked property onto the wrong batch. Labels are now suffixed until actually unused, and asserted. MAX_SUPPORTING drops from 4 to 2. Review argued the supporting properties should be author context rather than batch members; they stay first-class, since a dependency that is only suggested is never verified and the primary's proof could then rest on an unchecked assumption. But a batch of five was more than "one property plus what it rests on" ought to mean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

shellygr · 2026-08-31T20:39:48Z

Claude answers:

Four of the five are right and are fixed in b89217b. One I have pushed back on, with the part of it that was fair taken.

1. The selected primary is not derived from the ranking. Agreed, fixed, though not quite as proposed.

The bug is real: nothing forced primary to be the top of ranked, so property_ranking.json could rank A first while the run pursued D.

The recommendation was a combined priority score, validated ordering, and primary = ranked[0]. The formula has to exist either way, so rather than define it, tell the model to sort by it, and then check the model's arithmetic, the formula now lives in code and code does the picking:

CRITICAL_MATCH_BONUS = 15
def priority(rp): return rp.score + (CRITICAL_MATCH_BONUS if rp.critical_match else 0)

primary and supporting are off the schema entirely. Each ranked property now carries its own depends_on, which is what keeps this to one LLM call: the model cannot name dependencies for a primary that code has not picked yet. select takes max(ranked, key=priority) and reads that entry's dependencies. Disagreement is now unrepresentable rather than merely detected, and validate_ranking got shorter.

2. Cache hits should be checked for focus compatibility. Agreed, and this was worse than P2.

Right, and the consequence is sharper than the finding says. A replay never calls formalize, so none of the focus protections apply to it: not the gated give_up, not the skip protection, not the rewritten prompt. A prioritized run could therefore return a comprehensive result that had skipped the one property it existed to establish, with exit code 0 and nothing proved.

Implemented as recommended. _focus_satisfied checks that every focus property is mapped to at least one check and none was retired, using property_checks() and skipped off BackendResult, so it is backend-agnostic. A hit that fails is treated as a miss and re-formalized. It cannot loop: the live tools refuse to retire the focus, and the one path that overrides them is a budget wrap-up, which yields Curtailed and is never cached.

3. Cache inspection cannot locate prioritized results. Agreed, and it is broader than reported.

cache_autoprove.py rebuilt the key as FORMALIZATION_KEY(GeneratedCVL, bug_cache.items) with no plugins argument, while the driver writes it from batch.props and contributing_plugins. Those already disagreed on master in two ways before this branch existed: batch.props is post-POST_PROPERTY_KEY plugin rewrites, and a contributing plugin adds a suffix. Pruning was a third.

Fixed exactly as recommended: _resolve_formalization_key reads FINAL_PROPERTIES_KEY (mode-parameterized) and keys off final.items + final.tool_plugins, falling back to the bug-analysis path for older records. Worth noting FinalProperties was written for precisely this and had no reader anywhere in the repo, and AutoProveCacheTags.run_mode was write-only; both now have one. Also fixed three docstrings pointing at composer.meta.run as the offline walker, which does not exist and never did.

4. Five properties instead of one. Pushing back on the reframing, taking the magnitude.

This one re-litigates a decision that was made deliberately. The design question was put explicitly and "top-1 plus its supporting cluster" was chosen over "exactly one property", with the batch specified as 1..k. So the behaviour matches intent rather than drifting from it.

On the merits: a dependency handed to the author as context is never verified, so the primary's proof could rest on an unchecked assumption. Keeping the supporting properties first-class means the judge demands rules for them and they are skip-protected, which is the point of pulling them in at all.

What is fair in the finding is the magnitude. "One property plus what it rests on" should not quietly mean five, so MAX_SUPPORTING drops from 4 to 2. A prioritized batch is now the primary plus at most two dependencies, and the PR body says so rather than leaving it to be inferred.

5. Generated component labels can collide. Agreed, fixed.

Confirmed by construction: ["Vault", "Vault", "Vault (2)"] produced Vault, Vault (2), Vault (2). Since by_key is a dict, one entry shadowed the other and select took whichever came first.

unit_index is the real identity, as noted. Rather than restructure the key, which would cost the PropertyKey alignment shared with the report and the grouping model, labels are now suffixed until actually unused and asserted unique, so the label is an identity by construction. Test covers the pathological input.

pytest -m "not expensive": 1133 passed. pyright: 0 errors. The 21 errors in the suite are a local pgvector testcontainer that will not stay up; they are in test_rag_db / test_indexed_tool and predate the branch.

Finding 3 is the one the suite cannot really cover, since it walks a live LangGraph store. Verifying that one by hand against a prioritized run and an existing comprehensive run.

…mode

jtoman · 2026-09-01T18:58:00Z

+    return f"Giving up on {label}: {p['reason']}"
+
+
+def _verify_attempts(state: dict) -> int:


you can do better on this type I think

Claude answers: done

jtoman · 2026-09-01T18:58:38Z

+@tool_family(GiveUpParams)
+class GatedGiveUp(
+    WithInjectedId,
+    WithInjectedState[dict],


ibid, this is a weak sauce type bound.

Claude answers: done

jtoman · 2026-09-01T18:59:38Z

+                return tool_state_update(
+                    self.tool_call_id,
+                    f"Rejected: you have run the prover {ran} time(s) on this task, and this run "
+                    f"requires at least {floor} before a property may be abandoned. This is the "
+                    "one property the run exists to establish. Decompose it into lemmas, add or "
+                    "strengthen a harness, or formalize a weaker core of it and state the gap — "
+                    "then verify. If the toolchain itself is broken, stop with "
+                    "sort='environment' instead.",
+                )


for this, its my preference to make the return type of the tool be str | Command. And then do return "Error message" on the error path. It's more explicit about which branches are updating state and which are "oopsie didn't work"

Claude answers: done

jtoman · 2026-09-01T19:03:41Z

+def gated_give_up_tool(
+    *,
+    name: str,
+    description: str,
+    label: str,
+    min_attempts: int,
+    reason_description: str = "The reason for giving up on your task",
+) -> BaseTool:


tioli, I prefer to make the dependencies of the state of a tool like this explicit. You can do this with:

class GatedGiveUpDeps(TypedDict, MessagesState): result: ReadOnly[str] failed: ReadOnly[bool] class gated_give_up_tool[T: GatedGiveUpToo]( *, ..., state_ty: type[T] ) -> BaseTool: return GatedGiveUp[state_ty].with_template(...)

Claude answers: not done as sketched. The state type is now GatedGiveUpState rather than dict, but the generic parameter does not survive the tool_family decorator: it returns an already-specialized _TemplatedTool, so GatedGiveUp[state_ty] is a pyright error.

I think GatedGaveUp.with_template(...)[t] might work? I honestly forget; but I think eric used parametricity and tool families successfully.

Claude answers: done. You were right, the subscript just has to come after with_template rather than before it. The state type is SourceCVLGenerationState now, so failed turned out to be bool | None and required.

jtoman · 2026-09-01T20:05:34Z

    threat_model_digest: str | None,
    with_refinement: bool,
    extra_context_digest: str | None = None,
+    run_mode: str = "comprehensive",


literal type, remove the default.

Claude answers: done

jtoman · 2026-09-02T06:05:49Z

+  - `score`: 0-100, how much *proving it* would raise confidence in the overall correctness of the
+    system. Score importance, not difficulty.


There is absolutely no scale provided here. Any ordering within 0-100 provides information for relative positioning I suppose, but what does a score 100 look like? 5? 25? Are we fine just leaving that up to the agent?

Claude answers: done. Anchored with a scored example at each level.

jtoman · 2026-09-02T06:06:50Z

+  - `depends_on`: the properties from the SAME component that would be needed to state or discharge
+    this one — the lemmas it assumes, the invariants its argument leans on. Only the run's chosen
+    property has its dependencies pursued, and only the first {{ max_supporting }} of them, so put
+    the ones the proof genuinely cannot do without first. A property that is merely *related* is
+    not a dependency; leave it out.


see my comments elsewhere about my dubiousness around the utility of what we're asking for here. There is a sort mismatch here in what we're telling it to find within "depends on".

Claude answers: done

jtoman · 2026-09-02T06:07:31Z

+  W1. Its violation is a real loss — funds, access, or an accounting identity — not a cosmetic
+      deviation.


"real loss"

It is at this point, I realize we've never even told the agent this is for a Web3/Defi protocol. So it has no idea what we're talking about here.

with how tied we are to solidity I don't think this is not sensible

Claude answers: done

jtoman · 2026-09-02T06:07:51Z

+WHAT MAKES A PROPERTY WORTH THE RUN:
+  W1. Its violation is a real loss — funds, access, or an accounting identity — not a cosmetic
+      deviation.
+  W2. It constrains behaviour across many entry points rather than one narrow path.


Commounweaulth speulling jump scaure.

But also, what does this mean? This sounds like you're asking for "cross cutting", but I'd argue that's not a really important metric. A rebalanceShares function that is called in one entry point is probably the most important in the whole contract.

Claude answers: done

Claude answers: done. Dropped.

jtoman · 2026-09-02T06:09:35Z

+    not a dependency; leave it out.
+  - `rationale`: one or two sentences. Say what breaks if the property does not hold.
+
+WHAT MAKES A PROPERTY WORTH THE RUN:


what run! this is the first time you've mentioned a "run"

Claude answers: done

The ranking read nothing that pre-formalization produces, but it waited for all of it anyway. On a RiverV1 run that meant four hours of autosetup and structural invariant proving before the run made the one decision the mode exists to make, with a single invariant prover job accounting for two of those hours. The extracted batches and the guidance documents are what the ranking needs, and both are in hand the moment extraction lands. Moving it ahead of the await also puts the focus in hand before the setup finishes, which is what a setup step would need to aim at it. The empty-batch check stays where it was, after the await. Raising it earlier would let "no properties extracted" mask a setup that failed, which two of the overlap tests rightly caught. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Review found that the "supporting lemmas" idea was not one. A property that follows from another is not something this pipeline models, the property agent is told not to write them, and what the field would actually have collected is "these are important too". So the ranker now groups candidates into claims and the run pursues the group holding the highest-scoring property. Grouping is a shape the report already asks a model for and gets, unlike a dependency graph with no cycle check and nothing to say about indirect dependencies. The ranking prompt is rewritten against its sibling, property_analysis_system_prompt.j2. It never said the subject was a Web3 protocol, never explained what a run or a verification budget was, and asked for scores on a 0-100 scale it never anchored, which also left the flagged-concern bonus measured against nothing. It now opens on the domain, says where the work sits, and anchors the scale with scored examples. Two bits of advice come out of the author prompt. Telling a stuck agent it may add a `require` that rules out unreachable states reads as licence to assume away the states where the property is interesting, which is the opposite of the training this thing has had. What remains is decompose or weaken honestly, with weakening tied to the rule that a property saying nothing is a failure rather than a result. The focus protection read an in-memory flag that the budget monitor flipped. It was not checkpointed, so a resumed session could have the flag and the state disagreeing about whether the run was wrapping up. It reads `budget_curtailed` from the state now, which is where that was recorded all along. The field is optional on the shared state: only the prover and foundry authors have a budget, and natspec and rustapp share the tool. Also: the retry replays the rejected ranking, without which the model was asked to fix something it had no memory of producing; validation reports every problem at once rather than one per attempt; component labels carry the unit index, so two components sharing a name need no invented suffix; and the give-up gate takes a real state type instead of `dict`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

jtoman

much better imo

jtoman · 2026-09-02T17:31:46Z

+def gated_give_up_tool(
+    *,
+    name: str,
+    description: str,
+    label: str,
+    min_attempts: int,
+    reason_description: str = "The reason for giving up on your task",
+) -> BaseTool:


I think GatedGaveUp.with_template(...)[t] might work? I honestly forget; but I think eric used parametricity and tool families successfully.

jtoman · 2026-09-02T19:10:27Z

+    if batches and run.run_mode is RunMode.PRIORITIZED:
        with named_budget_or_nop("property_extraction"):
            batches, deprioritized = await _prioritize(
                backend.analysis_spec.properties_key, backend.artifact_store,
                batches, run, phases["extraction"], threat_model, extra_context,
            )

+    staged = await staged_task
+    if not batches:
+        raise ValueError("No properties extracted from any component.")


run in parallel imo

Claude answers: not done. It already overlaps: staged_task is a live task started before extraction, so the setup keeps running while the ranking waits on its model call. Gathering them explicitly reads better but changes nothing at runtime, and the fuller version breaks two tests that pin this pair as overlapped-but-not-gated.

The tool family does take a type parameter, with the subscript after the render rather than before it. GatedGiveUp is generic in its state again, and the CVL author names SourceCVLGenerationState at the bind site, so the fields the gate reads and the surrender records are checked against the state it actually runs on instead of a bound that merely happened to be satisfied. Matching the real state meant `failed` is `bool | None` and required, not an optional `bool`. The test state was seeding neither, which the bound now catches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…mode

shellygr and others added 2 commits August 31, 2026 19:16

Merge remote-tracking branch 'origin/master' into shelly/prioritized-…

7dfe0bb

…mode

jtoman requested changes Sep 2, 2026

View reviewed changes

shellygr and others added 2 commits September 2, 2026 11:35

shellygr closed this Sep 2, 2026

shellygr reopened this Sep 2, 2026

shellygr added the autoprover label Sep 2, 2026

jtoman approved these changes Sep 2, 2026

View reviewed changes

shellygr and others added 2 commits September 2, 2026 23:41

Merge remote-tracking branch 'origin/master' into shelly/prioritized-…

9a71323

…mode

		return f"Giving up on {label}: {p['reason']}"


		def _verify_attempts(state: dict) -> int:

		- `score`: 0-100, how much proving it would raise confidence in the overall correctness of the
		system. Score importance, not difficulty.

		W1. Its violation is a real loss — funds, access, or an accounting identity — not a cosmetic
		deviation.

Uh oh!

Conversation

shellygr commented Aug 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why

What

How it is turned on

The ranking is not trusted

The author may not walk away

The output says what it did not look at

What does not get cheaper

Scope

Also in here

Testing

Not validated here

Uh oh!

shellygr commented Aug 31, 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!

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!

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!

Reviewers

Assignees

Labels

shellygr commented Aug 31, 2026 •

edited

Loading