Monitoring for budget pressure, prover abuse by jtoman · Pull Request #90 · Certora/AutoProver

jtoman · 2026-07-20T20:13:22Z

Uses the monitoring feature of Certora/graphcore#24 to add two monitors:

A prover monitor, which keeps the state of prover tool calls, and tracks whether the agent is "banging its head" against a set of rules. If so, it uses the new "reminder" channel to emit a "nag", urging the agent to either give up or try something new
A budget monitor, which accumulates the total cost of all LLM calls within a given "cost center". If we detect that the task is reaching a budget limit (defined as 80% of the allocated budget) we emit a "wrap it up" message. For verification tasks, we also halt any active feedback agents, and disable all feedback gating (with the idea that it's better to finish under budget with lower quality than blow the budget and return nothing).

Budget cancellation is co-operative, if the agent is overbudget/under budget pressure, it throws a special exception which is interpreted as the appropriate "I give up" type (only for the verification tasks).

As mentioned, there is a per cost center budget and a total "overall run" budget. The sum of cost center budgets does not necessarily have to be the overall budget, in fact, it is expected to be greater. This was chosen over a strict allocation of the total budget to different centers, with some arcane budget rebalancing for unused costs.

As part of this, and as predicted by @shellygr, we have moved the pricing information out of the display subsystem into the llm/ module. We also more accurately track 1hr vs 5m cache costs, as this matters when computing budget pressure.

Adds nudges to the agent to give up/try something new; refuse to run the prover on "let's just try a timeout again" case

jar-ben

Left some comments. The high-level approaches here look good; I think both the budget constraints and the check for "looping over the same prover input" can be helpful (and I think it would solve the real issue we have seen).

jar-ben · 2026-07-21T13:55:21Z

+
+        if len(state['prover_history']) > 0:
+            last_item = state["prover_history"][-1]
+            if last_item["sort"] == "run" and any(i == "TIMEOUT" for (_,i) in last_item) and last_item["spec_digest"] == spec_hash:


Why only timeouts? verified rules, violated rules, sanity failures, .., are also not transient

that's a great point actually.

jar-ben · 2026-07-21T13:57:31Z

+
+        if len(state['prover_history']) > 0:
+            last_item = state["prover_history"][-1]
+            if last_item["sort"] == "run" and any(i == "TIMEOUT" for (_,i) in last_item) and last_item["spec_digest"] == spec_hash:


last_item["spec_digest"] == spec_hash is it possible in the current (or intended future) workflow that the .spec remains the same, but the .conf or .sol files changed? In such situations, a rerun makes sense.

yeah, this assumes the only thing the agent can change is the spec. That's true currently, but will change. we'll have to digest the conf and/or VFS once those changes land.

jar-ben · 2026-07-21T14:12:14Z

+        )
+
+        stuck_rules = {
+            k: v for (k,v) in result.raw_rule_status.items() if v in ("TIMEOUT", "ERROR", "SANITY_FAILED")


"SANITY_FAILED" is sometimes the expected and "right" result, especially for parametric rules/invariants if there is a method that is intended to always revert (in such case, the whole rule/invariant is also flagged with SANITY_FAILED. I am not sure autoprover can currently fix this, and nagging with "You may need to significantly change your approach, or skip the property if this is a persistent issue" might just drop the rule completely.

I'm writing this comment from memory, but I thought there was something here that didn't nag about rules that are expected to fail. If a rule's "correct" outcome is a failure (whether sanity fail or whatever), the agent should mark those rules as expected to fail, which will suppress this nag.

If we don't skip "expected to fail" rules in the nagging, that's something I need to fix.

I just double checked, and we ignore the "expected to fail" state when considering nags; that's a bug

jar-ben · 2026-07-21T14:29:04Z

+    """The author's monitor: budget wrap-up takes precedence; otherwise the
+    usual reminders-channel drain. On the (single) turn the budget warning
+    fires any pending reminders are dropped — moot, since the warning tells
+    the agent to ignore prover/feedback outcomes anyway."""


It might be good to propagate to the reporting part (or at least log) that we dropped validations.

🤦 of course, why didn't I think of this.

ericeil

I like the use of context vars for this; it feels like a good fix for "ambient" data that would be a pain to pass around explicitly everywhere. I left some naive comments, but overall the mechanism looks good to me.

ericeil · 2026-07-21T20:39:23Z

+    later phases."""
+    curr = _cost_centers.get()
+    if curr is not None:
+        raise RuntimeError("Not good")


Should we use a more descriptive message here?

I forgot about this (obvious placeholder) message lol, I'll fix it

ericeil · 2026-07-21T20:57:26Z

+    prev_accum = _budget_accumulator.set(pool)
+    try:
+        yield None
+    finally:


(I'm just learning about @contextmanager now - what an odd convention! - so forgive me if this question is nonsense): isn't the finally implied here? Is this the idiomatic way to write these?

Get ready for a crash course on context managers!

A context manager is just an object which defines two special functions __enter__ and __exit__.

When you write:

with some_context_manager as x:

python calls __enter__ on some_context_manager; the value returned by that function is used to bind to x (roughly, I'm glossing over/partially misremembering some details)

When the context block is exited (normally, or via exception) it calls the special __exit__ method. If there is an exception being propagated, those are passed into the __exit__ function.

So, what does @contextmanager do?

Well, now we need to understand generators. If the keyword yield appears anywhere in a function, python transforms it into a generator object. A generator object exposes three methods, two of which are important to us, send and throw. On the first call to send, the body of the function begins executing up until the first yield statement. When it reaches said yield, execution of the generator suspends, and the yielded value is returned from send(). If you call send(something) on the generator again, something becomes the value returned from the yield expression, and execution of the generator resumes from the yield until the function exits, or another yield is hit.

The eagle eyed reader (which you are) will notice these are just kotlin coroutines; it is left as an exercise to the reader how you could implement generators on top of kotlin coroutines. Fun bonus fact: before async became first class, it was all bolted on top of this generator api.

The dual of send is throw, instead of having the most recent yield return a value, you have it throw the passed in exception.

You can now probably guess how @contextmanager works. It roughly looks like this:

class ContextManagerImpl: wrapped: Generator def __enter__(self): return self.wrapped.send(None) def __exit__(self, exception): if exception: self.wrapped.throw(exception) else: self.wrapped.send(None)

where wrapped is the generator returned by calling the function decorated with @contextmanager. I'm glossing over some details (you can suppress exceptions during __exit__ for example) but this is the basic shape of it.

Now with all that background we can understand why we need finally. Without it, if the with block is exited with an exception, the yield statement in named_budget would throw, and that would immediately terminate any further execution in the body which would in turn skip the cleanup statements. By wrapping the yield in try: ... finally: ... we can ensure that any cleanup we need to do happens even if the with block terminates exceptionally.

TL;DR - isn't the finally implied here? -> No.

Thanks for the explanation!

ericeil · 2026-07-21T20:58:31Z

+    # to — and feels pressure from — the pool directly.
+    prev_accum = _budget_accumulator.set(pool)
+    try:
+        yield None


Is there a difference between yield None and the bare yield you use elsewhere?

no. can fix to be consistent

ericeil · 2026-07-21T21:31:41Z

+
+
+# Pricing tables transcribed from Anthropic + OpenAI rate cards.
+# Sources should be re-checked when new model families ship.


Is there no way to query for the current rates programmatically?

(Oh I see this is existing code copied from elsewhere)

It's a good question, and the answer is: not really. There are 3rd party efforts to catalog this stuff into some standardized format. Might be worth looking into.

…over-monitoring

jtoman added 7 commits July 16, 2026 19:35

Wires in monitoring

b4d01a7

Adds nudges to the agent to give up/try something new; refuse to run the prover on "let's just try a timeout again" case

pricing info moved

7f60a8e

checkpoint

12017e6

checkpoint

c2a4e8a

Pool based accounting

48815ab

Circular import

123622c

Budget aware caching

4769789

jtoman requested review from jar-ben and shellygr July 20, 2026 20:13

jtoman added the autoprover label Jul 20, 2026

jar-ben reviewed Jul 21, 2026

View reviewed changes

take skips into account when determining "stuck" status

5a1dce7

ericeil reviewed Jul 21, 2026

View reviewed changes

jtoman added 3 commits July 22, 2026 11:15

Merge branch 'master' of github.com:Certora/AutoProver into jtoman/pr…

84a5405

…over-monitoring

sync graphcore pin

442b1a8

okay fine, we'll use the old types

28651f7



		# Pricing tables transcribed from Anthropic + OpenAI rate cards.
		# Sources should be re-checked when new model families ship.

Uh oh!

Conversation

jtoman commented Jul 20, 2026

Uh oh!

jar-ben 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!

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!

ericeil 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!

jtoman Jul 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jtoman Jul 21, 2026 •

edited

Loading