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

The Iron Rule Checklist: Structured Specification Elicitation Reduces False-Pass Rates from 82% to 3.5% in LLM-Generated Lean 4 Specifications

Tang Meng

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

Read the report

Report: The Iron Rule Checklist: Structured Specification Elicitation Reduces False-Pass Rates from 82% to 3.5% in LLM-Generated Lean 4 Specifications

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

We measure the false-pass rate in NL-to-Lean 4 specification pipelines: how often objectively insufficient natural language descriptions produce specs that pass all decide-based verification tests. Across 243 descriptions (81 VERINA problems × 3 personas), the baseline false-pass rate is 82.4%. Free-form LLM questioning reduces it to 16.4%. The Iron Rule Checklist, a structured 7-category elicitation protocol, reduces it to 3.5% with zero regressions and 4 of 8 issue types reaching 100% detection. The 6 remaining misses decompose into three structural categories defining the method's theoretical ceiling.

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 paper presents a small empirical study into a prompt-engineering effort in improving the specification writing capabilities of LLMs. The authors propose a 7 step checklist, which when presented to an LLM, was found by the authors in their test set to reduce the rate of generation of faulty specifications. Overall, I think this work is interesting, and provides a useful signal to people looking into this problem. I appreciated the quantitative evaluation of the natural language prompt and the analysis of the results. That being said, ultimately the experimental results boil down to providing an additional natural language prompt to an existing agent, which feels rather incremental. I would be curious to see if through the methodology used to derive the prompt the authors are able to extend this to additional tools and interfaces that could be exposed to an LLM to improve its ability to write specifications. Are there specific tools (such as model checkers, symbolic execution) that an LLM could use to sidestep some of the failure modes identified in this paper?

    Read full reviewShow less

  2. Finding ambiguities in specifications is incredibly important. This sprint produced (a) 7 key questions to probe, and (b) a test set of 243 specs with known gaps. The test set, which was built manually by varying VERINA, may be useful in future as a basis of benchmarks and experiments. The one qualm I have is that as far as I understand, the ambiguous specs were written by the same person who designed the 7 key questions; if so, there's a confounding factor, which is understandable for a hackathon, but going forward it would be interesting to find methodologies that reduce the concern about this.

Cite this project

@misc{meng2026iron,
  title = {{The Iron Rule Checklist: Structured Specification Elicitation Reduces False-Pass Rates from 82\% to 3.5\% in LLM-Generated Lean 4 Specifications}},
  author = {Tang Meng},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/the-iron-rule-checklist-structured-specification-elicitation-reduces-falsepass-rates-from-82-to-35-in-llmgenerated-lean-4-specifications-zy8x}},
  url = {https://apartresearch.com/sprints/projects/the-iron-rule-checklist-structured-specification-elicitation-reduces-falsepass-rates-from-82-to-35-in-llmgenerated-lean-4-specifications-zy8x}
}

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