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

SpecCheck: When LLMs Formalize, Who Checks the Spec?

Bhagyesh Kumar · Team invi

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

Read the report

Report: SpecCheck: When LLMs Formalize, Who Checks the Spec?

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

Proof checkers guarantee that code satisfies a specification, but not that the specification captures what the user intended. When large language models formalize natural language requirements, they can silently weaken postconditions, drop edge cases, or resolve ambiguous terms in ways the user did not expect: a failure mode we call intent drift. We present SpecCheck, a pipeline that detects intent drift through two complementary techniques: ambiguity elicitation, which surfaces implicit assumptions before formalization, and round-robin cross-validation, where two independent models each formalize the same requirement and informalize the other's output. Across Lean~4 theorems (VERINA) and Python Hypothesis property suites, we find that the value of cross-model validation is formalism-dependent: on Lean~4, it exposes under-formalization that single-model assessment systematically misses (20-percentage-point gap), while on property-based tests, single-model assessment is already well-calibrated. The full pipeline achieves a 97% confirmation rate on correct specifications and 100% detection on deliberately weakened ones. Ambiguity count at elicitation time predicts which requirements will cause trouble downstream, flagging difficult requirements before formalization.

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. Thank you for submitting this – this is a strong contribution! It addresses an important problem, and presents a thorough methodology and intriguing results! Great presentation, too!

  2. The contribution is the formalism-dependent finding, and it is a good one: cross-model validation buys a clean 20-point gap on Lean 4 yet next to nothing on Python property tests. The ablation, the three runs per condition, and the GPT-4o cross-provider replication are all real methodological strengths. The main hesitation is that the central VERINA story turns on whether B2 is genuinely higher-recall or merely noisier, and the paper cannot yet tell those apart: the only recall evidence is ten specifications the authors weakened themselves. Until LLM-generated specs are sampled and human-labeled for drift, "essential signal for Lean 4" reads as a well-supported hypothesis rather than an established result. Variance should also be reported rather than three-run means: one run produced seven tautology disputes against a baseline near zero, a swing larger than several of the cross-condition effects being interpreted.

    Read full reviewShow less

Cite this project

@misc{kumar2026speccheck,
  title = {{SpecCheck: When LLMs Formalize, Who Checks the Spec?}},
  author = {Bhagyesh Kumar},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/speccheck-when-llms-formalize-who-checks-the-spec-iyuz}},
  url = {https://apartresearch.com/sprints/projects/speccheck-when-llms-formalize-who-checks-the-spec-iyuz}
}

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