Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026Bengaluru

Does Oracle Quality Matter? Adversarial Feedback for Formally Verified Code Synthesis

Pranav Kasetty · Team OracleGap

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: Does Oracle Quality Matter? Adversarial Feedback for Formally Verified Code Synthesis

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

Counterexample-Guided Inductive Synthesis (CEGIS) is the standard approach for repairing LLM-generated code that fails formal verification. We investigate whether augmenting the verifier's error feedback with adversarial LLM-generated counterexamples accelerates convergence. Using 50 Dafny tasks from the Vericoding benchmark, we find that adding a same-capability oracle (Sonnet) does not change pass rates but improves early convergence: pass@2 increases from 66% to 72%, with 9 tasks converging faster vs 6 slower among 42 jointly-solved tasks. The more surprising finding emerges when we upgrade to a stronger oracle (Opus): it unlocks a task that failed under all prior conditions by providing specific proof-repair guidance — identifying a missing lemma call — where the weaker oracle could only report "it times out." This suggests that for secure program synthesis pipelines, oracle quality — the ability to provide actionable proof-engineering feedback — matters more than oracle presence.

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. The project does a clean CEGIS ablation with a Dafny verifier.

    Good next steps are to try for multiple seeds, extend to Lean, explore the Opus effect over more tasks and compare to a non-LLM-counterexample baseline to isolate adversarial counterexample mechanisms from second model feedback.

  2. This project asks a good, focused question for secure program synthesis: when LLM-generated verified code fails, does adding an adversarial LLM oracle improve the CEGIS repair loop, and does the strength of that oracle matter? The framing is useful because verifier feedback in Dafny can be cryptic, and a practical repair system needs feedback that is not only correct but actionable.

    The strongest part of the project is the clear experimental setup. The author compares verifier-only repair against verifier-plus-oracle repair on 50 Dafny tasks from Vericoding, then separately studies a harder subset with a stronger Opus oracle. The result is nuanced rather than overclaimed: same-tier oracle feedback does not meaningfully improve final pass rate, but it seems to improve early convergence; a stronger oracle unlocks at least one task by identifying a concrete missing lemma call. That case study is compelling because it shows the difference between vague feedback and proof-engineering guidance.

    I also liked the failure taxonomy. Breaking failures into timeout, nonlinear arithmetic, quantifier reasoning, specification complexity, and syntax repair oscillation is useful for future work. It makes the project more than just a pass-rate comparison; it points toward which kinds of proof failures need specialized mitigation.

    The main limitation is statistical strength. The experiment uses 50 tasks with one trial per condition, and the paired convergence improvement is not statistically significant. The Opus result is also based on one especially interesting success case, so it should be treated as a strong qualitative signal, not yet as a general conclusion. For a hackathon project that is fine, but a research version would need multiple trials, a larger benchmark slice, and clearer separation between oracle benefit and sampling variance.

    Another limitation is that the “adversarial counterexample” framing is not always fully matched to formal verification repair. In some cases the oracle seems less like a counterexample generator and more like a proof-debugging assistant. That may actually be the better framing: the most useful oracle is not necessarily one that finds bad inputs, but one that gives targeted proof repair advice.

    Overall, this is a thoughtful and useful project. It has a clear research question, a real experimental loop, honest limitations, and a practical implication: use a cheaper generator most of the time, but call a stronger proof-oriented oracle when the repair loop gets stuck. The result is not yet definitive, but it is a good direction and a strong hackathon contribution.

    Read full reviewShow less

Cite this project

@misc{kasetty2026oracle,
  title = {{Does Oracle Quality Matter? Adversarial Feedback for Formally Verified Code Synthesis}},
  author = {Pranav Kasetty},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/does-oracle-quality-matter-adversarial-feedback-for-formally-verified-code-synthesis-ur3c}},
  url = {https://apartresearch.com/sprints/projects/does-oracle-quality-matter-adversarial-feedback-for-formally-verified-code-synthesis-ur3c}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026