PANTHER formal verification plugins: Ivy language intelligence and NCT/NACT/NSCT protocol testing methodology
npx claudepluginhub elniak/panther-ivy-pluginIvy language server for code intelligence, diagnostics, and navigation in .ivy formal specification files
NCT/NACT/NSCT methodology guidance for Ivy protocol testing via ivy-tools MCP server. Provides agents, skills, and commands for formal protocol specification, attack modeling, and simulation-based testing using the 14-layer template architecture.
NCT/NACT/NSCT methodology guidance for Ivy protocol testing via native Ivy LSP and ivy-tools MCP server. Provides agents, skills, and commands for formal protocol specification, attack modeling, and simulation-based testing using the 14-layer template architecture.
Version: 0.4.0 | License: MIT | Author: ElNiak
This is a Claude Code plugin for the PANTHER-Ivy tester. It provides methodology guidance, domain knowledge, and interactive tooling for formal protocol testing using Microsoft's IVy language.
What it does:
What it does NOT do:
| Methodology | Full Name | Purpose |
|---|---|---|
| NCT | Network-Centric Compositional Testing | Formal spec plays one protocol role against an Implementation Under Test (IUT) to verify RFC compliance |
| NACT | Network-Attack Compositional Testing | Extends NCT with the APT 6-stage lifecycle to model and test protocols from an attacker's perspective |
| NSCT | Network-Simulator Centric Compositional Testing | Runs the same Ivy specs inside Shadow Network Simulator for deterministic, large-scale, topology-controlled testing |
panther/plugins/services/testers/panther_ivy/).lsp.json) -- go-to-definition, find-references, hover, document symbols for .ivy files (diagnostics via MCP ivy_lint/ivy_diagnostics).mcp.json):
Claude Code auto-discovers plugins via the .claude-plugin/ directory. No pip install is needed for the plugin itself.
panther/plugins/services/testers/panther_ivy/submodules/panther-ivy-plugin/.mcp.json file configures the ivy-tools MCP server and the .lsp.json file configures the native Ivy LSP| Component | Count | Description | Details |
|---|---|---|---|
| Agents | 4 | Methodology guide, model reviewer, spec analyst, traceability agent | agents/ |
| Commands | 5 | Slash commands for verification, compilation, and scaffolding | commands/ |
| Skills | 6 | Domain knowledge for Ivy language, methodologies, and tooling | skills/ |
| Hooks | 3 | PreToolUse (warn CLI), PostToolUse (lint .ivy), SessionStart (workspace detection) | -- |
The plugin relies on one MCP server plus native LSP support:
| Component | Role | Capabilities | Source |
|---|---|---|---|
| Native Ivy LSP | Language intelligence for .ivy files | Diagnostics, go-to-definition, find-references, hover | ivy-lsp (configured via .lsp.json) |
| ivy-tools MCP | Verification, analysis, and visualization | ivy_verify, ivy_compile, ivy_model_info, ivy_lint, ivy_coverage, ivy_query, ivy_visualize, ivy_quality, ivy_patterns | ivy-lsp (configured via .mcp.json) |
| Claude's native tools | Code navigation and editing | Read, Edit, Write, Grep, Glob, Bash | Built into Claude Code |
A PreToolUse hook (hooks/scripts/block-direct-ivy.sh) intercepts Bash tool calls and warns about direct invocations of ivy_check, ivyc, ivy_show, and ivy_to_cpp, suggesting the corresponding MCP tool. This encourages all Ivy operations to go through the MCP server for consistent behavior and structured output.
A PostToolUse hook (hooks/scripts/post-write-ivy-lint.sh) runs fast structural checks on .ivy files after Write/Edit operations, providing immediate feedback on missing #lang headers or unbalanced braces.
A SessionStart hook (hooks/scripts/detect-ivy-workspace.sh) detects the Ivy workspace root and injects context for Claude, including the path to protocol models and MCP server scope.
Claude Code marketplace entries for the plugin-safe Antigravity Awesome Skills library and its compatible editorial bundles.
Production-ready workflow orchestration with 84 marketplace plugins, 192 local specialized agents, and 156 local skills - optimized for granular installation and minimal token usage
Directory of popular Claude Code extensions including development tools, productivity plugins, and MCP integrations