claimcheck: Measuring and Improving Specification Faithfulness

Martin Amster; One An; Holly Baker; Fernanda Graciolli; Simon Henniger; Nada Amin

cs.CLOct 12, 2026

claimcheck: Measuring and Improving Specification Faithfulness

Authors: Martin Amster, One An, Holly Baker, Fernanda Graciolli, Simon Henniger, Nada Amin

Organizations: Universidad de Buenos Aires Buenos Aires, Argentina · University of Pennsylvania Philadelphia, PA 19104, USA · PolicingLab Dublin, Ireland · Midspiral, Inc. Cambridge, MA 02139, USA · Harvard University Cambridge, MA 02138, USA · Harvard University & Midspiral, Inc. Cambridge, MA 02138 & MA 02139, USA

Abstract

Formal verification proves that a program satisfies its specification, but says nothing about whether the specification captures what the author meant. As LLMs increasingly write both code and specifications, a gap between the author's natural-language requirement and the specification becomes a live risk. A machine-checked proof of a property narrower than the one requested is worthless but passes every check. Closing this gap is solving the spec formalization problem: given a natural-language requirement, produce a formal artifact whose meaning matches it. To measure the gap, we curate an end-to-end benchmark for spec formalization spanning four formal languages: Dafny contracts and Lean 4, Isabelle and Rocq theorem statements. Each of its 3,234 rows pairs a natural-language requirement with a formal artifact and a label established by execution, by proof, or by the benchmark it is drawn from. A third of the rows are meaning-preserving rewrites of the artifact that keep the faithful label, so a judge cannot score by detecting that a row was edited. We introduce claimcheck, a tool that detects incorrect formalizations: the formal artifact is translated back into plain English by a model that never sees the requirement, and a separate model, the judge, decides whether the informalization and the requirement express the same guarantee. On all four languages it gains 8.2 to 9.8 points of macro recall over a single call shown the requirement and the artifact, and 4.2 to 6.0 over that call handed the same list of meaning-preserving rewrites. Showing the judge the artifact as well costs 1.4 to 4.5 points. Across four judges that also see the artifact, the gain shrinks as the judge gets stronger, to within a point of the informed single call for the strongest.

Figures & tables

Panel of Figure 1 — Figure 1: One claimcheck run, on a Dafny contract from CloverBench whose postcondition was weakened (class C2 ). Like the sorting example, the contract still verifies and is satisfied by returning zero. Step 1 translates the contract into English without ever seeing the requirement, so the informalization can only report what the contract says. Step 2 compares the informalization with the requirement and names the discrepancy; it never sees the contract. Colours follow the data: blue is the natural-language requirement, amber the formal artifact, green its informalization. A single-call baseline shown both sides at once scores lower on all four languages (Table 2 ).

	rule	Lean	Isabelle	Rocq
control	true_and	98	94	62
	or_false	98	96	66
	double_neg	97	95	57
	forall_not_exists	24	22	38
	iff_comm	21	18	25
semantic	negate	293	285	185

Table 1: The PutnamBench slices. Controls are labelled confirmed , semantic mutations disputed . A dash marks a rule that is not applied in that language; see the text.

Dafny remove_front , the slice takes the wrong end
requirement Removes the front element from the array a and returns the resulting array c .
contract method remove_front(a: array<int>) returns (c: array<int>) requires a.Length > 0 ensures a[0..a.Length - 1] == c[..]
step 1 informalize reads the contract, never the requirement “The returned array c contains the elements of array a from index 0 to a.Length - 1 (i.e. all elements except the last one).”
step 2 compare reads the requirement and the informalization disputed , wrong-property “The requirement says to remove the FRONT (first) element, but the back-translation describes removing the LAST element (slice from index 0 to a.Length-1 excludes the last element, not the first).”

Figure 2: An example claimcheck run on a Dafny contract. The contract has the right shape and one wrong index inside the slice: a[0..a.Length - 1] drops the last element where a[1..] would drop the first, so the method it describes returns the array with the wrong end removed. The contract verifies against a body that satisfies it.

	Lean	Isabelle	Rocq	Dafny
