Code editor by jtoman · Pull Request #72 · Certora/AutoProver

jtoman · 2026-07-14T19:13:30Z

Prototype for editor agent to allow the cvl author to request (limited) changes to the source code to work around prover limitations (unstructured/custom storage, refactoring, etc.)

Gated with a judge agent as usual.

…de-munger

shellygr

do we include edits in the final report? I missed it here

shellygr · 2026-07-25T14:16:35Z

+
+        result, stdout = await run_prover_inner(
+            folder,
+            [_CONF_NAME, "--build_only"],


do you want to go further and use --compilation_steps_only to make sure the changes are compatible with the spec? or is that handled elsewhere?

oh that's a great point, if we change a storage layout that the spec is directly accessing.

But now that I'm thinking it through; the editor can't change the spec. If we gate completion on "the spec still works", the editor can't propose changes that break the spec, even if the author fully intends to fix the spec in response. The agent being able to rollback its edits are the defense against the editor agent completely borking the spec.

fair enough

shellygr · 2026-07-25T14:19:34Z

+
+Decide whether anything in the diff contradicts or outdates the answer. If every claim the answer makes still holds against the changed source, it is still valid. If the diff changes something the answer depends on — a moved or renamed symbol, altered control flow, a removed branch, a changed signature — it is no longer valid, and you say in one sentence what changed.
+
+Edits are usually small and surgical, so most findings are unaffected; mark a finding invalid only when the diff actually touches what the answer relies on."""


is it given the original or current version? some changes could look local but they are not.

it is shown the diff. And you're right, a change in foo() may or may not be relevant to gorp, depending on whether bar() (called by gorp) itself calls foo.

I think I will make this prompt pessimistic to account for this wrinkle. Ugh, of course it wasn't easy.

shellygr · 2026-07-25T14:20:38Z

+    edit_store: EditStore,
+    sc: SourceCode,
+) -> MigrationOracle:
+    """Build a :class:`MigrationOracle` that decides, in one LLM call, whether a


as above, point for future review - not sure it's a one-shot call

why wouldn't it be? it's operating on raw BaseChatModel with ainvoke; we aren't calling a graph.

I meant that maybe it's better to allow for calling a graph?

shellygr · 2026-07-25T15:36:35Z

+        # "commit_edit" is the name the editor's result message tells the author
+        # to call (see EditMungeTool.run's result_msg) — keep them in sync.


🤔
isn't there a less fragile way to maintain this?

I'm not sure what I follow; what fragility are you foreseeing here? The alternative is to have the edit agent make direct edits to the author's state (bad) or provide a way for the author agent to say directly what edits to apply, but that's just a backdoor to synthesize edits without the edit author. Having agents communicate results between each other with keyed ids is pretty effectively used elsewhere, and is both economical token wise and the only way to make sure an agent doesn't misrepresent or garble results.

I meant the tool names; if those are so stable we can afford keeping them constant strings that's fine

oh oh oh, yes, let's make those constants.

shellygr · 2026-07-27T19:34:44Z

+
+## Do Not Reject For
+
+- Incidental overflow reverts from ordinary checked Solidity math in new code. These are expected


so solidity to solidity new reverts due to math are okay but assembly/unchecked to checked solidity is not

yeah exactly. If somehow one plus turns into two, I don't want a munge getting rejected with "YOU ADDED A REVERT".

jtoman · 2026-07-27T20:01:08Z

+        # "commit_edit" is the name the editor's result message tells the author
+        # to call (see EditMungeTool.run's result_msg) — keep them in sync.


I'm not sure what I follow; what fragility are you foreseeing here? The alternative is to have the edit agent make direct edits to the author's state (bad) or provide a way for the author agent to say directly what edits to apply, but that's just a backdoor to synthesize edits without the edit author. Having agents communicate results between each other with keyed ids is pretty effectively used elsewhere, and is both economical token wise and the only way to make sure an agent doesn't misrepresent or garble results.

jtoman · 2026-07-27T21:01:44Z

+
+        result, stdout = await run_prover_inner(
+            folder,
+            [_CONF_NAME, "--build_only"],


oh that's a great point, if we change a storage layout that the spec is directly accessing.

But now that I'm thinking it through; the editor can't change the spec. If we gate completion on "the spec still works", the editor can't propose changes that break the spec, even if the author fully intends to fix the spec in response. The agent being able to rollback its edits are the defense against the editor agent completely borking the spec.

jtoman · 2026-07-27T21:03:02Z

+
+Decide whether anything in the diff contradicts or outdates the answer. If every claim the answer makes still holds against the changed source, it is still valid. If the diff changes something the answer depends on — a moved or renamed symbol, altered control flow, a removed branch, a changed signature — it is no longer valid, and you say in one sentence what changed.
+
+Edits are usually small and surgical, so most findings are unaffected; mark a finding invalid only when the diff actually touches what the answer relies on."""


it is shown the diff. And you're right, a change in foo() may or may not be relevant to gorp, depending on whether bar() (called by gorp) itself calls foo.

I think I will make this prompt pessimistic to account for this wrinkle. Ugh, of course it wasn't easy.

jtoman · 2026-07-27T21:03:57Z

+    edit_store: EditStore,
+    sc: SourceCode,
+) -> MigrationOracle:
+    """Build a :class:`MigrationOracle` that decides, in one LLM call, whether a


why wouldn't it be? it's operating on raw BaseChatModel with ainvoke; we aren't calling a graph.

jtoman · 2026-07-27T21:10:51Z

+
+## Do Not Reject For
+
+- Incidental overflow reverts from ordinary checked Solidity math in new code. These are expected


yeah exactly. If somehow one plus turns into two, I don't want a munge getting rejected with "YOU ADDED A REVERT".

jtoman · 2026-07-27T21:12:27Z

                        tool_call_id=tool_call_id, content=result.result_str,
-                        prover_link=result.link, validations=stamper(state),
+                        prover_link=result.link,
+                        validations=stamper(state, state["version_history"]),


this is where we include the version history (which implicitly includes the vfs).

jtoman added 14 commits July 8, 2026 16:28

New data model for "source can be edited" model

f7d8dc2

bug fix

369d783

what WAS I thinking

8f73a46

Start of editor

de11d1e

boop

c88d6fa

checkpoint

f5e55cd

almost there maybe

1e96b4b

final cleanups

d51decd

save/restore version history on crashes

0452300

finishing rebase

b0154f2

pruning

c536861

oops

0e68e68

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

e0f330a

…de-munger

Test fixups

20bbd56

jtoman marked this pull request as ready for review July 17, 2026 05:10

jtoman requested a review from shellygr July 17, 2026 05:11

jtoman added the autoprover label Jul 17, 2026

jtoman added 2 commits July 17, 2026 13:25

house keeping

47b372e

prompt updates

2bd70e0

shellygr reviewed Jul 27, 2026

View reviewed changes

jtoman commented Jul 27, 2026

View reviewed changes


		Decide whether anything in the diff contradicts or outdates the answer. If every claim the answer makes still holds against the changed source, it is still valid. If the diff changes something the answer depends on — a moved or renamed symbol, altered control flow, a removed branch, a changed signature — it is no longer valid, and you say in one sentence what changed.

		Edits are usually small and surgical, so most findings are unaffected; mark a finding invalid only when the diff actually touches what the answer relies on."""

		# "commit_edit" is the name the editor's result message tells the author
		# to call (see EditMungeTool.run's result_msg) — keep them in sync.


		## Do Not Reject For

		- Incidental overflow reverts from ordinary checked Solidity math in new code. These are expected

Uh oh!

Conversation

jtoman commented Jul 14, 2026

Uh oh!

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

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!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants