Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/metareflection/claimcheck/llms.txt

Use this file to discover all available pages before exploring further.

Claimcheck can receive its input three different ways depending on where you are in your workflow. File mode is the standard path: point it at a .dfy source file and a mapping JSON, and it extracts the lemma text automatically. Stdin mode skips extraction entirely — you supply pre-built claim objects over a pipe, which is useful for programmatic integrations and CI steps that already have the Dafny code in memory. Multi-domain mode, provided by the claimcheck-multi command, handles projects where lemmas are spread across several .dfy files and runs them in parallel sub-processes before merging the results.

​
File mode

File mode is the default. Pass a mapping file and a .dfy source file; claimcheck extracts each lemma by name and then runs the audit. 
claimcheck \
  -m mapping.json \
  --dfy claims.dfy \
  -d mydomain

​
How the mapping file works

The mapping file (-m / --mapping) is a JSON array. Each entry pairs a natural language requirement with the name of the Dafny lemma that is claimed to formalise it: 
[
  { "requirement": "The counter value is always non-negative", "lemmaName": "CounterNonNegative" },
  { "requirement": "A task cannot move from Done back to In Progress", "lemmaName": "NoRegressionFromDone" }
]
Claimcheck iterates through the array in order. If a lemmaName is not found in the .dfy source, that entry is reported with status error.

​
How lemmas are extracted

Claimcheck reads the full .dfy source text and locates each lemma by matching its identifier. The extracted text includes the lemma signature and body. If the .dfy file uses Dafny modules and you also want to run --verify, pass --module <ModuleName> so that the Dafny verifier can resolve the module scope correctly. The --module flag is not required for the LLM audit itself.

​
Example: file mode with verification

claimcheck \
  -m test/integration/mappings/counter.json \
  --dfy test/integration/claims/counter.dfy \
  --module CounterDomain \
  -d counter \
  --verify
dafny must be in PATH when using --verify. Lemmas that fail verification are reported as verify-failed and are excluded from the LLM round-trip.

​
Stdin mode

In stdin mode (--stdin), claimcheck reads a JSON object from standard input. You provide the dafnyCode for each claim directly — no .dfy file is needed. This is the right choice when a build system, agent, or CI pipeline has already assembled the claims programmatically. 
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
The input object has two fields:
FieldTypeRequiredDescription
claimsarrayYesArray of claim objects, each with requirement, lemmaName, and dafnyCode.
domainstringNoDomain name for context. Defaults to "unknown" if omitted.
Output is always JSON in stdin mode, regardless of whether --json is passed. The result schema is the same as the JSON output format.

​
Library usage

The same interface is available as a JavaScript module: 
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',
});

​
Multi-domain mode (claimcheck-multi)

claimcheck-multi is a separate command for projects where lemmas live in multiple .dfy files. It accepts a mapping that includes a file field on each entry, groups the entries by file, dispatches one claimcheck subprocess per file, and merges the results into a single report. 
claimcheck-multi \
  -m multi-mapping.json \
  -d myproject \
  --json

​
Multi-domain mapping format

Each entry in the mapping must include a file field that resolves relative to the mapping file’s own directory: 
[
  {
    "requirement": "The counter value is always non-negative",
    "lemmaName": "CounterNonNegative",
    "file": "claims/counter.dfy"
  },
  {
    "requirement": "A task cannot move from Done back to In Progress",
    "lemmaName": "NoRegressionFromDone",
    "file": "claims/kanban.dfy"
  }
]
Entries without a file field fall back to the --dfy flag if provided; if neither is present, claimcheck-multi exits with an error.

​
How claimcheck-multi works

1

Group entries by file

Claimcheck-multi resolves each file path relative to the mapping file and groups entries by resolved absolute path.
2

Write per-file temp mappings

For each group, a temporary mapping JSON (without file fields) is written to a system temp directory.
3

Invoke claimcheck per file

Each group is dispatched as a separate node claimcheck.js subprocess with the appropriate --dfy path and a shared set of passthrough flags (mode, model, backend, verbosity). Subprocesses always receive --json so results can be parsed and merged.
4

Merge and output

Results from all subprocesses are reassembled in original mapping order and emitted as a single merged report. Pass --json to receive the merged output as JSON; otherwise a Markdown summary is printed.

​
All claimcheck flags are supported

claimcheck-multi accepts and forwards the same flags as claimcheck: 
claimcheck-multi \
  -m multi-mapping.json \
  -d myproject \
  --single-prompt \
  --model claude-sonnet-4-6 \
  --verify \
  --vertex \
  --vertex-project my-gcp-project \
  --json
See CLI options and flags reference for the full flag list.

​
When to use each mode

File mode

Typical workflow. You have a .dfy file with lemmas and a mapping JSON. Claimcheck handles extraction automatically. Use --verify to gate on proof correctness before the LLM audit.

Stdin mode

Programmatic and CI use. A script, agent, or pipeline already holds the Dafny code as a string. Pipe it in and get JSON back. No filesystem dependency on a .dfy file.

Multi-domain

Large projects. Lemmas are spread across multiple .dfy files organised by bounded context or module. claimcheck-multi runs each file’s lemmas concurrently and returns a unified report.

Build docs developers (and LLMs) love

Get started for freeTalk to us