Drop the eager structural-invariant phase by shellygr · Pull Request #214 · Certora/AutoProver

shellygr · 2026-09-05T11:33:10Z

What was blocking

The structural-invariant phase sat inside prepare_formalization, and the driver joins that
before any component is formalized. Its formulation half already ran alongside AutoSetup, so
that was never the cost. The cost was the invariant CVL generation: a full
batch_cvl_generation with real prover jobs, serial after the gather because it needs
AutoSetup's prover_config. #200's own commit message measured it at two of four hours on one
run, and it was paid whether or not any property turned out to need an invariant.

It was also the run's only fatal path, since a give-up there raised and killed everything, and
it was all-or-nothing: a budget curtailment quarantined the spec and no component imported it.

What replaces it

The component author writes the invariant it needs, in its own spec, and the prover checks it in
the same run as the rule that cites it. The author prompt already said to do this on an
impossible starting state. What it lacked was any reason to prefer that over a bare require,
which was cheap and always available. The ladder now makes the invariant the default rung and
spells out what the last rung costs. A structural_invariant_guidance tool carries the
selection knowledge the deleted judge held, pulled only when the author hits an unreachable
prestate rather than sitting in every prompt.

Two ways this could have gone green while proving nothing, both closed:

An invariant that no property names is dropped from the report as an orphan
(collect.py). PublishResultTool now reads the declared rule set off the last prover run
and passes it to validate_property_rules, which already had the both-directions branch
behind that argument and no caller on this path. An unmapped invariant blocks publication.
expect_rule_failure on an invariant that a requireInvariant cites turns every citing rule
into an unproven assumption while the run reports green. Refused in the author prompt, on the
tool's own description, and in the judge's laundering practice.

The judge's overconstrained-inputs criterion was scoped to preserved blocks, which is where a
bare require used to land. Without a pre-proven invariants.spec it will land in rule bodies
too, so that criterion widens to any require that fixes the shape of the prestate.

Notes for review

prepare_formalization is AutoSetup plus the summaries built on its config. No await
moved. The overlap with property inference and Add a prioritized run mode #200's prioritization already existed; this
makes the thing being overlapped cheap. tests/test_pipeline_staged_formalizer.py still pins
the ranking ahead of the join, unchanged.
tests/test_prover_prepare_formalization.py is the new load-bearing test. It asserts no
CVL_GEN-phase task is launched before the barrier, which is the precise statement of the
change.
The deleted tape lane was the Counter harness's designated tool-coverage lane. Its turns
(manual and recipe search, the research sub-agent, the typechecker rejection path,
skip/unskip, expect-fail/passage) move into the component lane rather than being lost.
A warm local cache from before this commit will mis-hit. FORMALIZATION_KEY is keyed on
the property batch and plugin ids only, so a replayed GeneratedCVL still imports
invariants.spec, which nothing writes now. Use a fresh --cache-ns. Cloud is unaffected: a
git+ install puts the commit in the root key.
Old cache namespaces keep structural-inv and invariant-cvl subtrees that the walkers
no longer render, and a project re-run in place keeps a stale certora/specs/invariants.spec
and its conf and properties files. Both are expected, not data loss.
formalization_preparation keeps its budget key because BUDGET_PHASES is derived from
it and dropping it would reject existing budget files. Nothing left under that phase installs
a monitor, so it is attribution-only now, and the budget matrix's T3 scenario is deleted
rather than reworded.
No frontend change needed. The webapp's invariants.spec handling is a display allowlist
that .spec already covers, so historical reports keep rendering.
scripts/autoprove_cache_explorer.py still imports the deleted module. It has been
unimportable for unrelated reasons for a while and is outside both pyright and pytest. Left
alone deliberately; say the word and I will delete it.

Verification

COMPOSER_STRICT_TEMPLATES=1 uv run pytest -m 'not expensive' tests/ passes 1163, and pyright
reports 0 errors, against current master with the updated graphcore pin. The expensive
integration lane still needs a run, and so does one real end-to-end run on a project with a
pre-change baseline.

The acceptance criterion for that run is not in report.json: a rule that requires its way past
a counterexample reports VERIFIED and GOOD. Compare the generated autospec_*.spec files
against the baseline for invariants authored, requireInvariant citations, and bare requires
in rule bodies, parsed with the real CVL parser rather than grep.

🤖 Generated with Claude Code

