Skip to content

Code gen changes, Pt 4#10

Open
jtoman wants to merge 4 commits into
jtoman/audit-db-migrationfrom
jtoman/codegen-multi-spec
Open

Code gen changes, Pt 4#10
jtoman wants to merge 4 commits into
jtoman/audit-db-migrationfrom
jtoman/codegen-multi-spec

Conversation

@jtoman

@jtoman jtoman commented Jun 23, 2026

Copy link
Copy Markdown
Contributor

Multi spec. Allow multiple spec files to gate the generated code. Adjust internal data structures to match; no CLI entry point exists as the only producer (the assistant) no longer exists.

jtoman added 4 commits June 22, 2026 18:50
Four major changes:
1. Resurrect main.py in the form of a proper "console-codegen"
2. Asyncify all of our code
3. New CEX handling API, uses an agentic analyzer for the codegen
4. Adds dedicated CEX remediation agent (codegen agent was *awful* at
   writing CVL fixes)
Untangling some setup code, better store discipline, modern resource
management. Refactoring out common "validation" logic.
* Remove audit db, move it to store
* takes this opportunity to finally centralize around a single
  file/document abstraction
* better recovery of in progress VFS
* removes trace html generation, no longer served by any live DB
Multi spec. Allow multiple spec files to gate the generated code.
Adjust internal data structures to match; no CLI entry point exists as
the only producer (the assistant) no longer exists.
@jtoman jtoman requested a review from shellygr June 23, 2026 22:59

Follow this procedure:

## Step 0 — Orient

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is not a direct copy of the synthesis_prompt is it? the rewrite seems much more significant, is it just to support multiple spec files?

Comment on lines +248 to +249
isolation + summarization.** Write code so the awkward parts have a natural seam where a
summary can attach.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if we have a more thorough explanation of the rely-guarantee concept around in these prompts, as it seems a more likely candidate for the llm to pick up and understand (separation of concerns, modules, trust-but-verify assumptions) rather than adjectives such as "awkward" and "natural seam".

Comment thread composer/tools/prover.py
"until committed, and runs against it never stamp)."
))

use_working_spec : bool = Field(description=(

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

question about the old code - in which case it is allowed to modify the spec?

@jtoman jtoman force-pushed the jtoman/audit-db-migration branch from eb891fe to 2bcb4fc Compare July 2, 2026 20:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants