Understanding Claimcheck output

Every requirement-lemma pair that claimcheck audits produces a result with a status and a set of supporting fields that explain the verdict. By default the report is Markdown, suitable for reading in a terminal or pasting into a pull request. Pass --json to get a machine-readable object suitable for CI pipelines, dashboards, or downstream tooling. This page explains what each status means, what the Markdown report looks like, the full JSON schema, and the nested sub-objects that carry informalization and comparison detail.

Statuses

Status	Meaning	Recommended action
`confirmed`	The round-trip passed — the lemma’s back-translated meaning matches the requirement.	No action needed.
`disputed`	The round-trip failed — a meaningful discrepancy exists between what the lemma guarantees and what the requirement states.	Review `discrepancy` and `weakeningType`, then fix the lemma or refine the requirement.
`verify-failed`	Dafny verification failed for this lemma (only possible when `--verify` is used). The lemma may not actually be proved.	Fix the Dafny proof before re-running the audit.
`error`	The lemma name was not found in the `.dfy` source file.	Check that `lemmaName` in the mapping matches the exact lemma identifier in the source.

Markdown output (default)

The default report groups results into sections: Confirmed Mappings, Disputed Mappings, Verification Failures, and Errors. A summary at the top shows counts for each category. Confirmed mapping example:

# Audit Report: counter

## Summary

- **Mappings audited:** 1
- **Confirmed:** 1

## Confirmed Mappings

**The counter value is always non-negative**
- Lemma: `CounterNonNegative`
- Back-translation: Given a counter state satisfying Inv, the counter value is at least zero.
```dafny
lemma CounterNonNegative(m: int)
  requires Inv(m)
  ensures m >= 0
{}

Disputed mapping example:

## Disputed Mappings

**The counter can never overflow**
- Lemma: `CounterBounded`
- Discrepancy: The lemma only ensures the value is non-negative, not that it is bounded above.
- Weakening: narrowed-scope
- Back-translation: Given Inv holds, the counter value is greater than or equal to zero.
```dafny
lemma CounterBounded(m: int)
  requires Inv(m)
  ensures m >= 0
{}

A footer line reports token usage when the Anthropic API was called: *API usage: 1240 input tokens, 312 output tokens*.

JSON output (`--json`)

Pass --json to receive a single JSON object on stdout. The top-level shape:

domain

string

required

The domain name passed via -d or derived from --module / the .dfy filename.

timestamp

string

required

ISO 8601 timestamp of when the audit completed.

results

object[]

required

Array of per-claim result objects. One entry per mapping entry. See the Result object section below.

tokenUsage

object

required

Aggregate token counts for the entire audit run.

Show properties

input

number

required

Total input tokens consumed across all API calls.

output

number

required

Total output tokens generated across all API calls.

Result object

Each entry in results contains:

requirement

string

required

The natural language requirement string from the mapping file.

lemmaName

string

required

The Dafny lemma identifier from the mapping file.

status

string

required

One of confirmed, disputed, verify-failed, or error.

dafnyCode

string

The extracted Dafny lemma source text. Present on all results except error (where the lemma could not be found).

informalization

object

The back-translation produced during the informalization step (two-pass and single-prompt modes). Absent on error results.

Show properties

naturalLanguage

string

required

Plain English statement of what the lemma guarantees, derived from the code alone without seeing the requirement.

preconditions

string

required

English description of the requires clauses — what must hold before the lemma applies.

postcondition

string

required

English description of the ensures clauses — what the lemma guarantees.

scope

string

required

What the lemma applies to: a single state, a transition, all reachable states, etc.

strength

string

required

How strong the claim is. One of trivial, weak, moderate, or strong. A trivial lemma’s ensures clause restates its requires or is a tautology.

confidence

number

required

Confidence (0–1) that the back-translation faithfully represents the Dafny code.

comparison

object

The result of comparing the back-translation against the requirement (two-pass mode). In single-prompt mode this object also contains a nested claimcheck field with richer verdict detail. Absent on error results.

Show properties

requirementIndex

number

required

Zero-based index of the requirement in the original mapping array.

lemmaName

string

required

Name of the lemma that was compared.

match

boolean

required

true if the lemma faithfully expresses the requirement; false if a meaningful discrepancy was found.

discrepancy

string

required

When match is false, a description of exactly what the lemma gets wrong or misses.

weakeningType

string

required

Category of weakening detected, or none if match is true. See Weakening types below.

explanation

string

required

Brief reasoning that explains how the comparison verdict was reached.

claimcheck

object

Present only in single-prompt mode (--single-prompt). Contains the richer per-pair verdict from the combined informalize-and-compare call.

Show properties

verdict

string

required

One of JUSTIFIED, PARTIALLY_JUSTIFIED, NOT_JUSTIFIED, or VACUOUS.

vacuous

boolean

required

true if the ensures clause literally restates a requires clause without unfolding any definitions. Note: extracting a consequence from an invariant (e.g. requires Inv(m); ensures m >= 0) is not considered vacuous.

