verifying-claims · diff
v0.1.0 to v0.2.0
72 added, 130 removed. Audit A to A.
---
name: verifying-claims
- description: Verify typed claims embedded in markdown/docs against live state, and run the literate-TDD loop (write spec with claims → red/green → gate in CI). Use this whenever the user wants to check that a README, spec, ops note, or design doc still matches the code it describes; whenever they mention claim verification, documentation drift, spec drift, executable documentation, literate testing, doc-code sync, or "docs that fail when they're wrong"; whenever turning a spec into a test that fails on drift; or when wiring doc-verification into TDD, CI, pre-commit, or a publish gate. Covers the `signature` and `command-output` claim types, the invariant-vs-mutable-state rule (never verify state that is expected to change), and the GitHub Action + pytest forcing functions that make the check unskippable.
+ description: Check that a document's claims about code are actually true by reading the prose, the code, and the tests and reporting (or fixing) where they disagree. Use whenever the user wants to verify a README, guide, spec, or docstring still matches the code; whenever they mention documentation drift, doc-code sync, "is this still accurate", stale docs, or keeping docs/tests/code consistent; before publishing or merging a docs change; or as a periodic doc-accuracy sweep. The agent reads the prose's meaning directly — there is no claim-comment DSL to maintain. Pairs with TDD: the test suite is the deterministic behavioral gate, this skill is the semantic prose-vs-reality review.
metadata:
- version: 0.1.0
+ version: 0.2.0
---
# verifying-claims
- A claim verifier for documentation. Prose makes typed claims as HTML comments;
- `verify_claims.py` resolves each against live state and reports PASS / FAIL / STALE /
- ERROR. The point: documentation that **breaks loudly when it drifts**, instead
- of going silently stale.
-
- Named after [Verso](https://github.com/leanprover/verso), Lean's literate
- framework, where the documentation and the formal proof share one elaboration
- context so they cannot drift. This is the lightweight, language-agnostic
- cousin: claims live next to prose and are checked against the live system.
-
- ## Claim syntax
-
- A claim is an HTML comment sitting next to the prose it backs:
-
- ```
- parse_claims takes a `text` argument.
- <!-- claim: signature target=mymod.parse_claims has-params=text -->
- ```
-
- The prose stays human-readable; the claim is invisible in rendered markdown.
-
- ## Claim types
-
- Both encode **invariants** — things that should stay true. A FAIL means a real
- defect to fix, not the passage of time.
-
- ### `signature`
- Does a Python callable accept the listed named parameters? An interface
- contract — like a checked header file.
- ```
- <!-- claim: signature target=pkg.module.func has-params=a,b,c -->
- ```
- Imports are restricted to an allowlist of module prefixes for safety
- (`VERIFY_CLAIMS_IMPORT_ALLOW`, default `muninn_utils,scripts,verify_claims`).
-
- ### `command-output`
- Run a command (subprocess, no shell, no eval) and assert its exit code and/or
- output substrings. This is the behavioral / acceptance claim, and the bridge
- to a real test suite — point it at a named test:
- ```
- <!-- claim: command-output cmd='pytest tests/test_parse.py::test_quoted' exit=0 -->
- <!-- claim: command-output cmd='mytool --help' exit=0 stdout-contains=usage -->
- ```
- Args: `cmd` (required), `exit`, `stdout-contains`, `stderr-contains`, `timeout`.
-
- ## The one rule that matters: verify invariants, not mutable state
-
- Only encode claims about things that **should stay true**. Do NOT verify state
- that is *expected* to change — a PR's open/merged status, an issue's state, a
- "current version" number. A PR going open→merged is the PR doing its job, not
- drift.
-
- The diagnostic: **which artifact do you edit to make a failing check pass?**
- - Signature mismatch → you fix the code. Correct: there's a defect.
- - "PR #687 is open" gone red → you can only edit the *claim* to say "merged,"
- chasing reality instead of constraining it.
-
- When the document is the thing that must change, the check is just confirming a
- stale cache. Mutable state wants **transclusion** (render the current value at
- read time), not a frozen assertion + diff — a different mechanism, out of scope
- here. (Earlier versions had `pr-state`/`issue-state`; they were removed for
- exactly this reason.)
+ Check that what a document *says* about code is true, by reading the document,
+ the code, and the tests together and reporting where they disagree.
- ## Verdicts, and how they map to TDD states
+ ## What changed (v0.1 → v0.2)
- - **PASS** — claim matches reality → green
- - **FAIL** — the referenced thing exists but the assertion fails → classic red
- - **STALE** — the referenced thing doesn't exist yet (function/test missing) →
- you're ahead of the code; pre-red
- - **ERROR** — the resolver couldn't run (bad syntax, blocked import, timeout)
+ v0.1 was a comment-DSL: you hand-wrote `<!-- claim: ... -->` next to prose and
+ a script checked the *comment* against the code. That had a fatal gap — the
+ comment and the prose were two artifacts stapled together, and only the comment
+ was checked, while humans read the prose. The prose could lie with a green run.
- Exit 0 if all PASS, 1 otherwise. `--json` for machine output.
+ v0.2 drops the DSL. The reviewer is the agent: it reads the prose's *meaning*
+ directly and compares it to what the code does and what the tests assert. No
+ shadow copy, because the thing being checked is the thing the human reads.
+ (Existing tools already own the alternatives — Gherkin binds executable
+ scenarios, Lean's Verso transcludes facts into prose, TDD couples code to
+ tests. This fills the remaining slot: free-prose documentation, judged.)
- ## Literate TDD: the spec doc IS the test suite
+ ## Division of labor — read this first
- verifying-claims is the **outer** loop around a normal TDD inner loop. The inner loop
- stays pure pytest (red→green→refactor, fast, behavioral). verifying-claims binds the prose
- spec to those tests and to the code's interface, so the doc cannot claim a
- behavior whose test was deleted.
+ This skill does NOT gate merges and is NOT a test framework.
- The loop, test-first:
- 1. Write the spec doc describing what you want, with claims pointing at
- not-yet-written tests and signatures.
- 2. Run `verifying-claims spec.md` → all STALE/FAIL → **red**.
- 3. Write the test, then the implementation.
- 4. `verifying-claims spec.md` all PASS → **green**.
- 5. Refactor with verifying-claims as the regression net.
+ - **The test suite (TDD/CI)** owns the behavioral contract: deterministic,
+ cheap, auditable, gated. A green check is something you can hold CI to.
+ - **This skill** owns the prose layer: does the documentation match reality?
+ That needs semantic judgment across artifacts, which is non-deterministic and
+ fallible — so it runs as a *triggered review* (before docs ship, on request,
+ as a sweep), not as a per-commit gate. "The agent said the docs match" is not
+ a guarantee you gate a merge on; it's a review you act on.
- `signature` claims give the contract-first variant: write the API in the doc,
- run verifying-claims (STALE), stub the function (PASS) — you've locked the interface in
- prose before writing behavior.
+ Tests are the anchor. The docs are correct when they agree with what the tests
+ assert about the code. So write/keep good tests first; this skill keeps the
+ prose pinned to them.
- Honest limit: verifying-claims does not assert `f(x) == y` itself (the unsafe `eval`
- claim type was removed). Behavioral truth lives in pytest; `command-output`
- claims check that the named test *passed*. verifying-claims is a binding/acceptance layer,
- not a replacement for your assertions.
+ ## Procedure
- ## What forces a run (the part that actually matters)
+ 1. **Identify** the document(s) to check and the code + tests they describe.
+ 2. **Gather** consistent input: run `scripts/gather_context.py --doc DOC --src
+ SRC --tests TESTS`. It ast-parses source (no imports, no execution) and
+ bundles the document text, the public API surface, and the test inventory.
+ 3. **Extract the claims** the prose makes — every checkable assertion about the
+ code (signatures, behavior, return shapes, defaults, guarantees, examples).
+ Do this by reading; there are no claim markers.
+ 4. **Judge each claim** against the API surface and the tests:
+ - Does the code actually do what the prose says?
+ - Is the claim backed by a test, or merely asserted?
+ - Does it reference something that no longer exists?
+ 5. **Report** drift, ranked by severity, each finding citing the prose claim and
+ the contradicting reality (file/function). Use the verdicts below.
+ 6. **Optionally fix**: rewrite the prose to match reality, and/or flag claims
+ that need a test (an UNSUPPORTED claim is a missing test, not just a doc bug).
- A verifier only helps if it runs — otherwise the drift moves from "doc vs code"
- to "the verify-run vs reality." Unlike real Verso, where the check *is*
- compilation, markdown renders fine whether or not its claims pass. So nothing
- intrinsic forces a run. Bind verifying-claims to an event with its own enforcement, ranked
- by how hard it is to skip:
+ ## Verdicts
- 1. **Required CI check on PRs** — strongest. Branch protection makes the verifying-claims
- job a required status; you cannot merge red. Structural, not disciplinary.
- Template: `assets/verify-claims.yml`.
- 2. **Claims as part of the pytest suite** — `test_verify_claims` runs verifying-claims and
- asserts exit 0, so verifying-claims runs whenever tests run and inherits the green-bar
- gate. Best fit when verifying-claims wraps a TDD loop. Template:
- `assets/test_verify_claims.py`.
- 3. **Publish-time gate** — the publish flow runs verifying-claims and refuses to ship a
- doc with failing claims. Binds verify to the irreversible action.
- 4. **Pre-commit hook / `--watch` / boot-surfacing** — raise the probability,
- don't force. Bypassable, local, or merely informational.
+ - **PASS** — the prose claim matches the code and is exercised by a test.
+ - **FAIL** — the code contradicts the claim (the doc is wrong, or the code
+ regressed and the doc caught it).
+ - **UNSUPPORTED** — the claim matches the current code but no test backs it, so
+ nothing protects it from future drift. Surface as a missing test.
+ - **STALE** — the claim refers to something removed or renamed.
- General rule: only gating the **irreversible action** (merge, publish, deploy)
- on a **required** check actually forces a run, because it removes the choice.
+ ## Invoking
- ## Running it
+ - "Check the README against the code before I publish it."
+ - "Does `docs/api.md` still match `pkg/`?"
+ - "Sweep the docs for drift after this refactor."
- ```
- python3 scripts/verify_claims.py spec.md # verify once; exit 0/1
- python3 scripts/verify_claims.py --json spec.md # machine-readable output
- python3 scripts/verify_claims.py --watch spec.md # re-verify on save (inner-loop aid)
- ```
+ Run it at moments that matter — pre-publish, post-refactor, on a docs PR — not
+ on every commit. The deterministic gate is the test suite; this is the layer
+ tests can't reach.
- `--watch` re-runs in a fresh subprocess on every save, so `signature` claims
- pick up edited code. It forces nothing — it's category 4 above.
+ ## Honest limits
- ## Setting up the gate in a repo (the integration)
+ - Non-deterministic and fallible: a review can miss drift or misjudge. Treat
+ output as a careful review, not a proof.
+ - Cost/latency: reading three artifacts and reasoning is expensive next to a
+ test run. Don't wire it where a cheap deterministic check belongs.
+ - It checks prose against code+tests; it does not verify the tests themselves
+ are correct. Garbage tests → confident-but-wrong PASS. TDD discipline upstream
+ still matters.
- 1. Copy `assets/test_verify_claims.py` into the repo's `tests/`, and point the
- `SPECS` list at the docs you want gated. Keep gated specs **all-green** —
- don't put teaching/demo claims that intentionally FAIL into a gated file.
- 2. Copy `assets/verify-claims.yml` into `.github/workflows/`. It runs verifying-claims on
- the gated specs and the pytest suite on every PR.
- 3. In repo settings → branches, add the workflow's job as a **required status
- check**. Now drift cannot merge.
+ ## When NOT to use
- See `references/example-spec.md` for a working all-green spec.
+ - As a CI merge gate (use the test suite).
+ - To verify behavior (write a test).
+ - On prose with no factual claims about code (nothing to check).
## Files
- - `scripts/verify_claims.py` — the verifier (signature + command-output, --watch).
- - `assets/verify-claims.yml` — GitHub Action template (forcing function #1).
- - `assets/test_verify_claims.py` — pytest template (forcing function #2).
- - `references/example-spec.md` — an all-green spec suitable for gating.
+ - `scripts/gather_context.py` — deterministic input bundler (doc + API surface +
+ test inventory), ast-only, no imports.
+ - `references/drift-report-example.md` — what a review report looks like.