claimcheck

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.

Installation

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/bench-cc.js)

Same single-prompt approach piped through claude -p — no structural or prompt-level separation (the model sees everything at once). Useful for comparing whether look-ahead matters.

Usage

File mode (extract lemmas from .dfy)

# Two-pass audit (default)
claimcheck \
  -m test/integration/mappings/counter.json \
  --dfy test/integration/claims/counter.dfy \
  -d counter

# With explicit module (needed for --verify with module-based .dfy files)
claimcheck \
  -m test/integration/mappings/counter.json \
  --dfy test/integration/claims/counter.dfy \
  --module CounterDomain -d counter --verify

# Single-prompt audit
claimcheck \
  -m test/integration/mappings/counter.json \
  --dfy test/integration/claims/counter.dfy \
  -d counter --single-prompt --json

Stdin mode (pure JSON-in/JSON-out)

Pre-extract your claims and pipe them in:

echo '{
  "claims": [
    {
      "requirement": "The counter value is always non-negative",
      "lemmaName": "CounterNonNegative",
      "dafnyCode": "lemma CounterNonNegative(m: int)\n  requires Inv(m)\n  ensures m >= 0\n{}"
    }
  ],
  "domain": "counter"
}' | claimcheck --stdin

Library usage

import { claimcheck } from 'claimcheck';

const { results, tokenUsage } = await claimcheck({
  claims: [
    {
      requirement: 'The counter value is always non-negative',
      lemmaName: 'CounterNonNegative',
      dafnyCode: 'lemma CounterNonNegative(m: int)\n  requires Inv(m)\n  ensures m >= 0\n{}',
    },
  ],
  domain: 'counter',
});

Tests and benchmarks

# All test projects
node test/integration/run-all.js

# Single test project
node test/integration/run-all.js counter

# Run benchmarks
node eval/bench.js --runs 3 --label two-pass
node eval/bench.js --runs 3 --label single-prompt --single-prompt
node eval/bench-cc.js --runs 1 --label cc-sonnet

# Run a single domain or lemma
node eval/bench-cc.js --runs 1 --label test --domain counter
node eval/bench-cc.js --runs 1 --label test --domain counter --lemma CounterNonNegative

# Compare results
node eval/compare.js two-pass single-prompt
node eval/compare.js two-pass cc-sonnet

Options

Flag	Description
-m, --mapping <path>	Path to mapping file (JSON: [{requirement, lemmaName}, ...])
--dfy <path>	Path to claims .dfy file (contains the lemmas)
--module <name>	Dafny module name (optional; needed for --verify with module-based files)
-d, --domain <name>	Human-readable domain name (default: from --module or .dfy filename)
--json	Output JSON instead of markdown
--single-prompt	Use single-prompt claimcheck mode (one call per pair)
--model <id>	Model for single-prompt mode (default: sonnet)
--verify	Also run dafny verify on each lemma
--informalize-model <id>	Model for back-translation in two-pass mode (default: haiku)
--compare-model <id>	Model for comparison in two-pass mode (default: sonnet)
--stdin	Read JSON from stdin (pure claimcheck, no file extraction)
-v, --verbose	Verbose API/verification logging

Output

For each mapping entry, one of:

Status	Meaning
confirmed	Round-trip passed — lemma faithfully expresses the requirement
disputed	Round-trip failed — discrepancy between lemma meaning and requirement
verify-failed	Dafny verification failed (only with --verify flag)
error	Lemma not found in source

In single-prompt mode, disputed results include richer detail: verdict category, vacuity analysis, and surprising restrictions.

Test Projects

Project	Claims file	Domain module
counter	test/integration/claims/counter.dfy	CounterDomain
kanban	test/integration/claims/kanban.dfy	KanbanDomain
colorwheel	test/integration/claims/colorwheel.dfy	ColorWheelDomain
canon	test/integration/claims/canon.dfy	CanonDomain
delegation-auth	test/integration/claims/delegation-auth.dfy	DelegationAuthDomain

Each claims file includes its domain from ../dafny-replay/. Mappings in test/integration/mappings/.

Benchmark Results

Accuracy across 5 domains (counter, kanban, colorwheel, canon, delegation-auth) with 36 requirement-lemma pairs, including 8 deliberately bogus lemmas (tautologies, weakened postconditions, narrowed scope):

Variant	Accuracy	Time/run	API calls/run
Two-pass (default)	96.3% (104/108)	~108s	2 (batch informalize + batch compare)
Single-prompt	86.1% (31/36)	~353s	36 (one per pair)
Claude Code (bench-cc)	69.4% (25/36)	~693s	36 (one claude -p per pair)

Two-pass had 3 runs; single-prompt and Claude Code had 1 run each.

Key takeaways:

• Structural separation (two-pass) is both the most accurate and fastest
• The informalize-without-seeing-requirement step prevents anchoring bias
• Batching into 2 API calls vs 36 individual calls gives a ~3x speed advantage
• Claude Code's general-purpose system prompt and lack of structured output hurt both accuracy and speed

Requirements

• Node.js 18+
• ANTHROPIC_API_KEY environment variable
• dafny in PATH (only for --verify)
• dafny-replay cloned as a sibling directory (required for tests and benchmarks — the claims .dfy files include domain files from ../../dafny-replay/)