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

Counterexample-Guided Validation & Repair of LLM-Generated Safety Specifications

Yifei Lu · Team 9999

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

Read the report

Report: Counterexample-Guided Validation & Repair of LLM-Generated Safety Specifications

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

LLMs can turn natural-language safety requirements into formal specifications, but a fluent specification can still be the wrong one. It might quietly drop a guard, block access the policy should allow, or respond inconsistently when a safety-relevant input changes. We built a pipeline that checks whether an LLM-generated specification matches the intended policy, using biosecurity access control as a testbed. Each requirement is broken into traceable safety obligations such as clearance, training, approval validity, expiration, external anonymization, and emergency logging. Candidate specifications are written in a restricted DSL, and four oracles judge each one together: obligation coverage, sampled behavioral agreement, metamorphic relations, and SMT-guided counterexample search over Z3. Every candidate ends up with a risk-weighted review card. Across 30 simulated LLM candidates and 60 controlled mutants, small manual test suites caught only 63.3% of injected faults and 55.3% of the high-severity ones, while systematic validation reached 98.9% overall and 100% on high-severity faults. Feeding counterexamples back as repair signals fixed 29 of 30 candidates, raising the mean score from 70.1 to 95.4 and clearing every high-severity under-constraint, with one regression. In a live run, specifications from Gemini 3.5 Flash were parsed and validated end-to-end, and obligation-guided prompting reached full obligation coverage. Together, these results show that LLM-generated safety specifications can be validated systematically, with each failure traced back to a specific missing guard.

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 project attacks an core part of the deployment of AI to SPS. The particular idea here is not especially new, and the active focus of ongoing research, but the execution is excellent.

    The use of large amounts of external ground truth make it a compelling contribution to the field. The experimental design is well-considered and the authors displayed considerable honesty and epistemic hygiene in their analysis and discussion. The write-up is convincing in its gathering of relevant evidence and discussion of what the work does and does not show.

    It suffers, slightly, from relying on a non-adversarial threat model. I expect that high-value deployment of this and similar techniques will be in a situation where that assumption does not hold (e.g. with concerns of secret loyalties or misalignment). The arguments for applicability are also a little too dependent on confidence in gold validity.

    Read full reviewShow less

  2. The author has good instincts for this problem. The observation that all three systematic strategies converge on the same detection rate and that the formal oracles add zero raw detection over sampling, thus their value is diagnostic, not detective is sharp.

    The execution is sparse relative to those instincts, and the useful future work is to build the harder experiments the author's own thinking is pointing at.

Cite this project

@misc{lu2026counterexampleguided,
  title = {{Counterexample-Guided Validation \& Repair of LLM-Generated Safety Specifications}},
  author = {Yifei Lu},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/counterexampleguided-validation-repair-of-llmgenerated-safety-specifications-0s4g}},
  url = {https://apartresearch.com/sprints/projects/counterexampleguided-validation-repair-of-llmgenerated-safety-specifications-0s4g}
}

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