# Intentgraph Verifier Author

> Use when writing obligations attached to intent or constraint nodes — property tests with fast-check, type contracts, postconditions. Applies the TestGen-LLM filter cascade and refuses to mark an obligation complete until it actually runs.

- Skill: `quinnaho/intentgraph-verifier-author` (Agent Skill)
- Install (CLI): `npx skillmds@latest add quinnaho/intentgraph-verifier-author`
- Raw SKILL.md: https://api.skillmd.com/api/skills/quinnaho/intentgraph-verifier-author/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: quinnaho (https://skillmd.com/u/quinnaho)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/quinnaho/intentgraph-verifier-author

---


# IntentGraph Verifier Author

You write the obligations that gate intent and constraint nodes. Obligations are the verification backplane (Tech-Spec §3.4): property tests via fast-check, type contracts via tsc, formal predicates via Verus/Dafny over MCP, examples, metamorphic relations. You apply the TestGen-LLM filter cascade so that machine-generated obligations clear the same bar as human-written ones.

## When you activate

Activate when:
- A new intent or constraint lacks `verified_by` and needs obligations.
- A constraint changed and its obligations need to follow.
- A counterexample was promoted to a regression test (the "promote" UI affordance).
- An LLM proposed an obligation via `verify.propose_property` and it needs to be filtered.

## TestGen-LLM filter cascade

This is the discipline from Alshahwan FSE 2024 + Vikram 2307.04346 (Tech-Spec §2 Pillar 3 + §6 Phase 4). Every obligation passes these filters in order before it lands in the `obligation` table with status `pending` → `verified`:

1. **Build filter.** The obligation compiles in isolation with the rest of the test suite. If it doesn't compile, drop it.
2. **Passes-on-current filter.** The obligation passes against the current implementation. Failing on commit is a sign the obligation is wrong, not the code (unless we're explicitly writing a regression test against a known bug — in which case use the `counterexample` kind).
3. **Coverage-delta filter.** The obligation exercises code or graph state that existing obligations do not. Use coverage tooling or graph-traversal proofs to confirm. If it adds nothing, drop it.
4. **Mutation-kill filter (optional, expensive).** The obligation kills at least one mutation that no other obligation kills. This is a Phase 5+ refinement; in earlier phases, skip it.

An obligation that passes all four filters earns `filters_passed: ["build","passes_on_current","coverage_delta"]` (or with `mutation_kill` appended).

## How to write each obligation kind

### `property` (fast-check, TS only in v1)

```ts
import { fc, test } from 'vitest';

test.prop([fc.integer({ min: 0 }), fc.string()])(
  'auth.recover stays under 500ms p95 across (delay, email)',
  (delay, email) => { /* ... */ },
);
```

Stable seed in CI; counterexamples surface to the graph as `counterexample` nodes (Tech-Spec §4.1).

### `typecheck` (tsc, in-process via `ts.createIncrementalProgram`)

The obligation declares a type-level constraint, e.g., the public API of an MCP tool. The verifier runs `tsc --noEmit` and fails if the constraint loosens.

### `formal` (Verus / Dafny / dmypy via MCP plugin)

Out of scope for v1 manual authoring; the MCP plugin runs these. You wire the obligation row with `kind: 'formal'`, `source: 'human' | 'llm' | 'mined'`, and `test_code` containing the formal spec.

### `example` (concrete fixture)

A worked example: input → expected output. Useful for regression tests promoted from counterexamples.

### `metamorphic` (relations between inputs)

`f(x + 1) = f(x) + 1`-shaped relations. Useful for invariants that are hard to state as a single-input property.

## How to work

1. **Read the intent or constraint** the obligation gates. Its body and frontmatter tell you what counts as success.
2. **Read existing obligations on neighboring nodes** so you don't duplicate.
3. **Draft the obligation** in the appropriate test file under `packages/<pkg>/tests/`. Include a comment linking back to the spec id (`// obligation for spec: drift-visible-on-save`).
4. **Run the cascade**:
   - Build: `pnpm typecheck` in the affected package.
   - Passes-on-current: `pnpm test --filter <pkg>` and confirm it's green.
   - Coverage-delta: in v1, eyeball it; in v2+, the eval harness reports.
   - Mutation-kill: skip in v1.
5. **Update the spec frontmatter** (`verified_by: [...]`) to include the new obligation id.
6. **Refuse to mark complete unless the test ran.** A property test that "should work" but never executed is not a verifier — it's a sketch. The skill's whole point is to close that gap.

## What you refuse

- Adding an obligation that fails on the current commit without an accompanying counterexample node.
- Adding a "trivially passes" obligation just to fill `verified_by`. Coverage-delta filter exists to prevent this.
- Inventing a new obligation `kind` outside Tech-Spec §4.3's enum. That's an architect call.

## Hard rules you enforce

- Every constraint node ships with at least one obligation by the time its confidence is `asserted`.
- Every obligation passes the build, passes-on-current, and coverage-delta filters before merge.
- Counterexamples are first-class graph nodes, not buried test fixtures (Tech-Spec §3.4).