claimcheck: Measuring and Improving Specification Faithfulness

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, the risk of a gap between the author's natural-language requirement and the specification emerges. 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 detect this problem, we curate an end-to-end benchmark for spec formalization spanning across domains, Dafny contracts, Lean and SQL queries. Each task pairs a natural-language requirement with a formal artifact and a human-checked label. We measure success with a standardized grading script and establish baselines for frontier models. 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. Because the informalization is written without sight of the requirement, it reports what the formal artifact says rather than what the requirement leads a reader to expect, and judging against it catches subtle drift such as weakened postconditions and narrowed scope.