CVLR: classify rule verdicts and allow expected failures by ericeil · Pull Request #280 · Certora/AutoProver

ericeil · 2026-10-23T22:51:00Z

In current master, CVLR rules that don't verify are always treated as unfinished work. This PR classifies each verdict (the rule's own assertion failed, the Prover stopped on an assertion it generated, timeout, error, no verdict, etc.) and lets authors mark a rule as an expected failure, with a reason. The draft is stamped only when every unmarked rule verifies and every marked rule fails on its own assertion.

Each run also reports the functions the Prover treated as external, taken from the job's alert report. An external call may be modeled unsoundly by the Prover, so the author is told which functions those are.

Why is this needed?

The CVL backend already supports expected failures, but it never needed the rest. Autosetup turns optimistic_loop on for CVL, so loop-unwinding assertions don't appear. The EVM Prover has no counterpart to the Solana Prover's Cannot overflow assertion. And an unresolved EVM call is havoced, which is sound. The Solana Prover tells us more through assertions it adds itself and through its alert report: whether a rule actually reached its property, and which calls it modeled as writing nothing. Without reading both, we can't tell a real violation from a check that never finished, or a sound verdict from one that depends on an external call.

Where to start

How the stamp is decided. unaccounted and accounted_for (composer/spec/cvlr/verify.py) decide whether a run's verdicts are accounted for under the current markings. LastVerdicts (composer/spec/cvlr/state.py) keeps the last run's verdicts so verify_rules can judge them again.
What the author sees after a run. VerifyRules._report (composer/spec/cvlr/verify.py) turns a prover run into notes for the author, rendered from composer/templates/cvlr/verdicts.j2, and decides the stamp. Tests are in tests/test_cvlr_verify.py.
How a violation is classified. classify_violation (composer/prover/ptypes.py) reads the Prover's assertOrigin. Tests are in tests/test_assert_origin.py and tests/test_solana_cex_trace.py.

How the pieces fit

Expected failures. When a rule fails because the program really breaks the property, the author calls expect_rule_failure with a reason, and expect_rule_passage withdraws the mark. The tools only record the marking; a rule can be marked before any run shows its failure. A marked rule is accounted for only in a run where it is VIOLATED on its own assertion, so a marked rule that later verifies, or that stops on a Prover-generated assertion, blocks the stamp. Tests are in tests/test_cvlr_expected_failures.py.

Re-judging the last run. This works the way CVL's gate does. CVL's collect_results re-reads the prover history under the current markings; CVLR's verify_rules checks LastVerdicts first. When that run is of the current draft and is accounted for under the current markings, verify_rules stamps without submitting. Otherwise it submits, and one check, accounted_for, decides the stamp for the fresh run too. LastVerdicts.draft leaves the markings out, because they change how a run is judged, not which run it was.

