/polynv

name: polynv
description: Elicit the invariants for a state machine — the plugin takes the lead. Harvest candidate invariants from the contract's own vocabulary (terminal states, typed fields, reject rules, effect kinds), contribute the frontier model's domain knowledge as candidates, pre-check every candidate against the machine so each question arrives with a HOLDS verdict or a concrete counterexample story, then drive a plugin-led interview that converges an append-only intent ledger into a confirmed invariants.mjs. Use when the user asks "what invariants should this machine have", "help me write invariants", "is my invariant set any good", or when polygen/polygraph need an invariants.mjs that does not exist yet. Elicitation is an ongoing, multi-person activity — sessions resume from intent-ledger.json and never re-ask settled questions.

polynv — elicit the invariants (the plugin leads)

Every Polygraph gate is exactly as good as `invariants.mjs`, and writing good invariants from a blank page is a scarce skill. This skill routes around it: **you (the in-session assistant) drive the interview**; the designer's job is reduced to judging concrete stories — confirm / reject / modify / defer — which is a common skill. Never wait for the designer to propose invariants unprompted; propose, ask, and record.

> **Disclosure (same as the whole plugin).** This is experimental, unproven > technology. A pre-check verdict is a consistency check over the declared > finite (action, data) domains, not a proof. Harvested candidates describe > BEHAVIOR, not intent — a machine with a bug yields candidates that bless > the bug — which is why nothing enters `invariants.mjs` without the > designer's explicit disposition, and why you must never answer an intent > question on the designer's behalf. A CONVERGED verdict means every question > was answered AND the mutation adequacy grade ran — it still does not prove > the questions were sufficient: the grade bounds unconstrained behavior, it > does not certify intent, and behavior-removing mutations largely evade it.

The CLI is `${CLAUDE_PLUGIN_ROOT}/polynv/bin/polynv.mjs`; an artifact dir holds `contract.json` + the SAM v2 module + optional `effects.manifest.json` (what polygen emits). The system of record is `intent-ledger.json` in that dir — append-only, in git, holding every record ever considered including rejected and abandoned ones. Deterministic, no API key.

Step 1 — Harvest (mechanical)

node ${CLAUDE_PLUGIN_ROOT}/polynv/bin/polynv.mjs harvest --artifacts <dir> \
  [--traces <dir-or-file.ndjson>] [--snapshots <corpus>] [--min-obs N]

Generates template candidates from the contract's own vocabulary (one absorbing question per terminal state, range/sign/set-once/monotone per typed field, one no-op question per reject-describing special rule, one at-most-once question per manifest effect kind) and pre-checks each against the machine — emission candidates through the machine ∘ mapper composition (polyrun check-effects) whenever the dir carries `effects.cjs` + manifest. **Resuming after the machine changed?** Run `drift --artifacts <dir>` first: it re-checks every recorded answer and names the verdicts that moved; `--reopen --author <designer>` re-asks judged answers whose ground truth drifted, while a confirmed rule now violated stays confirmed as a finding. **Always offer to mine**: if traces, a polyrun journal export, or fleet snapshots exist, pass them — the miners add observed-behavior candidates (in-domain, ranges, orderings, control-key implications, temporal precedence) with observation counts as evidence; mined candidates are *behavior*, so their question is always "rule, or artifact of the corpus?". Below-threshold observations become notes, not questions. Read the output notes: a special rule that mentions rejection but was not mechanically templatable is YOUR question to ask by hand; pruned and vacuous candidates are listed with reasons. Re-running harvest is always safe — settled records are never re-proposed.

Step 2 — Contribute domain priors (your obligation, before the first question)

Identify the domain from the contract vocabulary and any feature prose (payments, auth/session, inventory, approval flow, …). Enumerate the invariants canonical to that domain from your own knowledge — the designer of a payment system gets asked about authorization-before-capture whether or not any harvester surfaced it. Add each as a candidate with provenance:

node ${CLAUDE_PLUGIN_ROOT}/polynv/bin/polynv.mjs add --artifacts <dir> \
  --id "prior:<slug>" --target state|transition \
  --question "<the domain norm, as a question about THIS machine>" \
  --js "<the predicate>" --author <your-name> --source domain-prior \
  --domain <domain> --norm "<the norm as you state it>" --model <your model id>

The pre-check runs immediately: a prior that FAILS arrives at the interview with its counterexample attached. A prior the designer rejects is documentation gold — record their reason as `--concern`.

Step 3 — The interview (you lead, one question at a time)

node ${CLAUDE_PLUGIN_ROOT}/polynv/bin/polynv.mjs questions --artifacts <dir> --next --json

Present exactly one question, concrete-story-first. The ranking is information-greedy: counterexample questions come first — show the shortest path verbatim and ask *"the machine can do this today; is this acceptable?"* Acceptable → record `reject` (the behavior is intended; note why). Not acceptable → record `confirm` — the rule becomes intent AND the counterexample is the repro of a live finding; say so plainly. For HOLDS questions ask *"rule, or coincidence of the current code?"* For emission questions (pre-check NOT-RUN at M0) still ask; a confirmed one is recorded for check-effects wiring.

Record every answer with attribution:

node ${CLAUDE_PLUGIN_ROOT}/polynv/bin/polynv.mjs record --artifacts <dir> \
  --id <recordId> --disposition confirm|reject|abandon|defer|mod