nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 this does NOT catch"…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 specs", "re-verify"…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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".
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 of /lean-impl…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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, and only…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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, compares outputs, and…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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", "compile dafny".
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
Generate a Dafny implementation body that satisfies a verified spec. Iteratively adds proof hints, loop invariants, and lemmas until the verifier accepts. Use after /spec-iterate produces an approved spec. Triggers: "implement the spec", "generate verified code", "prove the implementation".
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 oracle); pairs with…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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, emits a content-addressed JSON attestation, and enforces a 30% FP kill criterion.…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
Generate a bidirectional invariant-to-test coverage gate for a repo that uses docs/invariants/.md plus // Invariant : 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, TypeScript; Rust/Ruby/Java are…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 location. Triggers…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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; downstream of…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 loop against leancheck…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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. Triggers: "lightweight…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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", "root cause"…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 — the implementer agent…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 this code adequate"…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 this safe?".…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
Adversarially probe a module's invariant documentation for missing properties. Given docs/invariants/ .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 block for human review. Layer 6…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 spec"…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 verification targets"…
nicholls-inc/claude-code-marketplace
Skill Claude CodeCodex
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 flow".
nicholls-inc/claude-code-marketplace
Plugin Claude Code
Generate structured performance reports on plugins, skills, and agents by analysing Claude Code session conversations.