vacuousExplanation

string

required

Explanation when vacuous is true; empty string otherwise.

ensuresMatchesNL

string

required

One of Yes, Partially, or No — does the ensures clause express the natural language claim?

ensuresExplanation

string

required

Explanation of the ensures-vs-requirement comparison. Always populated when ensuresMatchesNL is not Yes.

surprisingRestrictions

string

required

Any requires clauses that restrict when the property holds in a way the natural language does not mention. "None" if there are no surprising restrictions.

discrepancy

string

Top-level copy of the discrepancy description. Present on disputed results for convenient access without traversing the comparison object.

weakeningType

string

Top-level copy of the weakening type. Present on disputed results. See Weakening types below.

error

string

Error message. Present on error and verify-failed results only.

Weakening types

The weakeningType field categorises how a disputed lemma falls short of its requirement:

Value	Meaning
`none`	No weakening — lemma matches the requirement (`confirmed` results).
`tautology`	The `ensures` clause is trivially true regardless of inputs, so the lemma proves nothing meaningful.
`weakened-postcondition`	The lemma’s conclusion is strictly weaker than what the requirement states.
`narrowed-scope`	The lemma applies only to a subset of states or transitions that the requirement covers.
`missing-case`	The lemma omits a case that the requirement explicitly includes.
`wrong-property`	The lemma proves a different property to the one stated in the requirement.

JSON examples

Confirmed result

{
  "domain": "counter",
  "timestamp": "2024-11-01T10:23:45.123Z",
  "results": [
    {
      "requirement": "The counter value is always non-negative",
      "lemmaName": "CounterNonNegative",
      "status": "confirmed",
      "dafnyCode": "lemma CounterNonNegative(m: int)\n  requires Inv(m)\n  ensures m >= 0\n{}",
      "informalization": {
        "naturalLanguage": "Given a counter state satisfying the invariant, the counter value is at least zero.",
        "preconditions": "The counter state m satisfies the invariant Inv.",
        "postcondition": "The counter value m is greater than or equal to zero.",
        "scope": "Any single counter state that satisfies the invariant.",
        "strength": "moderate",
        "confidence": 0.97
      },
      "comparison": {
        "requirementIndex": 0,
        "lemmaName": "CounterNonNegative",
        "match": true,
        "discrepancy": "",
        "weakeningType": "none",
        "explanation": "The back-translation faithfully captures non-negativity under the invariant, matching the requirement."
      }
    }
  ],
  "tokenUsage": {
    "input": 1240,
    "output": 312
  }
}

Disputed result

{
  "domain": "counter",
  "timestamp": "2024-11-01T10:24:10.456Z",
  "results": [
    {
      "requirement": "The counter can never overflow a 32-bit integer",
      "lemmaName": "CounterBounded",
      "status": "disputed",
      "dafnyCode": "lemma CounterBounded(m: int)\n  requires Inv(m)\n  ensures m >= 0\n{}",
      "informalization": {
        "naturalLanguage": "Given a counter state satisfying the invariant, the counter value is at least zero.",
        "preconditions": "The counter state m satisfies the invariant Inv.",
        "postcondition": "The counter value m is greater than or equal to zero.",
        "scope": "Any single counter state that satisfies the invariant.",
        "strength": "weak",
        "confidence": 0.95
      },
      "comparison": {
        "requirementIndex": 0,
        "lemmaName": "CounterBounded",
        "match": false,
        "discrepancy": "The lemma only proves non-negativity, not that the value is bounded above by 2^31 - 1.",
        "weakeningType": "narrowed-scope",
        "explanation": "The requirement states an upper bound; the lemma only establishes a lower bound."
      },
      "discrepancy": "The lemma only proves non-negativity, not that the value is bounded above by 2^31 - 1.",
      "weakeningType": "narrowed-scope"
    }
  ],
  "tokenUsage": {
    "input": 1380,
    "output": 298
  }
}

Use --json combined with jq to filter results in CI. For example, to fail a build when any disputed results exist:

claimcheck -m mapping.json --dfy claims.dfy -d mydomain --json \
  | jq 'if (.results | map(select(.status == "disputed")) | length) > 0 then error else . end'

Get Started

How It Works

CLI Reference

Library & Backends

Benchmarks

Guides

Understanding Claimcheck output

Statuses

Markdown output (default)

JSON output (`--json`)

Result object

Weakening types

JSON examples

Confirmed result

Disputed result

Build docs developers (and LLMs) love

Get Started

How It Works

CLI Reference

Library & Backends

Benchmarks

Guides

Documentation Index

​Statuses

​Markdown output (default)

​JSON output (--json)

​Result object

​Weakening types

​JSON examples

​Confirmed result

​Disputed result

Build docs developers (and LLMs) love

Statuses

Markdown output (default)

JSON output (`--json`)

Result object

Weakening types

JSON examples

Confirmed result

Disputed result