SpecCheck: When LLMs Formalize, Who Checks the Spec?

SpecCheck detects intent drift in LLM-formalized requirements using ambiguity elicitation and cross-model validation, evaluated on Lean 4 theorems and Python property-based tests.

Project Details

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.

Hackathon paper: SpecCheck: When LLMs Formalize, Who Checks the Spec?
Code: github.com/invi-bhagyesh/SpecCheck

Theory of Impact

Formal verification can prove that code follows a specification, but it cannot tell us whether the specification says what the user actually wanted. SpecCheck aims to add a check at this missing step. We want to find out whether independent model disagreement is a useful way to catch mistakes such as missing cases or weakened requirements. If it works, this could give LLM-based formal verification a simple extra layer of checking before we trust the final specification.

People

Bhagyesh Kumar

Team Member

Track Record

Secure Program Synthesis Hackathon (Apart Research), 2026

Grants Received– no grants recorded

Add grant

Funding Asks

Funding ask

Open

Minimum

$5,000

Ideal

$10,500

What this ask is

SpecCheck looks at a simple problem: when an LLM turns a natural-language requirement into a formal specification, how do we know it kept the original intent? We use two ideas: asking the model to flag ambiguities first, and having independent models check each other's formalizations. Our first experiments found that this catches issues that single-model checking misses, especially for Lean 4. The next step is to test how well this really works. We will create more LLM-generated specifications, have people label whether they match the original requirement, test different models and formalisms, and add stronger checks such as formal equivalence and counterexamples.

How the money will be spent

$3,500: LLM API costs
$3,000: RunPod GPU compute
$4,000: Human annotation

Discussion

Private comments in this thread are only shown to approved funders and grant reviewers. Email hi@grantmaking.ai or to request access.

Private UserPrivate15d?