# claimcheck: Measuring and Improving Specification Faithfulness

arXiv: https://arxiv.org/abs/2610.17358 · HTML: https://mlsanity.com/paper/2610.17358/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 30 of its 38 references that are in the map.
- First posted on arXiv 12 Oct 2026.

## Builds on (most cited first, 30 of 30)

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Large Language Models are not Fair Evaluators](https://mlsanity.com/paper/2305.17926/) (2023)
- [LLM Evaluators Recognize and Favor Their Own Generations](https://mlsanity.com/paper/2404.13076/) (2024)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements](https://mlsanity.com/paper/2606.16541/) (2026)
- [Judging Against the Reference: Uncovering Knowledge-Driven Failures in LLM-Judges on QA Evaluation](https://mlsanity.com/paper/2601.07506/) (2026)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [Anchoring Bias in LLM-as-a-Judge Systems: Prior Scores Compromise Evaluation Independence](https://mlsanity.com/paper/2608.25869/) (2026)

## Abstract (arXiv)

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.