zero-shot baseline	79.7 $\pm$ 2.1	81.5 $\pm$ 1.9	79.6 $\pm$ 2.3	84.0 $\pm$ 3.8
baseline + list	83.2 $\pm$ 1.9	85.3 $\pm$ 1.8	83.0 $\pm$ 2.3	88.9 $\pm$ 3.2
claimcheck, judge sees artifact	84.8 $\pm$ 1.9	87.2 $\pm$ 1.8	83.5 $\pm$ 2.3	91.7 $\pm$ 2.8
claimcheck	87.9 $\pm$ 1.8	91.3 $\pm$ 1.7	88.0 $\pm$ 2.1	93.1 $\pm$ 2.6

Table 2: Main results. Informalizer claude-haiku-4.5 ; judge and baseline claude-sonnet-4.6 . Macro recall (mean of the confirmed and disputed recalls)

\pm

its 95% interval.

	Lean	Isabelle	Rocq	Dafny
held-out rules	88.0 $\pm$ 1.8	91.8 $\pm$ 1.7	87.5 $\pm$ 2.3	92.3 $\pm$ 2.8
no back-translation (judge sees artifact)	82.0 $\pm$ 2.0	81.9 $\pm$ 2.0	77.5 $\pm$ 2.6	86.7 $\pm$ 3.4
informalizer sees requirement	85.3 $\pm$ 1.9	89.9 $\pm$ 2.1	87.2 $\pm$ 2.6	90.1 $\pm$ 3.1

Table 3: Ablations, with the models of Table 2 . Macro recall (mean of the confirmed and disputed recalls)

\pm

its 95% interval.

Figure 3: The model sweep, with

95\%

intervals; values in Table 4 . As there, claimcheck is the variant whose judge also sees the artifact, and the claude-sonnet-4.6 row is Table 2 ’s judge under that variant.

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

	Lean	Isabelle	Rocq	Dafny
gemini : baseline	94.6 $\pm$ 1.2	94.8 $\pm$ 1.2	91.4 $\pm$ 1.9	91.4 $\pm$ 2.9
gemini : baseline + list	95.6 $\pm$ 1.1	95.2 $\pm$ 1.2	92.2 $\pm$ 1.8	95.6 $\pm$ 2.1
gemini : claimcheck	95.2 $\pm$ 1.1	96.1 $\pm$ 1.1	92.8 $\pm$ 1.8	95.3 $\pm$ 2.2
luna : baseline	63.4 $\pm$ 2.1	60.7 $\pm$ 2.1	61.1 $\pm$ 2.8	69.0 $\pm$ 4.6
luna : baseline + list	72.8 $\pm$ 2.2	75.2 $\pm$ 2.2	69.7 $\pm$ 2.6	84.0 $\pm$ 3.8
luna : claimcheck	82.0 $\pm$ 2.1	85.9 $\pm$ 2.0	82.8 $\pm$ 2.5	87.6 $\pm$ 3.3

Appendix

Table 4: Model sweep: other judges, with informalizer claude-haiku-4.5 unless stated. Macro recall (mean of the confirmed and disputed recalls)

\pm

its 95% interval. The claimcheck rows are the variant whose judge also sees the artifact.

variant	requirement	contract	label
original	Swap two integers.	ensures x==Y ensures y==X	confirmed
docstring mutated ( C1 )	Assign the second integer to the first integer.	unchanged	disputed
contract mutated ( C2 )	Swap two integers.	requires X==0 ensures x==Y ensures y==X ensures y==0	disputed
contract + body ( C6 )	Swap two integers.	ensures x==X ensures y==Y	disputed
control, meaning-preserving ( merge_ensures )	Swap two integers.	ensures (x==Y) && (y==X)	confirmed

Appendix

Table 5: Every Dafny variant on one Clover program, swap . C1 is the only class where the requirement is what is wrong: the contract is still a correct swap, but the requirement now asks for something else. C2 narrows the contract to inputs where X==0 . C6 returns the inputs unchanged. The control merges two ensures clauses into one, which changes the text but not the meaning.

Explore similar work

Oct 7, 2026

Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation

