Phase 3: LLM Seed Generation + Repair

[quinn-dougherty]

Phase 3: LLM Seed Generation + Repair

Use Claude to generate poisoned prefixes targeting specific attack categories, and iteratively repair prefixes that have syntax/type errors.

Status: NOT STARTED

Ref: docs/design-plan.md Phase 3

---

Files to create

• scaffold/src/scaffold/synthesizer.py — LLM prefix generation
• scaffold/src/scaffold/repair.py — Iterative prefix repair
• BAML definitions for structured LLM calls (baml-py dependency installed but unused)

Prefix Synthesizer

• Implement LLM call with attack category parameterization
• Structured output parsing (BAML)
• Rate limiting and cost tracking

Repair Engine (prefix-focused)

When a prefix has syntax/type errors, repair it iteratively (up to 5 attempts). The repair only needs to make the DECLARATIONS valid — much easier than making proofs valid.

• Implement iterative repair loop
• Feed diagnostic categorization from diagnostics.py into repair prompts
• Track repair success rates per error category

Sorry-seeding strategy

• Generate prefixes where some helper theorems use sorry
• Verify golden suffix doesn't transitively depend on sorry'd helpers via #print axioms