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

Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents

Linh Le, David Williams-King · Team Lida Safety

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

Read the report

Report: Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents

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

Specifications for real systems do not exist as one-shot artifacts: the user's intent emerges as they discover edge cases, rewrite drafts, and react to failing tests. We present an iterative pipeline that takes this seriously --- every spec artifact (the Lean predicate, the Python reference oracle, the generated code, the LLM-emitted concrete test cases) is independently editable and individually re-verifiable. Each round of the brief regenerates only the artifacts the reviewer asks for; the rest are preserved. This operationalises Dodds' position that "specifications don't exist" in the complete-and-coherent form formal-verification tools expect --- the right tooling shape is iterate-and-export, not generate-and-ship. Concrete contributions: (i) the iterative pipeline itself --- editable Lean, code, oracle, and test cases; (ii) LLM-emitted concrete test cases derived from the spec, run row-by-row against the agent's implementation; (iii) a behavioral + structural invariant DSL; (iv) mutation testing for specifications; (v) Lean 4 generation of a structural Diff->Prop block and an algorithmic predicate over the function's arguments, both type-checked by lake build; (vi) Hypothesis property-based testing of the agent's code against the (editable) reference oracle. On the 60-pair evaluation derived from prior work, our structured validator reaches 98.3% accuracy, 2.2% false-accept rate, and Cohen's K = 0.957 while matching the strongest LLM judge at ~300x lower wall-clock cost. The mutation harness finds 39.7% of perturbations load-bearing with zero brittle mutations. Cross-dataset experiments on five Python benchmarks spanning 2021-2025 (MBPP, HumanEval, BigCodeBench, HumanEval Pro, LiveCodeBench) show 100% Lean type-check across 25 problems, and a codegen-validation rate that improves from 40% to 92% after three targeted fixes. We trace the iterative pipeline end-to-end on a deliberately under-specified word-wrap brief whose intent stabilised only after four rounds of refinement, and use the simpler is_not_prime task to show the same pipeline handling a clean one-shot intent. All code, the Lean prelude, the evaluation harness, and a browser demo are released.

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. A notably complete submission: a working NL→Lean→code→validate loop with real Lean that type-checks under lake build, released code, and a genuine ablation; the execution and presentation are thorough and well-polished. Two reservations weigh on the impact score. The headline numbers, 98.3% accuracy and κ=0.957, are measured against labels the authors assigned on a corpus they built, which is agreement with their own intent rather than validator correctness; a handful of third-party-labeled pairs would settle it. And the 40→92% codegen jump is harness and parsing work, not evidence the spec layer improved, so the paper would read more honestly leading with that distinction. The structural invariants are also behavior-agnostic by design: scope-clean but semantically-wrong candidates would be needed before the validator can be trusted against an LLM judge.

  2. The authors were transparently honest about the circularity problem and a good next set of steps could be to try to measure it and define its boundary. Future work could also be on semantic adequacy, where one proves equivalence of the emitted predicate to the oracle on a bounded domain. Good work overall; keep this going!

Cite this project

@misc{le2026vibecoding,
  title = {{Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents}},
  author = {Linh Le and David Williams-King},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/vibecoding-specs-eliciting-editing-and-verifying-specifications-for-ai-coding-agents-re3p}},
  url = {https://apartresearch.com/sprints/projects/vibecoding-specs-eliciting-editing-and-verifying-specifications-for-ai-coding-agents-re3p}
}

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