When generating verifiable code, natural language requirements are mapped to machine checked code using LLMs and agentic workflows. A crucial component of this pipeline is specification generation (SpecGen), which produces a formal contract against which an agent can prove implementation correctness. Proof generation can obtain deterministic feedback from a theorem prover, but SpecGen lacks a definitive check that a generated specification captures the user's intent. A checked proof can therefore establish correctness against a specification that misrepresents the intended behaviour. We take a step towards holistic SpecGen evaluation with a unified dataset assembled from

350

existing Lean tasks, including

189

from VERINA and

161

from CLEVER, and a framework covering formal validity, reference similarity and equivalence, and behavioural adequacy. We distinguish acceptance of required inputs from acceptance of valid outputs and rejection of invalid outputs, while making each metric's evidence scope explicit. Across four SpecGen configurations, restricting the generalized tree edit distance (GTED) comparison, a reference similarity measure, to

32

jointly measurable VERINA tasks changes the VERINA configuration's position from second to fourth in mean similarity, showing the importance of measurement coverage. In an authored control, a specification achieves

100\%

positive test recall and negative test rejection while accepting

0\%

of required inputs. This demonstrates that perfect postcondition scores can miss an unusable input contract, motivating separate feedback on input coverage and output constraints.

Srijith Nair, Aditya Vempaty, Jia Liu +1

Department of Electrical & Computer Engineering The Ohio State University · Emergence AI

Formal Verification Autoformalization

Ask PDF

May 26, 2026

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization

AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promising path: an agent generates code together with a machine-checked proof, guaranteeing that the code satisfies a formal specification. However, there is no guarantee that the formal spec itself matches the user's intent. In this work, we study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications. We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems targeting Verus, a verifier for Rust, and Verus-SpecGym, an agentic environment in which models interact with Verus, bash, & the filesystem to develop these specs. The central challenge is evaluation: expert-written reference specs are expensive to write, & LLM judges can miss subtle mistakes. We address this by (a) extending Verus's exec_spec mechanism so that generated specs can be executed as Rust code, & (b) testing them against official Codeforces tests & adversarial cases extracted from Codeforces "hacks", which are edge cases written by competitors to break incorrect solutions. On Verus-SpecBench, the strongest model, Gemini 3.1 Pro, solves 77.8% of tasks, other frontier models solve 51.1--57.8% & OSS models reach only 21.5--25.5%. Our analysis of failure modes shows that model-generated specs can omit important input assumptions, accept incorrect outputs, & reject valid ones. We also find that LLM-as-a-judge evaluation misses 26% of the failures our evaluator catches. Overall, our results suggest that spec autoformalization is within reach for frontier agents but remains brittle even on problems where they can already generate correct code. The code, data, & logs can be found at https://github.com/formal-verif-is-cool/verus-spec-gym

Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6

CMU · Amazon · Work performed while at Amazon.

LLM Agent Evaluation Formal Verification AI Agent Benchmarks Autoformalization

Ask PDF

Jun 30, 2026

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Lean verifies that a generated declaration is well typed, but not that it expresses the statement a user intended. We study two questions for autoformalization without canonical Lean targets: whether LLM judges can provide a usable proxy for human semantic review, and how much compilation overstates faithfulness across systems. Our criterion combines Lean compilation with strict semantic consensus between GPT-5.2 and Gemini-2.5-Pro. On an independently audited random sample, it agrees with human majority on 89.7% of cases (Wilson 95% CI: 82.1--94.3%). Across eight systems evaluated on 400 graduate-level statements, every system has a nonzero compile--faithfulness gap, whose observed magnitude ranges from 3.0 to 29.0 percentage points. The full GPT-5.2 tool-augmented agent shows the largest gap, compiling 89.5% while satisfying the semantic criterion on 60.5%. Human review, an independent third-family judge, and a BEq formal cross-check provide complementary evidence that the accepted core is reliable and that most audited outputs in the gap are genuine semantic mismatches. A secondary

2^3

factorial analysis shows that elaboration feedback is the largest validity intervention, yet does not eliminate semantic drift. LLM judging is therefore useful as a human-calibrated, conservative aggregate measure, not as an equivalence oracle.

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3

University of California, Riverside · University of Arizona · University of California, San Diego

LLM-as-a-Judge Lean Theorem Proving Autoformalization

Ask PDF