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 is available as a Node.js library with two named exports. This page documents both exports: claimcheck for pure JSON-in/JSON-out audits where you supply pre-extracted Dafny lemmas, and audit for file-based workflows that handle lemma extraction, optional Dafny verification, and claim checking in a single call.
Installation Exports The package exposes two entry points:
Import path Export Purpose "claimcheck"claimcheckPure JSON-in/JSON-out audit "claimcheck/audit"auditFile-based lemma extraction and verification
claimcheck()Import from the root entry point:
import { claimcheck } from 'claimcheck' ;
Runs a round-trip audit on pre-extracted claims. No file I/O, no side effects. Accepts an array of {requirement, lemmaName, dafnyCode} objects and returns structured results for each one.
Parameters Array of claim objects to audit. Each object must have the following shape: The natural language requirement the lemma is supposed to express.
The Dafny lemma name, used to match results back to inputs.
The full Dafny lemma source text. Claims with an empty or missing value are returned immediately with status: "error".
Human-readable domain name passed to the LLM as context (e.g. "counter", "kanban").
Optional configuration for the audit run. Use single-prompt mode: one LLM call per requirement-lemma pair instead of two batched calls. Produces richer verdicts (JUSTIFIED, PARTIALLY_JUSTIFIED, NOT_JUSTIFIED, VACUOUS) but is slower.
Use naive mode: one LLM call per pair with no structured reasoning. Intended as an ablation baseline; not recommended for production use.
Override the default model for single-prompt and compare steps. Defaults to the backend’s sonnet model.
Override the model used for the informalization (back-translation) step in two-pass mode. Defaults to the backend’s haiku model.
Override the model used for the comparison step in two-pass mode. Defaults to the backend’s sonnet model.
Enable verbose API and verification logging.
Custom logging function. Defaults to console.error. Receives progress messages during the audit.
Return value Returns a Promise that resolves to an object with the following fields:
One result object per input claim, sorted in the original claim order. The original natural language requirement.
Audit outcome. One of:
"confirmed" — round-trip passed; lemma faithfully expresses the requirement."disputed" — round-trip failed; discrepancy detected between lemma meaning and requirement."error" — input error (empty or missing dafnyCode). The Dafny source for this lemma. Present on confirmed and disputed results.
The LLM’s back-translation of the lemma into natural language. Present on confirmed and disputed results.
The LLM’s comparison result between the back-translation and the original requirement. Present on confirmed and disputed results.
Human-readable description of the mismatch. Present only on disputed results.
Category of the detected weakening. Present only on disputed results. One of "tautology", "wrong-property", "weakened-postcondition", "narrowed-scope", or "none".
Error message. Present only on error results.
Aggregate token consumption for the audit run. Show tokenUsage properties
Total input tokens consumed.
Total output tokens consumed.
Example 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' , });
audit()Import from the audit entry point:
import { audit } from 'claimcheck/audit' ;
A higher-level wrapper over claimcheck() that handles lemma extraction from a .dfy source file, optional Dafny verification, and threading expected fields from the mapping back into results. Use this when you have a mapping file and a .dfy source on disk.
Parameters Array of requirement-to-lemma mapping entries. Show mapping entry properties
The natural language requirement.
Name of the Dafny lemma in dfySource that is claimed to express this requirement.
expected
string
default: "\"confirmed\""
The expected audit outcome, used for evaluation. Typical values are "confirmed" and "disputed".
Full Dafny source text. audit() uses this to extract each lemma named in mapping.
Absolute path to the .dfy file on disk. Required by dafny verify when opts.verify is true.
Dafny module name. Only needed when opts.verify is true and the .dfy file uses module-scoped declarations.
Human-readable domain name passed to the LLM as context.
Optional configuration. Accepts all options from claimcheck() plus: Run dafny verify on each extracted lemma before the LLM audit. Lemmas that fail verification are returned with status: "verify-failed" and are not passed to claimcheck().
Custom logging function. Defaults to console.error.
Enable verbose API and verification logging.
Use single-prompt mode for the underlying claimcheck() call.
Override the default model.
Override the informalization model (two-pass mode only).
Override the comparison model (two-pass mode only).
Return value Returns a Promise that resolves to an object[]. Each entry corresponds to one mapping entry, sorted in the original mapping order.
Per-mapping results. Zero-based position of this entry in the original mapping array.
The original natural language requirement.
The expected outcome from the mapping entry (defaults to "confirmed").
Audit outcome. One of "confirmed", "disputed", "verify-failed", or "error".
Extracted Dafny lemma source. Present on all statuses except "error" (lemma not found).
Back-translation produced by the LLM. Present on confirmed and disputed results.
Comparison result from the LLM. Present on confirmed and disputed results.
Description of the mismatch. Present on disputed results.
Error or verification failure message. Present on error and verify-failed results.
audit() requires dafny to be on your PATH only when opts.verify is true. For LLM-only audits, no Dafny installation is needed.
