crosscheck

Plugin crosscheck from marketplace nicholls in nicholls-inc/claude-code-marketplace. Commands read from the repo's manifest — yesterday.

Skills (30)

• acceptance-oracle-draft

  Scope the top-N user-observable flows for a repo and emit mechanically-verifiable acceptance-scenario skeletons (YAML/JSON) plus a runner-script stub. Does NOT run the scenarios — that's CI's job. Enforces a strict mechanical-verification-only rule: subjective criteria ("UX feels good") must be quan

• assurance-init

  Interactive bootstrap that scaffolds the governance skeletons a repo needs to adopt the 6-layer assurance hierarchy. Creates docs/assurance/ROADMAP.md + horizon directories, .claude/rules/protected-surfaces.md (two-class partition), and skeleton docs/invariants/ docs for 1-3 user-chosen modules. Ask

• assurance-layer-audit

  Entry-point diagnostic for the 6-layer assurance hierarchy. Inspects a repo, detects language and tooling, and emits a per-layer projection table (current reach + ecosystem limits) plus a prioritised gap list. Run this FIRST, before /assurance-init, to scope realistic reach for your codebase. Trigge

• assurance-probe

  Measure test strength via mutation/vacuity/generator probes (rotation-based). Layer 4 deterministic-strength check: parses the Failure condition clause of each invariant, generates targeted source mutations, and runs covering property-based tests against them, then adds vacuity (branch-coverage delt

• assurance-roadmap-check

  Parse each roadmap item under docs/assurance/**/*.md, read its Status field, and diff the declared state against observed repo/PR state. Flags drift in both directions — docs that say Done but lack a merged PR or expected artifact, docs that say Not started but whose code already exists, stale In pr

• assurance-status

  Onboarding-gated status dashboard for a repo that has adopted the 6-layer assurance hierarchy. Phase 1 runs a deterministic onboarding check (no LLM); Phase 2 emits a status dashboard covering ROADMAP Status drift, invariant coverage gaps, protected-surface edits lacking governance notes, intent-che

• audit-invariant-consistency

  Layer 5 + 6 hybrid consistency audit. Given a glob of invariant docs and an optional spec, runs three passes (within-module contradictions, cross-module contradictions, invariant-vs-spec contradictions) and emits a capped, prioritised findings file with 4-path triage blocks (`Accept (amend spec)` is

• audit-spec-coverage

  Layer 6 spec-coverage probe. Given a prose spec and a glob of invariant docs, emits two coverage matrices (spec section → invariant IDs; audit-finding ID → invariant IDs) plus a prioritised gap list and 4-path triage blocks. Mirrors /spec-adversary's discipline (capped output, kill criteria, "what t

• check-regressions

  Scan the spec registry for verified Dafny specs whose associated source files have changed. Re-verify affected specs and report which properties still hold. Use for regression detection after code changes, pre-commit checks, or spec maintenance. Triggers: "check regressions", "did my changes break s

• compare-patches

  Determine whether two code patches are semantically equivalent by tracing execution through the test suite using semi-formal reasoning. Produces a structured proof of equivalence or a specific counterexample. Triggers: "compare patches", "are these equivalent", "same behavior", "diff comparison".

• correspondence-review

  Review each Lean definition produced by `/lean-impl` against the actual source code and classify correspondence as exact, abstraction, approximation, or mismatch — with file:line citations. Documents divergences and assesses impact on any proved theorems. Step 4 of the Lean-side pipeline; downstream

• draft-invariants

  Contract-first methodology for drafting module-level invariants and property tests. Reads the project's prose spec first when one exists; falls back to user elicitation only when no spec is found. Anchors each invariant in real past failures (incidents, audit-findings), gap-analyses against the code

• drt-oracle

  Differential random testing between a Lean 4 model (the oracle) and a production implementation (the system under test), scoped by the classification document produced by `/correspondence-review`. Step 5 of the Lean-side pipeline; final step. Generates random inputs, executes both implementations, c

• extract-code

  Compile verified Dafny to Python or Go with Dafny runtime boilerplate stripped. Presents clean output ready for project integration, with type mappings and property-based test suggestions. Use after /generate-verified produces a verified implementation. Triggers: "extract to python", "extract to go"

• generate-verified

  Generate a Dafny implementation body that satisfies a verified spec. Iteratively adds proof hints, loop invariants, and lemmas until the verifier accepts. With `evidence: <path.dfy>`, commits the verified program there and emits an evidence record with dafny_evidence. Use after /spec-iterate produce

• informal-spec

  Extract a precise prose specification for a module before any Lean code is written — preconditions, postconditions, invariants, edge cases, concrete examples, and ambiguities flagged for the user. Step 1 of the Lean pipeline (informal spec → Lean spec stub → Lean impl → correspondence review → DRT o

• intent-check

  Portable round-trip informalization over (invariant prose, covering test, code diff) — Layer 5 of the assurance hierarchy. Runs a two-LLM pipeline (blind back-translator then diff-checker), appends outcomes to a false-positive tracker, writes an advisory JSON record of the run, and enforces a 30% FP

• invariant-coverage-scaffold

  Generate a bidirectional invariant-to-test coverage gate for a repo that uses docs/invariants/*.md plus `// Invariant <ID>: <Name>` test comments. Emits both a pre-commit hook and a CI job (dual-track enforcement), adapted to the target repo's language and test framework. v1 supports Go, Python, Typ

• journal-context

  Deterministic walk of the directory tree from a starting path up to the enclosing git repository root, dumping every JOURNAL.md it encounters in walk order (deepest first, root last). No LLM in the walk. Use before non-trivial design work in any directory to load the narrative record above that loca

• lean-impl

  Translate the source implementation into a Lean 4 functional definition that the propositions from `/lean-spec` can be connected to. For imperative or effectful production code, build a pure functional model and explicitly document what the model abstracts away. Step 3 of the Lean-side pipeline; dow

• lean-spec

  Translate a signed-off informal specification into a Lean 4 specification stub: type definitions mirroring the source, function signatures, key theorem declarations with `sorry` proof bodies, and the Mathlib imports needed to make the file `lake build` cleanly. Drives the Lean toolchain in a retry l

• lightweight-verify

  Generate lightweight verification artifacts for functions where full formal verification is overkill: design-by-contract assertions, property-based tests, and documented runtime invariant checks. Use for simple transformations, CRUD, concurrency, or floating-point code that Dafny cannot verify. Trig

• locate-fault

  Locate the root cause of a failing test using 4-phase semi-formal reasoning: test semantics analysis, code path tracing, divergence analysis, and ranked predictions. Traces from failure to root cause rather than fixating on crash sites. Triggers: "locate fault", "find the bug", "why does this fail",

• protected-surface-amend

  Given a planned change to a protected-surface file, generate the governance-note amendment block that must accompany the edit: change description, rationale, class (A/B), governing roadmap item, authority, explicit diff plan, test/coverage impact, and review checklist. Primarily agent-invocable — th

• rationale

  Build a hierarchical claim tree arguing that code adequately satisfies its requirements. Each leaf claim is classified by verification method (formal, behavioral, static, semantic) and verified where possible. Bridges formal verification and semi-formal reasoning. Triggers: "build rationale", "is th

• reason

  General-purpose semi-formal code reasoning that structures analysis into an evidence-driven certificate. Forces premise gathering, execution tracing, and alternative hypothesis checking before conclusions. Use for any code question: "Is this correct?", "Will this break?", "What does this do?", "Is t

• spec-adversary

  Adversarially probe a module's invariant documentation for missing properties. Given `docs/invariants/<module>.md` plus the module's code, proposes up to 3 candidate invariants the spec is failing to document, each annotated with evidence, category, confidence, and an accept/reject/defer triage bloc

• spec-iterate

  Draft and verify a Dafny formal specification from a natural language description. Produces a verified spec with preconditions, postconditions, and invariants. Use when the user wants to formally specify a function, algorithm, or correctness property. Triggers: "specify", "formal spec", "write a spe

• suggest-specs

  Analyze code to propose candidate formal specifications. Identifies functions that would benefit from verification and generates natural-language preconditions, postconditions, and invariants. Lowers the barrier to entry for /spec-iterate. Triggers: "suggest specs", "what should I verify", "find ver

• trace-execution

  Hypothesis-driven execution path tracing that builds complete call graphs from entry point to leaf functions. Documents observations with line numbers and updates hypotheses as evidence is gathered. Triggers: "trace execution", "what happens when", "follow the code path", "call graph", "trace the fl

Subagents (5)

• add-orchestrator

  ADD (Assurance-Driven Development) methodology workflow runner. Drives the spec-driven fast path: signed-off spec → bulk-drafted invariants → batched audit → user-triaged findings → approved invariant docs ready for implementation. Dispatches parallel subagents per module. Hands off to byfuglien for

• auditor

  ADD Phase 5 auditor — the read-only consolidation agent. Runs scheduled or on-demand passes over the ADD artifact stack and renders one verdict per artifact: settled / active / drifted. Grounds every verdict in deterministic signals (coverage matrices, session-marker hashes, JOURNAL diff-type lines,

• byfuglien

  Orchestrator for formal verification and semi-formal code reasoning. Classifies tasks, routes to appropriate verification or reasoning skills, and validates output quality. Use for any formal verification, structured code reasoning, fault localization, patch comparison, or specification management t

• hellebuyck

  Orchestrator for specification-chain assurance (Layers 4–6) and governance scaffolding. Classifies tasks, routes to /assurance-*, /intent-check, /spec-adversary, /acceptance-oracle-draft, /protected-surface-amend, and validates output quality. Named after Connor Hellebuyck — the goalie, last line of

• lowry

  Phase 4 gated-implementation agent — the run-to-green loop. Drives a red build to green against a ratified invariant contract within three legal commit shapes (implementation / governance-amendment / new-invariant), and refuses to reach green by weakening an invariant: when the only path forward wea

MCP servers (1)

• dafny

  runs: node ${CLAUDE_PLUGIN_ROOT}/mcp-server/dist/index.js