claimcheck: Keeping LLM-Written Formal Specifications from Going Off the Rails

Title

claimcheck: Keeping LLM-Written Formal Specifications from Going Off the Rails

Meta Description

A new claimcheck paper proposes a tool for detecting semantic drift in formal specifications: using back-translation and an independent judge to determine whether a specification is faithful to natural language requirements, covering a 3,234-line benchmark across Dafny, Lean 4, Isabelle, and Rocq, with macro recall improvements of up to 9.8 percentage points.

Article Content

Formal verification can prove that a program satisfies its specification, but it cannot tell us whether the specification truly expresses the author's intent. Now that LLMs have begun writing both code and specifications, the semantic gap between natural language requirements and formal artifacts has become a real risk—a machine-checked proof of a property narrower than the requirement is worthless, yet it can pass every check. The claimcheck proposed in this paper exists precisely to fill this gap.

Specification Formalization: A Neglected Systemic Risk

The paper explicitly names this gap the "spec formalization problem": given a natural language requirement, produce a formal artifact whose semantics match it. The core of the problem lies in the directionality of the verification chain—formal verification only guarantees that "code satisfies the specification," but says nothing about whether "the specification is faithful to the requirement."

When human engineers write specifications by hand, this gap can still be bridged through repeated communication. But in scenarios where LLMs mass-produce code and specifications, verification passing while verifying the wrong thing becomes a systemic risk. If a formally proven property is narrower than the requirement, the technical success of the proof instead creates a false sense of security.

Formal verification refers to the technique of using mathematical methods to prove that a program satisfies its formal specification, with common approaches including theorem proving (such as Coq, Isabelle, and Lean) and model checking. Its core is constructing a machine-checkable proof confirming that all possible behaviors of the program fall within the set allowed by the specification.

A specification is a formal statement describing what a program "should do," usually written as preconditions, postconditions, and invariants. The reliability of verification depends entirely on the correctness of the specification: verification tools only answer "does the code satisfy the specification," not "does the specification match the intent." This is precisely the technical root of the problem the paper points to—the establishment of a formal proof and whether that proof is meaningful are two independent matters.

A Four-Language End-to-End Benchmark: The Design Ingenuity of 3,234 Lines of Data

To quantify this gap, the authors built an end-to-end benchmark covering four formal languages: Dafny contracts, Lean 4, Isabelle, and Rocq theorem statements. Each line pairs a natural language requirement with a formal artifact, with labels established by execution, proof, or benchmark source, totaling 3,234 lines.

The most noteworthy aspect of the benchmark design is its anti-cheating mechanism: one-third of the samples are meaning-preserving rewrites of formal artifacts, with labels still marked as faithful. This means a judge cannot simply score based on "this line was edited"—it must genuinely understand semantic equivalence. This design pushes the benchmark out of the comfort zone of pattern matching and into the deep waters of semantic understanding.

Dafny is a verification-aware programming language developed by Microsoft Research that writes programs and specifications in the same place, with a built-in verifier automatically generating verification conditions and invoking Z3 to solve them. Lean 4 combines a functional programming language with an interactive theorem prover, and has attracted widespread attention in recent years due to mathematical formalization projects. Isabelle is a general-purpose theorem prover based on higher-order logic, emphasizing human-readable proof scripts. Rocq (formerly Coq) is a proof assistant based on the calculus of inductive constructions, with a long track record in program verification and mathematical formalization.

The four languages cover two paradigms—"verification embedded within a programming language" and "standalone theorem proving"—enabling the benchmark to test the generalizability of methods across language styles.

How claimcheck Works: Back-Translation + Independent Judge

The core idea of claimcheck is "reverse verification": first translate the formal artifact back into natural language, with the translation model never having seen the original requirement; then an independent judge model determines whether this "de-formalized artifact" and the original requirement express the same guarantee.

The ingenuity of this design lies in cutting off the information leakage path. If the translation model sees the requirement, it may unconsciously gravitate toward it, masking the true semantics of the formal artifact. Only by having the translation model face the formal artifact alone can we obtain an "honest translation."

Back-translation originally referred in machine translation to translating a translation back into the source language to evaluate quality. claimcheck borrows this idea, but with a key difference: the translation model cannot see the original requirement, so the translation will not be "contaminated" by the requirement.

The design of the independent judge draws on the "isolation principle" in evaluation—the judge should not be exposed to information that might introduce bias. Having the judge see only the natural language requirement and the back-translation result prevents it from being drawn to the syntactic structure or proof state of the formal artifact, allowing it to focus more on judging semantic equivalence.

Experimental Results: Significant Improvement in Macro Recall

Across four formal languages, claimcheck achieved macro recall improvements of 8.2 to 9.8 percentage points compared to a single call (showing both the requirement and the artifact simultaneously); even when the baseline was given the same list of meaning-preserving rewrites, claimcheck still led by 4.2 to 6.0 percentage points.

A key finding is that letting the judge also see the formal artifact costs 1.4 to 4.5 percentage points of performance. This hints at the value of the independent judge—when the judge is drawn to the surface structure of the formal artifact, its sensitivity to the semantic gap actually decreases.

The study also reveals an interesting trend that varies with model capability: among the four judges that also saw the artifact, the stronger the model, the smaller claimcheck's gain, with the strongest judge approaching the level of "informed single call." This suggests that sufficiently capable models may have internalized part of the semantic equivalence judgment ability, but for current mainstream models, claimcheck's structured process still brings substantial benefits.

Implications for the AI Programming Toolchain

This work points to a broader engineering practice issue: in LLM-assisted programming workflows, specification correctness checking cannot be separated from code verification. The approach offered by claimcheck—using an independent model to back-translate formal artifacts and then compare them against requirements—can be embedded into CI pipelines as a semantic gate before formal verification.

For teams in the process of introducing formal methods, the benchmark in this paper itself has practical value: a four-language, 3,234-line test set with anti-cheating design can serve as a yardstick for evaluating one's own specification generation pipeline. As the cost of formal verification continues to fall, ensuring that "the right thing is being verified" will become the next bottleneck.

CI (continuous integration) is a pipeline in software development for automated building, testing, and verification. Embedding claimcheck into CI means that every specification change automatically triggers a semantic equivalence check, intercepting the problem of "specification deviating from requirements" before formal verification.

This kind of "semantic gate" complements traditional type checking and unit testing: type checking ensures structural validity, unit testing samples behavior, formal verification covers all behavior, and claimcheck guards the premise of verification—whether the specification itself has been correctly understood.

One-line Summary

claimcheck uses back-translation and an independent judge to detect whether LLM-generated specifications are faithful to natural language requirements, improving macro recall by 8.2-9.8 percentage points.

Paragraph Summary

The paper points out that formal verification only guarantees that code satisfies the specification, but cannot guarantee that the specification is faithful to natural language requirements. When LLMs generate both code and specifications, this gap becomes a systemic risk, called the "spec formalization problem." The authors built a 3,234-line end-to-end benchmark covering four formal languages—Dafny, Lean 4, Isabelle, and Rocq—one-third of which consists of meaning-preserving rewrites to prevent cheating. claimcheck adopts a "back-translation + independent judge" architecture: the translation model does not see the original requirement, first translating the formal artifact into natural language, after which an independent judge determines whether the translation and the requirement express the same guarantee. Experiments show macro recall improvements of 8.2-9.8 percentage points, and having the judge also view the formal artifact actually costs 1.4-4.5 percentage points. The stronger the judge model, the smaller claimcheck's gain relative to an informed single call.