Every run proved a set of structural invariants before writing a single component's CVL. The formulation half already ran alongside AutoSetup. The half that cost was the invariant CVL generation, serial after that gather because it needs AutoSetup's prover_config, and joined by the driver before any component is formalized, so one invariant prover job held up the whole run whether or not any property needed an invariant. It was also the run's one fatal path (a give-up there raised and killed everything) and all-or-nothing: a budget curtailment quarantined the spec and nobody imported it. Invariants are now written by the component author that needs one, in that component's own spec, and proven in the same verify_spec run as the rule citing them. The prompt already pointed at this on an impossible starting state; what it lacked was a reason to prefer it over a bare require. The ladder now makes the invariant the default rung and says what the last rung costs. A structural_invariant_guidance tool carries the selection knowledge the judge used to hold: what makes a state relationship worth stating, and the four ways a candidate goes wrong. Two ways this could have gone green while proving nothing, both closed: - An invariant no property names is dropped from the report as an orphan. PublishResultTool now reads the declared rule set off the last prover run and passes it to validate_property_rules, so the mapping is checked in both directions and an unnamed invariant blocks publication. - expect_rule_failure on an invariant that a requireInvariant cites turns every citing rule into an unproven assumption while the run stays green. Refused in the author prompt, on the tool's own description, and in the judge's laundering practice. The judge's overconstrained-inputs criterion was scoped to preserved blocks. That is where a bare require used to land. With no pre-proven invariants.spec it will land in rule bodies too, so the criterion widens to any require that fixes the shape of the prestate, wherever it appears. prepare_formalization is now AutoSetup and then the summaries built on its config, so what the driver overlaps with property inference and prioritization is finally cheap. No await moves; that overlap already existed. This also drops what the phase was the last user of: the invariants.spec artifact identity, two cache families, the synthetic report component and its Formalizer hook (the prover was its only implementer), the AutoProvePhase member, and batch_cvl_generation's component=None and editing_tools=None branches. The deleted tape lane was the Counter harness's designated tool-coverage lane, so its turns move into the component lane rather than being lost. formalization_preparation keeps its budget key, because BUDGET_PHASES is derived from it and removing it would reject existing budget files. But nothing left under that phase installs a monitor, so it is attribution-only now. The budget matrix's T3 scenario is deleted rather than reworded: every observable it named is unreachable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

An empty declaration set read as unknown. validate_property_rules turned set() into None through a falsy check, so a spec the prover typechecked as declaring nothing accepted a mapping naming rules that do not exist. None now means the caller has no ground truth, and an empty set means the prover looked and found nothing declared. tests/test_publish_mapping_gate.py drives PublishResultTool itself, which no test did before; both new cases fail against the old check. Restore the judge rejection round in the component tape. Porting the deleted invariant lane carried its tool coverage but not its good=False, revise, good=True sequence, which left an approval as the only judge verdict in the file. The author now puts a first draft that typechecks but leaves one property unformalized, the judge rejects it on coverage, and the revision is approved. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

shellygr · 2026-09-05T12:07:35Z

@@ -0,0 +1,61 @@
+A counterexample that starts from a state the contract could never actually reach is telling you that the


probably needs the standard headers for prompts as it had before

Claude answers: done, split into and and gave the four failure modes Good/Bad pairs. No role preamble though: cvl_system_prompt.j2 already opens the author's system prompt with the FV-engineer-at-Certora role, so the Web3 framing is in context already.

It was written as bare prose, copying unresolved_call_guidance.j2 and erc20_advice.j2. Those two are the exceptions: cvl_additions.j2 and natspec_stub_tools_guidance.j2 both carry a wrapper tag, and 18 templates open with <background>. Split into <background> for the situation and the candidate indicators, and <guidance> for the failure modes and diagnostics. No role preamble. The author's system prompt already opens with cvl_system_prompt.j2, whose Role block names the formal verification engineer writing CVL for Web3 applications and calls out inductive invariants by name. invariant_explanation.j2 restated that framing because it was the whole prompt for a standalone agent; this document is handed to an author mid-task. The four failure modes were adjectives and a remedy. They now carry Good and Bad example pairs, drawn from the contract shapes already in the document, which is how the rest of the prompts anchor a judgement call. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

jtoman

some nits.

jtoman · 2026-09-08T19:35:13Z

+You may also consider the inverse; over-constraining the input space may cause the prover to miss real bugs. In particular, any constraint that fixes the
+*shape of the prestate* — a relationship among the contract's own state fields that the contract maintains — and is *not* a `requireInvariant` statement
+(i.e., a *proven* assumption) should be subject to intense scrutiny, wherever it appears: in a `preserved` block or in the body of a rule. Such a
+relationship is exactly what an invariant is for, and a bare `require` asserts it where an invariant would prove it.


"asserts": somewhat confusing, as assert roughly means "proven" in cvl.

Claude answers: done, it says "assumes the relationship instead of establishing it" now. Same slip was in two more places you did not see, the author's ladder and the Criteria 8 bullet; both fixed.

jtoman · 2026-09-08T19:35:28Z