Markings are part of the verdict stamps. A verdict passes only under the markings, so the stamps of every gate that reports check verdicts now hash the names of the marked checks (make_verdict_stamper in composer/authoring/state.py): CVLR's prover stamp, foundry's forge_test, rustapp's validate, and each CVL buffer's prover stamp (that buffer's own rules only). Changing a marking after a green run makes those stamps stale the same way an edit does. Feedback and compile stamps leave the markings out, because judges aren't shown them and a build doesn't depend on them. check_completion now takes the session's stampers and compares each required key against what its own stamper would stamp now. merge_validation and merge_expected_failures are unchanged from master. This affects every backend.

Prover-generated assertions. The Prover reports where each violated assertion came from as assertOrigin in the rule output: "user", a kind of assertion it generated, or null. classify_violation turns that into a PropertyViolation or an IncompleteCheck:

A Prover limit (loop unwinding, Cannot overflow, an unresolved CPI, a recursion or hashing bound, ...) is an incomplete check. It says nothing about whether the property holds, so it can't account for a marked rule. panic and memcpyOverlap check the program itself, so they stay property violations.
A kind this version doesn't know is treated as an incomplete check and logged, so a new Prover limit can't become a finding unnoticed.
null, or a missing key, is read as the rule's own assertion. The CVL pipeline runs on the pinned certora-cli release, which predates the key and doesn't classify violations. CVLR runs with prover_version master; the release it pins before shipping must report assertOrigin.

ProverReport.incomplete carries the classified incomplete checks. The report gives the author specific advice for the two kinds they'll meet most. For loopUnwinding (a loop needed more iterations than loop_iter unrolls), CVL's autosetup picks a bound and turns optimistic_loop on before authoring (_find_optimal_loop_iter in certora_autosetup/setup/sanity.py), while this gate starts at loop_iter 2 with optimistic_loop off and the author raises the bound with adjust_prover_config. For cannotOverflow (under -solanaTACSoundSignedMath, the Prover couldn't show that an expression it treats as a pointer stays below 2^64), the fix is usually to bound a value the rule read from account data. For other kinds, the Prover's own message carries the advice.

The two recorded vault fixtures under tests/data/solana_cex got assertOrigin added by hand (see the README there); tests/data/solana_cex/assert_origin/ holds unedited output from the new Prover.

External functions. For cloud runs, the job's alert report is fetched with the job link's anonymous key, the same way the status poll reads the job, and parsed in memory (_fetch_alert_report in composer/prover/cloud.py, parse_alert_report in composer/prover/results.py). Local runs parse the file the Prover wrote. ProverReport.alerts carries the whole report. external_warnings (composer/spec/cvlr/externals.py) picks out the Prover's warnings about functions it neither inlined nor summarized, which only Solana runs raise, and verify_rules shows them to the author. A job with no alerts has no report. A report that couldn't be fetched or read is reported as such, not as a run with no external functions. Neither case fails the run. Tests are in tests/test_prover_alert_report.py and tests/test_cvlr_externals.py.

Testing

uv run --no-sync pytest tests/ -m "not expensive" (2000 passed) and pyright (0 errors) pass. The new tests need no cargo, network, or model.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…d for A rule that did not verify is not always unfinished work. It may expose a real defect, it may have stopped on an assertion the prover generated, or the report may have given it no verdict. The gate now tells these apart and stamps when every rule the build listed is accounted for. - LastVerdicts records the last run. expect_rule_failure and expect_rule_passage mark a rule whose own assertion failed, and re-decide the stamp against that run (unaccounted, stamp_under) without another submission. A run that is not accounted for withdraws a stamp of the same draft. - ProverReport carries the incomplete checks (LoopUnwound, OverflowUnproven, from classify_violation) and the Prover's external-function warnings from the job's alert report. - verify_rules' report names incomplete checks with advice, external functions, rules with no verdict, and expected failures that verified, from templates. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…report could not be fetched - unaccounted counts a marked rule that VERIFIED, so the stamp waits until the rule is fixed or the marking is withdrawn. expected_verified.j2 says so. - expect_rule_failure and expect_rule_passage tell the model not to call them in parallel: each decides the stamp as if it were the only marking. - expect_rule_passage on a rule that is not marked changes nothing and says so. - The alert-report fetch returns its outcome. A 404 is a job with no alerts; any other failure is UnreadableAlertReport rather than an empty list. cloud_results and _local_results yield FetchedResults to carry it. - State stores ExternalWarnings | UnreadableAlertReport instead of a None sentinel. - The verify_rules notes render through TypedTemplate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…lter is CVLR's The "neither inlined nor summarized" alert comes from the Prover's SBF inliner, so only Solana runs raise it. ProverReport and FetchedResults now carry the whole alert report (AlertReport, or UnreadableAlertReport), and composer/spec/cvlr/externals.py picks the external-function warnings out of it for the CVLR verify gate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…n is CVLR's "Unwinding condition in a loop" comes from the Prover's shared loop unroller, but "Cannot overflow" comes from the SBF sound-signed-math pass. run_prover classified both on every app, so an EVM rule asserting with a "Cannot overflow" message would have been taken for a Prover limit. ProverReport now carries each violated instance's assertion text (violated_assertions). ptypes keeps LoopUnwound and a classify_assertion that takes the table of generated assertions. OverflowUnproven and the CVLR table move to composer/spec/cvlr/incomplete.py, which the verify gate uses to decide which rules are incomplete. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

… constraint Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

merge_validation had no way to delete a key, so a withdrawn prover stamp was written as "" and only failed the gate because "" never equals a digest. merge_expected_failures read an empty reason as an unmarking. Both reducers now take None as the deletion, and the CVLR, foundry and rustapp tools that withdraw a stamp or a marking send it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The agent has no idea what the "sound-math pass" is; say instead that the Prover adds this check on its own, rather than the rule asserting it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

jtoman · 2026-10-28T18:58:27Z


-def merge_validation(left: dict[str, str], right: dict[str, str]) -> dict[str, str]:
+def merge_validation(left: dict[str, str], right: Mapping[str, str | None]) -> dict[str, str]:
+    """State reducer for validation stamps. A ``None`` withdraws the stamp under its key."""


I'm confused by this. Validations don't need to be withdrawn; not really. They are "withdrawn" in effect by simply changing the state that is hashed to give the current state. I'm trying to think of when you'd want to withdraw validation without just changing the dependent state, and can't. Can you explain?

As discussed in Slack, this was because we didn't include the expected failures in the hash, in any backend. I added a commit to fix this everywhere.

jtoman · 2026-10-28T19:04:37Z


    @override
    async def run(self) -> Command:
-        # Empty reason = remove the marking (see _merge_expected_failures).


So, for context, the reason I didn't do this is because a reducer typically has the type (A, A) -> A. This has type (A, B) -> A, to wit, A = dict[str, str] and B = dict[str, str | None]. I truly don't know whether langgraph's internals assume our reducers have the (A, A) -> A type or will tolerate (A, B) -> A type. For example, suppose we have a state channel like foo: NotRequired[dict[str, str]]. We then write {"blah": None}, but "foo" doesn't yet appear in the state. What happens? Is this an error? Is the reducer skipped, and now we have a dict[str, str | None] sitting in a state field that claims a different type?

I'm not claiming the above can or will happen, just that langgraph's documentation is so crap I don't know. Keeping uniform types is always safe though. We might be able to reason that "oh, whenever we write into this state channel, there is always an extant value, so the reducer definitely fires, so the 'wrong' type never hits the state (it's caught by the reducer)". That's fine I guess, but I'd prefer if we did a deep dive on the langgraph source/documentation to confirm that this is going to work and (more preferably) is documented as a "good" idiom.

Ok, yeah, that makes sense. I also could not find any documentation that supports this usage, so I'll change it back and add a comment so we don't rehash this later.

jtoman · 2026-10-28T19:07:40Z

+    """
+    try:
+        text = await asyncio.to_thread(
+            _results_api().fetch_output_file, job_id, ALERT_REPORT.name


wHy NoT mAkE iT aSynC

-- John, probably

Wow, I really thought I'd already fixed that...

jtoman · 2026-10-28T19:15:56Z

+    target = dest / ALERT_REPORT
+    target.parent.mkdir(parents=True, exist_ok=True)
+    target.write_text(text)
+    return read_alert_report(dest)


This is so weird right? You have some python code with the text of the report in memory. You write it out to disk at some magic path under dest, then call a function which ... reads the text from that file back into memory with our fingers crossed hope that it uses the same path. Am I losing my mind? Why do this? You can pass strings in python?? IIRC, all of these files are in a temp directory anyway, so the claim of "oh we want to look at the reports after the run" doesn't seem to hold up???

Yeah, this is some historical leftover BS. Fixing...

jtoman · 2026-10-28T19:16:32Z

        # them in the same layout the archive had, so the parse is unchanged.
        await _fetch_results(cloud_job.job_id, dest)
-        yield (dest, runtime_ms)
+        alerts = await _fetch_alert_report(cloud_job.job_id, dest)


it IS in a temp dir??? So yeah, you're passing a string argument through a filesystem op.

jtoman · 2026-10-28T19:51:08Z

@@ -0,0 +1,3 @@
+These rules are marked as expected failures but VERIFIED: {{ names }}. Either the defect is not there, or the rule does


This is an annoying nit, but this is a pretty weird way to compose templates; render a bunch of them and then stitch them together instead of... conditionals and loops and whatever in some "report" template. Why this scattershot approach?

Yeah, this made more sense when it was all in Python strings. I moved it to templates without reorganizing it. Should be better now.

jtoman · 2026-10-28T19:52:14Z

+
+_GENERATED: tuple[tuple[str, type[GeneratedAssertion]], ...] = (
+    *GENERATED_ASSERTIONS,
+    ("Cannot overflow", OverflowUnproven),


Not to belabor the point, but this will fire on something like:

cvlr_assert!(user_balance < total_balance, "Cannot overflow: user balances")

contrived, sure, but my point stands I think...

jtoman · 2026-10-28T19:53:38Z

+    if last is None or rule not in last.status:
+        return (
+            f"{rule} has no verdict yet. Mark it only after a run reports that the rule's own "
+            "assertion failed."
+        )


So, this is kind of pointless ceremony imo. I have seen many times AP write a rule that it knows a priori will fail, because it "hand traced" a bug.

jtoman · 2026-10-28T19:54:43Z

+    if last.status[rule] != "VIOLATED":
+        return (
+            f"{rule} is {last.status[rule]}. Only a rule whose own assertion failed can be "
+            "marked as expected to fail."
+        )


I'm confused why this is checked here. The CVL side (I believe) requires that expected_to_fail rules have status == "VIOLATED". I'm just not sure what this provides besides making the agent jump through hoops before it can do its state bookkeeping. I am open to convincing ofc.

jtoman · 2026-10-28T19:55:37Z

+def _remarked(
+    state: CvlrGenerationState, tool_call_id: str, said: str, marking: dict[CheckName, str | None]
+) -> Command:
+    """Apply ``marking`` and re-decide the prover stamp against the last run's verdicts."""
+    last = state.get("last_verdicts")
+    if last is None:
+        return tool_state_update(tool_call_id, said, expected_failures=marking)
+    stamp = stamp_under(last, merge_expected_failures(state["expected_failures"], marking))
+    current = prover_stamper()(state, tuning_history(state))
+    held = state["validations"].get(PROVER_VALIDATION_KEY) == current[PROVER_VALIDATION_KEY]
+    if stamp == current and not held:
+        said += (
+            " Every verdict the last prover run reported is now accounted for, so this draft is "
+            "stamped without another run."
+        )
+    elif stamp != current and held:
+        said += (
+            " The last prover run's verdicts are no longer all accounted for, so this draft's "
+            "prover stamp is withdrawn."
+        )
+    return tool_state_update(tool_call_id, said, expected_failures=marking, validations=stamp)


As stated elsewhere, I hate this, and I don't think trying to support this "observe failures, mark failure, get stamp" workflow is worth it (as stated elsewhere, the draft almost always changes with marked failures, so a prover rerun is required anyway...)

reworking this

A verdict passes only under the markings, but no stamp's hash covered them. Changing a marking after a green run left a stamp that the current markings no longer justified. The CVL backend kept that stamp, and CVLR deleted it by hand through a None in merge_validation. The verdict stamps now hash the names of the marked checks: CVLR's prover stamp, foundry's forge_test, rustapp's validate, and each CVL buffer's prover stamp (only that buffer's own rules). A changed marking makes those stamps stale the same way an edit does, so merge_validation goes back to a plain update and CVLR no longer withdraws stamps. Feedback and compile stamps leave the markings out, because the judges are not shown them and a build does not depend on them. check_completion now takes the session's stampers and compares each required key against what its own stamper would stamp now. CVLR's LastVerdicts keeps the run's hash without the markings, so a marking change can still stamp from the last run without a new submission. In the CVL backend the hash in prover_history stays marking-free, because it identifies the run. submit_buffer writes the stamp when a marking has completed a buffer, but not while any of that buffer's results are still uncollected. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Fetching the report called the synchronous results client on a worker thread, then wrote the body into the temporary results directory and read that file back. The job link's anonymous key already authorizes the read, the same way the status poll does, so the fetch is an aiohttp GET and the body is parsed in memory. The report comes back on FetchedResults. A local run still reads the file the prover wrote, through the same parser.

