Midspiral
As LLMs become more capable of writing code, the programmer's role shifts from implementation to describing intent.
Core trick
Translates Dafny lemmas back to English without seeing the requirement, then compares that English against the requirement with a second model call.
Tags
Description
As LLMs become more capable of writing code, the programmer's role shifts from implementation to describing intent. Two major open questions emerge in AI programming: 1) How do we know AI-generated code is correct, not just plausible? 2) How do we know the code accurately captures the programmer's intent? Our recent work addresses the first question by adding formal verification to the AI code generation loop — forcing the AI to mathematically prove its code is correct. But the second question remains: does the proved specification capture the intent?
Claimcheck closes the gap between “the code is guaranteed correct” and “the code makes the intended guarantees.” We use the Claude API to conduct round-trip informalization: it translates formal language to English without knowledge of the initial input. It then compares the intent to the guarantee to ensure they match.
On 108 comparisons, it got 96.3% correct in 2 API calls per run batched per file.
README excerpt
# claimcheck Does a Dafny lemma actually mean what a natural language requirement says? Dafny can verify proofs, but it can't verify meaning. Claimcheck fills that gap. Someone else (Claude Code, a human, any agent) writes the lemmas and claims "requirement X is covered by lemma Y." Claimcheck verifies that claim via a round-trip: informalize the lemma back to English (without seeing the requirement), then compare. [Blog post: _claimcheck: Narrowing the Gap between Proof and Intent_](https://midspiral.com/blog/claimcheck-narrowing-the-gap-between-proof-and-intent/). ## Installation ```bash npm install -g claimcheck ``` or ```bash npm install npm link ``` ## Modes ### Two-pass mode (default) Structural separation — different models for informalization and comparison: ``` 1. Extract mapped lemmas from claims .dfy file 2. Batch informalize all lemmas (haiku) — does NOT see requirements 3. Batch compare back-translations against requirements (sonnet) 4. Report: confirmed / disputed ``` ### Single-prompt mode (`--single-prompt`) Prompt-level separation — one model does both passes sequentially: ``` 1. Extract mapped lemmas from claims .dfy file 2. For each mapping: single LLM call with two-pass prompt a. Pass 1: informalize the lemma (before seeing the NL requirement) b. Pass 2: compare, check vacuity, flag surprising restrictions 3. Report with richer verdicts: JUSTIFIED / PARTIALLY_JUSTIFIED / NOT_JUSTIFIED / VACUOUS ``` ### Claude Code benchmark (`eval/benc