Sessions and claims
The claims stage extracts concrete claims from a summary file, an agent session file, or commit messages, and checks each one against the diff and the clean-room result.
Where claims text comes from
The strongest available source wins, in this order:
--claims <file>: any free-text file, read as-is.--session <file>: an agent session file; format auto-detected. If the file's format cannot be parsed, paranoid falls back to the range's commit messages.- If neither flag is given at all, the claims stage does not run.
The commit-message fallback only triggers when a
--session file is given but its format fails to
parse. With neither flag, the claims stage does not run, not even as a skipped check, and CLM001 to CLM006 do not
appear in that run's findings.
Supported agents
--session <file> accepts any of the formats
below; paranoid auto-detects the format from the file's
content. It tries the parsers in a fixed order, most specific
format first, so no format flag is needed.
| Agent | Session flag | What gets extracted |
|---|---|---|
| Claude Code | --session path/to/session.jsonl | Assistant turns from the session JSONL (modern block-array shape and the legacy plain-string shape) |
| Codex CLI | --session path/to/rollout.jsonl | Assistant text from response_item payload lines |
| Gemini CLI | --session path/to/checkpoint.json | Text of every "model"-role turn (Gemini's name for the assistant), from a JSON array or one turn per line |
| Aider | --session path/to/.aider.chat.history.md | The assistant's reply text between one "#### " user line and the next |
| Cursor | --session path/to/exported-chat.md | Text following an Assistant/Cursor speaker marker, up to the next marker |
--claude-session <file> is a hidden alias for
--session.
None of these five formats is a documented, versioned API; each vendor can change its session file's shape at any time. Every parser checks the shape of the input and skips any line or block it does not recognize without raising an error. A file that yields no usable text falls back to a weaker claims source (commit messages, then a skipped check) and the run does not fail. Extraction is best effort.
Claims rules (CLM)
| Rule | Severity | What it catches |
|---|---|---|
| CLM001 | medium | The agent claims to have changed a file the diff never touches |
| CLM002 | critical | The agent claims tests pass, but the clean-room run failed |
| CLM003 | low | A claimed action names an identifier the changed files never mention |
| CLM004 | medium | The agent claims N new tests; the diff contains fewer |
| CLM005 | low | The diff touches far more files than the claims describe |
| CLM006 | medium | The agent claims a proof, but no .lean or .v file changed |
CLM005 needs a diff of at least 6 files (lockfiles and manifests
the deps package already recognizes, like
package-lock.json and go.mod, never
count either way) before it looks at the ratio, and fires when
more than 60% of those files are neither a path the claims
mention nor a file containing an identifier the claims name.
CLM006 fires once per claim line that says something was
proved, proven, formally verified, or machine-checked (or that a
proof was written or added) when the diff touches no
.lean or .v file. Plain "verified" does
not count. Full rule text, including known false positives, is on the
rules page.
API surface rules
Two more rules, AS001 and AS002, only run when claims are present. They diff public symbols (Go, Python, JS/TS) between base and head and flag a symbol removed while the claims say a fix or feature landed, cross-checked against the whole head tree so a symbol that moved does not fire. With no claims source, this stage records a skipped check, "api-surface: no claims provided (pass --claims or --session to enable this check)". See the API surface rules.