LangGraph types a reducer as (Value, Value) -> Value. expected_failures stores dict[CheckName, str], so the update has to be that same map. An empty reason removes a marking. The marking tools reject an empty reason, and the CVLR, foundry, and rustapp unmark tools write one.

expect_rule_failure refused a marking unless the last run reported the rule VIOLATED on its own assertion. The stamp already enforces that: unaccounted counts a marked rule as accounted for only in a run where it fails on its own assertion. So the refusal guarded nothing, and it cost an extra round-trip whenever the author had traced a defect before running the rule. It also read the last verdicts without checking the draft digest, so a stale run's verdict could satisfy it. The incomplete-check note now says a marking does not account for such a rule, since the rule may already be marked when the note appears. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The marking tools decided the prover stamp themselves: each re-judged the last run under the new markings and wrote or withdrew the stamp. CVL's marking tools only record. Its gate re-reads the prover history under the current markings, so a marking after a failing run is stamped by the next collect_results without another run. CVLR now works the same way. expect_rule_failure and expect_rule_passage only record the marking, and the marked prover stamp goes stale on its own. verify_rules keeps the last run's verdicts, keyed by the draft without the markings. When that run is for the current draft and every rule is accounted for under the current markings, verify_rules stamps without submitting. One check, accounted_for, decides both that case and a fresh run. CVL's submit_buffer goes back to master's reply with no stamp, so collect_results is again the only place it stamps. CVL's only change from master is that the prover stamp covers the buffer's own markings. CVLR still accounts for a marked rule only when it is VIOLATED on its own assertion, where CVL forgives any status. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The Prover now reports where a violated assertion came from as assertOrigin in each rule's output: "user", a kind of assertion it generated itself, or null. Classify from that instead of matching the assertion message against a list of prefixes, which a rewording in the Prover would silently break. - A Prover limit (loop unwinding, Cannot overflow, an unresolved CPI, a recursion or hashing bound, ...) is an incomplete check. panic and memcpyOverlap check the program itself, so they stay findings. - A kind this version does not know is still generated: it is an incomplete check and is logged, so a new Prover limit cannot become a finding unnoticed. - null is read as the rule's own, as an unrecognized message was. - A missing key reads the same as null. The CVL pipeline runs on the pinned certora-cli release, which predates the key, and does not classify violations; refusing the output would fail every CVL run with a violation. CVLR runs with prover_version master on staging, and the release it pins before shipping (U25) must report assertOrigin. ProverReport carries the classified incomplete checks rather than the raw messages, and composer/spec/cvlr/incomplete.py goes away. The two recorded vault fixtures get assertOrigin added by hand (see their README); assert_origin/ holds unedited outputs from the new Prover. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…g about the program A loop-unwinding stop does say the loop can iterate past the bound. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

