Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 24, 2026Tel Aviv

Where to Look: Energy-Based Fault Localization for Verus Vericoding

Guy Nachshon · Team Oz Labs

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

Read the report

Report: Where to Look: Energy-Based Fault Localization for Verus Vericoding

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

A 1.5B-parameter discriminative energy-based model that scores each line of a Verus implementation with an energy proxy for "this line is the bug." Qwen2.5-Coder-1.5B + LoRA + sentinel-token per-line head, trained on 39k Microsoft Verus pairs with InfoNCE + pairwise hinge + ListNet. One adapter, runs on a single H100, demo runs in the browser.

The finding is split. The 1.5B specialist beats every frontier LLM on per-line fault localization (top-3 0.84 vs 0.74). Frontier LLMs win whole-impl ranking (AUROC 0.91 vs 0.78) and CEGIS repair (30% vs 25%). Different tools for different layers of the verification loop — and we're explicit about which.

The audit is the other contribution. Every FAIL impl in the dev-test corpus carries a // FAILS debug marker that Qwen's pretraining prior couples to failure. Strip the marker, watch the signal collapse for some checkpoints, hold for frontier LLMs, over-correct for ours. We document the leak, release the strip-FAILS audit pipeline, and ship Counterfactual Marker Augmentation as the fix.

Released: model, dataset, audit pipeline, CEGIS harness, every LLM-baseline record, browser-side demo. All under: https://ozlabsai.github.io/VericodingEBM/

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. This is a careful and technically honest project on fault localization for Verus verified code. The problem is relevant to secure program synthesis: when AI-generated verified code fails, developers and repair agents need help identifying where the proof or implementation likely went wrong. A line-level localizer could make verifier-in-the-loop repair more inspectable and efficient.

    The strongest part of the project is the evaluation discipline. The submission compares against static baselines, frontier LLMs, and a closed-loop CEGIS-style repair setup. It also includes a useful marker-leak audit showing that an earlier checkpoint benefited from // FAILS / FIXME leakage. That kind of careful negative-result reporting is valuable in this area because misleading localization performance could create false confidence in secure-code workflows.

    The main limitation is that the specialist model does not yet outperform frontier LLMs, and the CEGIS repair experiment does not show a clear repair-rate advantage from specialist-guided localization. To strengthen the work, I would focus the next iteration on demonstrating a concrete repair-loop benefit: better success under limited model budget, faster local inference, improved robustness on unseen Verus patterns, or stronger performance when frontier LLMs are not available. Broader tests on additional verified-programming settings would also help.

    Overall, this is solid hackathon work with good methodology, clear reporting, and a meaningful security-relevant direction. The current results are mixed, but the artifact and evaluation setup are useful foundations for future secure program synthesis research.

    Read full reviewShow less

  2. The authors deserve credit for their transparent analysis, especially the strip-FAILS audit that clearly identified a serious pre-training data leak. However, as a practical system, the proposed EBM does not outperform strong zero-shot LLM baselines on localization or repair tasks. The evaluation appears statistically underpowered, and the model struggles with ensure clauses due to limited global context. Strengthening global reasoning and validating the approach on real production defects would significantly improve the work impact.

Cite this project

@misc{nachshon2026where,
  title = {{Where to Look: Energy-Based Fault Localization for Verus Vericoding}},
  author = {Guy Nachshon},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/where-to-look-energybased-fault-localization-for-verus-vericoding-0cdy}},
  url = {https://apartresearch.com/sprints/projects/where-to-look-energybased-fault-localization-for-verus-vericoding-0cdy}
}

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