+*shape of the prestate* — a relationship among the contract's own state fields that the contract maintains — and is *not* a `requireInvariant` statement
+(i.e., a *proven* assumption) should be subject to intense scrutiny, wherever it appears: in a `preserved` block or in the body of a rule. Such a
+relationship is exactly what an invariant is for, and a bare `require` asserts it where an invariant would prove it.
+A `require` that merely bounds a rule's own free inputs is not this; that is Criteria 3's business.


tighten this

Claude answers: done, four lines instead of five, and dropped the sentence that restated the one before it.

jtoman · 2026-09-08T19:36:49Z

+- A supporting invariant listed alongside a rule is evidence about that rule's proof, not coverage of
+  the property in its own right; judge coverage by the rules that assert the property.


this doesn't really make sense as an item under the "For each property:" directive. I'm also not entirely sure what this trying to say.

Claude answers: done, moved out of the list. It is about property_rules entries that name a supporting invariant the rules cite with requireInvariant, so it now says that below the list instead of pretending to be a fourth branch.

jtoman · 2026-09-08T19:39:22Z

+prover does not know something you do: the contract's fields stand in some relationship that the code
+maintains, and nothing in your spec says so. For example, the prover may hand you a starting state where a
+user's balance of a token is significantly greater than that token's total supply — clearly infeasible for a
+well-behaved token, but perfectly admissible to a tool that was never told otherwise.


this is too "cute"; "perfectly admissible to a tool" is a weird way of talking about the prover. "never told otherwise" is likewise a weird way to talk around "adding a constraint"

Claude answers: done, it now says the spec is missing a constraint and that the prover explores every state the spec admits.

In CVL `assert` is the thing that gets proven, so using it for a claim made without proof reads backwards. The prompts said it in three places: the author's ladder, Criteria 4, and the Criteria 8 bullet. They now use assume for `require` and prove or establish for an invariant, which is the vocabulary the rest of property_judge_prompt.j2 already speaks. Criteria 4 also lost a sentence that restated the one before it, and Criteria 8's note about supporting invariants moves out of the "For each property" list. That list is a set of branches and the note is not one of them, which is why it read as a non-sequitur; it now sits below the list and says what it is actually for, that a supporting invariant named in property_rules is part of the proof rather than a second rule covering the property. The guidance opening described the prover as a tool that was never told otherwise. It now says the spec is missing a constraint and that the prover explores every state the spec admits. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

jtoman

RIP king

shellygr and others added 2 commits September 5, 2026 14:31

shellygr commented Sep 5, 2026

View reviewed changes

Comment thread source_edits_integration.md Outdated

shellygr and others added 2 commits September 5, 2026 15:10

Apply suggestion from @shellygr

69a4efe

shellygr requested a review from jtoman September 5, 2026 14:40

Merge branch 'master' into shelly/drop-structural-invariant-phase

127729e

shellygr mentioned this pull request Sep 8, 2026

Take graphcore 85be3db, which bounds the no-tool-call scolding loop #227

Open

jtoman reviewed Sep 8, 2026

View reviewed changes

jtoman approved these changes Sep 10, 2026

View reviewed changes

shellygr enabled auto-merge (squash) September 11, 2026 10:48

Merge branch 'master' into shelly/drop-structural-invariant-phase

b4181fe

shellygr merged commit ee3ee7a into master Sep 11, 2026
2 checks passed

Navigation Menu

Uh oh!

Drop the eager structural-invariant phase - #214

Drop the eager structural-invariant phase#214
shellygr merged 7 commits into
masterfrom
shelly/drop-structural-invariant-phase

shellygr commented Sep 5, 2026 •

edited

Loading

Uh oh!

shellygr Sep 5, 2026 •

edited

Loading

Uh oh!

shellygr Sep 5, 2026

Uh oh!

Uh oh!

jtoman left a comment

Uh oh!

jtoman Sep 8, 2026

Uh oh!

shellygr Sep 10, 2026

Uh oh!

jtoman Sep 8, 2026

Uh oh!

shellygr Sep 10, 2026

Uh oh!

jtoman Sep 8, 2026

Uh oh!

shellygr Sep 10, 2026

Uh oh!

jtoman Sep 8, 2026

Uh oh!

shellygr Sep 10, 2026

Uh oh!

jtoman left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		@@ -0,0 +1,61 @@
		A counterexample that starts from a state the contract could never actually reach is telling you that the

		- A supporting invariant listed alongside a rule is evidence about that rule's proof, not coverage of
		the property in its own right; judge coverage by the rules that assert the property.

Uh oh!

Conversation

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

Uh oh!

What was blocking

What replaces it

Notes for review

Verification

Uh oh!

shellygr Sep 5, 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!

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!

jtoman left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

shellygr commented Sep 5, 2026 •

edited

Loading

shellygr Sep 5, 2026 •

edited

Loading