verify_rules rendered six templates, one per kind of note, and joined the results in Python. cvlr/verdicts.j2 now holds them all, each behind its own condition, and _report fills one parameter set. The "every rule is accounted for" line moves into it as well, so it now comes before the external-functions note rather than after it. The rule lists the template takes are named for what they hold: marked_verified (formerly surprising), property_failures, unfinished. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

jtoman

a couple of TIOLI nits that shouldn't block merging. thanks for the iteration, this version is vastly better.

jtoman · 2026-10-30T18:01:59Z

-    state: AuthoringExtra,
+def check_completion[S: AuthoringExtra](
+    state: S,
+    stampers: Iterable[ValidationStamper[S]],


oh! this is a really cute idea. I love it.

jtoman · 2026-10-30T18:05:11Z

+async def _fetch_alert_report(job: CloudJob) -> AlertReport | UnreadableAlertReport:
+    """The job's alert report (:func:`composer.prover.results.parse_alert_report`).

-    A job with no alerts has no report. A fetch that fails otherwise does not fail the run: the
-    verdicts stand without the report.
+    Read with the link's anonymous key from the job host (:attr:`CloudJob.alert_report_url`), the
+    same way :func:`poll_job` reads the job. A job with no alerts has no report (HTTP 404). A fetch
+    that fails otherwise does not fail the run: the verdicts stand without the report.
    """
    try:
-        text = await asyncio.to_thread(
-            _results_api().fetch_output_file, job_id, ALERT_REPORT.name
-        )
-    except JobNotFoundError:
-        logger.info("Cloud job %s has no alert report", job_id)
-        return AlertReport()
+        async with aiohttp.ClientSession(headers=_NO_BROTLI_HEADERS) as session:
+            async with session.get(
+                job.alert_report_url, timeout=aiohttp.ClientTimeout(total=30)
+            ) as resp:
+                if resp.status == 404:
+                    logger.info("Cloud job %s has no alert report", job.job_id)
+                    return AlertReport()
+                if resp.status != 200:
+                    raise RuntimeError(f"HTTP {resp.status}")
+                text = await resp.text()
    except Exception as exc:  # noqa: BLE001 — a missing report does not fail the run
-        logger.warning("Cloud job %s: fetching the alert report failed (%s)", job_id, exc)
+        logger.warning("Cloud job %s: fetching the alert report failed (%s)", job.job_id, exc)
        return UnreadableAlertReport()


oh, sorry, I was fine with you doing async to_thread, POU isn't async supported, so I was joking about my irritating nitpickiness about async-ness. This is fine I guess! but honestly I think it's probably better to revert it maybe so we just have one source of truth around "how to fetch output results"

will restore this

jtoman · 2026-10-30T18:06:31Z

+
+@dataclass(frozen=True)
+class UnknownKind:
+    """A kind of generated assertion that a newer Prover names and :class:`GeneratedKind` does not."""


smart, these will 100% drift so planning for that is a good call

jtoman · 2026-10-30T18:07:24Z

+    """The Prover did not say where the assertion came from.
+
+    The built-in rule checkers' assertions are reported this way, as are generated assertions the
+    Prover has not given a kind.


so UnknownKind is for when we get a kind, we just can't map it to GeneratedKind. Unclassified is when the prover output lacks any kind of classification? I'm not mad about this, just trying to understand the distinction

Yep, that's right

jtoman · 2026-10-30T18:08:15Z

+    The check did not finish, so it says nothing about whether the rule's property holds. Show it to
+    the author. Do not record it as a finding. It can still say something about the program: an
+    unwinding stop means some loop can run past the bound. ``assertion`` is the Prover's message,
+    which carries its own advice.


apropos nothing, I'm not sure why these comments are phrased as instructions? They don't make it into the output/input schema of any tool... right?

Yeah, it's just a weirdly-phrased comment.

jtoman · 2026-10-30T18:10:59Z

+        case str(kind) if kind in GeneratedKind:
+            return GeneratedAssertion(GeneratedKind(kind))
+        case str(kind):
+            _log.warning("the Prover reported a kind of generated assertion not in GeneratedKind: %s", kind)


This isn't your problem and is well beyond the scope of this PR, but I would like to have some principled way of collecting these kinds of "uh, hey you guys might want to take a look at this" messages instead of having them languish unseen in some logstream/cloudstream whatever.

Yeah, agreed.

jtoman · 2026-10-30T18:18:15Z

+            return tool_state_update(
+                self.tool_call_id,
+                "The last prover run of this draft is accounted for under the current markings, "
+                "so nothing was submitted. This draft is stamped.",
+                validations=_PROVER_STAMPER(self.state, history),
+            )


out of curiosity, is this something you've seen happen? how funny if so

Claude says it was just trying to match the CVL logic here. 🤷

ah, yeah, fair enough.

jtoman · 2026-10-30T18:19:03Z

-                ):
-                    lines.append("This run is not accounted for, so the prover stamp is withdrawn.")
-                    validations = {"validations": earned}
+                if stamped:


this whole function is vastly better. I have some idea about what its actually trying to do. 10/10. Thanks

jtoman · 2026-10-30T18:25:36Z

+checked, and this draft cannot be stamped until they are. Run verify_rules again; if they are still missing, the run's
+link is where to look.


the agent has zero way to access the run link tho

Will reword

jtoman · 2026-10-30T18:26:02Z

+Not accounted for: {{ property_failures | join(", ") }}. Fix the rule, or mark it with expect_rule_failure and say why
+the failure is real.


I wouldn't call these "unaccounted for"; they're very much accounted for, just failing when they shouldn't be.

Will reword

The alert report was fetched with its own aiohttp GET against the job link, a second way of reading a job's output beside the results client. It goes back to the results client's fetch_output_file on a worker thread, so one place decides how output files are fetched. The body is still parsed in memory rather than written into the results directory and read back. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…d failure A rule with no verdict sent the agent to the run's link, which it cannot open. If a retry does not bring the verdict back, it now stops resubmitting and says which rules were never checked. A rule that failed without a marking was "not accounted for". It is named as what it is: a failed property not marked as an expected failure. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Brings #280 (P3b2b) back from its squash commit. Its design replaces this branch's version of the slice, and the later work built on it is ported: - A marking now invalidates the prover stamp, and verify_rules re-judges the last run of an unchanged draft under the current markings. The branch's _remarked / stamp_under re-stamping in the marking tools, and tests/test_cvlr_restamp.py, are gone. - LastVerdicts is #280's (status codes, the draft digest) plus this branch's `rules`, which the publish gate and GeneratedHarness read. - The stamp covers the markings (make_verdict_stamper). PROVER_STAMPER and FEEDBACK_STAMPER live in cvlr/state.py, as foundry's do, and check_cvlr_completion passes both. VerifyDeps loses `stamper`. - Violations are classified by assertOrigin. _CaptureCallbacks skips a rule with no counterexample rather than classifying None. - The run's notes render from verdicts.j2; the five per-note templates are deleted. Its Cannot overflow advice keeps this branch's "bound once, then restate below the handler or skip" (0accd84). - External functions come from ProverReport.alerts. The judge's HarnessAssumptions carries ExternalWarnings | UnreadableAlertReport, and says when the report could not be read. external_functions.j2 keeps this branch's extraction / mock_fn advice. tests/test_prover_external_functions.py is replaced by #280's tests. Kept from this branch: - results_api (P3b3's rename); the alert report is fetched through it. A FAILED/HALTED job's ERROR alerts (_failure_alerts) and a succeeded job's report (_fetch_alert_report) share one fetch. - CloudResultsUnavailable, the static-verdict tree-view fix, the rustc 1.89 allocator shim, and the optional CexHandler. The author prompt no longer says a marking stamps without another run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Marks P3b2b merged as b45e74b with its measured size, says what review changed (assertOrigin classification, markings in the verdict stamps, verify_rules judging the last run again, the generic alert report, one notes template), and records how the merge into eric/solana-staging (42f0507) ported the branch's later work onto it. P1b is next. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil mentioned this pull request Oct 23, 2026

CVLR: stage summaries, edits, and settings, and account for each rule #268

Merged

Base automatically changed from eric/cvlr-harness-gate to master October 27, 2026 22:54

ericeil added a commit that referenced this pull request Oct 27, 2026

docs: split P3b2 into P3b2a (#268) and P3b2b (#280)

9303d0e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil added a commit that referenced this pull request Oct 27, 2026

docs: P3b2a merged as #268; P3b2b (#280) is next

bfc5cd1

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil force-pushed the eric/cvlr-verdict-meaning branch from 9c9fe2d to ae8bcee Compare October 28, 2026 16:42

ericeil changed the title ~~CVLR: say what a verdict means, and stamp when every rule is accounted for~~ CVLR: classify rule verdicts and allow expected failures Oct 28, 2026

ericeil and others added 6 commits October 28, 2026 10:48

prover: say what violated_assertions omits, without implying a Prover…

5bb21a8

… constraint Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

cvlr: say why unaccounted sorts its rule names

d16fb03

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

cvlr: describe Cannot overflow without naming the sound-math pass

e75c762

The agent has no idea what the "sound-math pass" is; say instead that the Prover adds this check on its own, rather than the rule asserting it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil marked this pull request as ready for review October 28, 2026 18:44

ericeil requested a review from jtoman October 28, 2026 18:44

jtoman requested changes Oct 28, 2026

View reviewed changes

ericeil and others added 9 commits October 28, 2026 14:52

prover: say plainly which mistake an untagged assertion can cause

e90f4e8

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

cvlr: an incomplete check says nothing about the property, not nothin…

26827fd

…g about the program A loop-unwinding stop does say the loop can iterate past the bound. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil requested a review from jtoman October 30, 2026 00:03

jtoman approved these changes Oct 30, 2026

View reviewed changes

ericeil and others added 2 commits October 30, 2026 11:44

Merge branch 'master' into eric/cvlr-verdict-meaning

6804ee3

ericeil merged commit b45e74b into master Oct 30, 2026
2 checks passed

ericeil deleted the eric/cvlr-verdict-meaning branch October 30, 2026 18:57

		@@ -0,0 +1,3 @@
		These rules are marked as expected failures but VERIFIED: {{ names }}. Either the defect is not there, or the rule does

		checked, and this draft cannot be stamped until they are. Run verify_rules again; if they are still missing, the run's
		link is where to look.

		Not accounted for: {{ property_failures \| join(", ") }}. Fix the rule, or mark it with expect_rule_failure and say why
		the failure is real.

Conversation

ericeil commented Oct 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why is this needed?

Where to start

How the pieces fit

Testing

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!

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

ericeil commented Oct 23, 2026 •

edited

Loading