Extended RAG, CVL context - #115
Open
jtoman wants to merge 11 commits into
Open
Conversation
shellygr
reviewed
Aug 1, 2026
| catch-all entry whose receiver the Prover could not pin to the named contract; | ||
| entry pattern mismatch (locations on reference-type parameters, exact | ||
| signature); an entry naming the inheriting contract instead of the defining | ||
| contract for an inherited method (A2.1); the call originating from CVL (A2.5). |
Contributor
There was a problem hiding this comment.
I think we cannot just assume sighash is conveniently always resolved and not to put specific instructions in such cases
Contributor
Author
There was a problem hiding this comment.
? I'm not sure what in the text you're referring to here.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Our attempts to make all CVL knowledge RAG driven has been yielding mixed results. This attempts to condense some of the most common and important information about CVL into "context documents" which are inlined into every CVL agent's task. Explicit cache markers are added to make this avoid prompt blow ups.
The context documents incorporate (and moot) several existing artifacts:
recipesindex (with some extra information as well beyond what was in kb_populate)cvl_guidance.j2has been expanded and updated and converted tocvl_baseline.md.In addition, we've tried our hand at CoNsTiTuTiOnAl Ai: we have pretty consistently viewed agents treating "get the spec all verified" as the end goal. The "verification_charter.j2" is our first attempt at making the goal of the agent explicit: verified software is the goal, not a verified spec. The feedback judge's criteria are now AlIgNeD with this constitutional principle; most of the evaluations we ask of it are grounded in this principle.
The feedback prompt has also been expanded to close one common failure mode; a property which ends up passing but skips all of the actually important methods.