Stats
Actions
Tags
From panther-ivy-plugin
Use when adding requirements to an Ivy specification one at a time with verification between each addition. Guides the add-verify-iterate loop for incremental formal specification development.
How this skill is triggered — by the user, by Claude, or both
Slash command
/panther-ivy-plugin:incremental-spec-devThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
This skill guides the iterative loop for adding RFC requirements to an Ivy formal specification one at a time. Each iteration adds exactly one requirement, verifies the model, and tracks coverage progress before moving to the next.
This skill guides the iterative loop for adding RFC requirements to an Ivy formal specification one at a time. Each iteration adds exactly one requirement, verifies the model, and tracks coverage progress before moving to the next.
Each requirement follows this 9-step cycle. Never skip steps or batch multiple requirements.
Use ivy_coverage(mode="gaps") to find uncovered MUST requirements first, then SHOULD:
ivy_coverage(mode="gaps", protocol="{prot}")
This returns unguarded_state_vars, uncovered_requirements, and orphaned_monitors. Focus on uncovered_requirements entries tagged with MUST level.
Use ivy_patterns(mode="analyze") to determine which pattern applies to the requirement:
ivy_patterns(mode="analyze", protocol="{prot}")
Common patterns and when they apply:
| Requirement Type | Pattern | Placement |
|---|---|---|
| Precondition on sending | Monitor (before) | {prot}_{role}_behavior.ivy |
| Postcondition after receiving | Monitor (after) | {prot}_{role}_behavior.ivy |
| State transition constraint | State machine | {prot}_connection.ivy or behavior file |
| Data format validation | Variants | {prot}_frame.ivy or {prot}_packet.ivy |
| End-state property | _finalize | Test specification file |
Add the requirement to the appropriate .ivy file:
# Before: guard precondition
before frame.stream.handle(f:frame.stream, scid:cid, dcid:cid, e:quic_packet_type) {
require f.offset + f.length <= max_stream_data(f.stream_id); # [rfc9000:4.1]
}
# After: state update + compliance check
after packet_event(src:ip.endpoint, dst:ip.endpoint, pkt:quic_packet) {
require pkt.hdr.version = negotiated_version; # [rfc9000:6.2]
}
Rules for writing the assertion:
# [rfc9000:X.Y] as a trailing comment on the require/ensure linebefore for preconditions (what must hold before an event), after for postconditions (what must hold after)require var_name(args) for safety properties that depend on protocol stateivy_lintRun structural validation (completes in milliseconds):
ivy_lint(relative_path="{path_to_modified_file}")
This catches:
#lang ivy1.7 headerFix any lint errors before proceeding. Do not skip this step.
ivy_verifyRun full formal verification:
ivy_verify(relative_path="{path_to_modified_file}")
If verification succeeds, proceed to Step 7.
When ivy_verify returns a failure:
counterexample_trace field in the output for a human-readable state trace| Failure | Likely Cause | Fix |
|---|---|---|
| Invariant not preserved | New assertion conflicts with existing state | Add a strengthening invariant or narrow the assertion scope |
| Safety property violated | Unreachable state is now reachable | Add a require guard in a before block |
| Ungrounded variable | Free variable in assertion | Bind the variable: require P = the_cid -> property(P) |
| Z3 timeout | Proof obligation too complex | Break into smaller isolates, add auxiliary lemmas |
Run coverage statistics to confirm the requirement is now covered:
ivy_coverage(mode="stats", protocol="{prot}")
Compare covered and coverage_percent with the previous iteration. The newly added requirement should appear as covered.
Run the quality gate after each addition:
ivy_quality(mode="gate", protocol="{prot}", level="minimal")
Gate levels:
If the gate fails, address the reported issues before continuing.
Commit the single requirement addition with a message referencing the RFC section:
git add {modified_files}
git commit -m "spec({prot}): add [rfcNNNN:X.Y] requirement - {brief description}"
One commit per requirement keeps the git history bisectable and each commit independently verifiable.
max_stream_data and total_data_sent.Use ivy_extract_requirements to parse remaining uncovered RFC sections:
ivy_extract_requirements(relative_path="{rfc_text_file}", output="structured")
This returns normative statements (MUST/SHOULD/MAY) with section references. Cross-reference against ivy_coverage(mode="gaps") to identify which ones still need assertions.
For a full traceability view:
ivy_coverage(mode="matrix", protocol="{prot}")
This shows the requirement-to-annotation mapping, making it clear which RFC sections have no corresponding Ivy assertions.
Every require, ensure, assume, or assert must include a bracket tag:
require conn_state = open; # [rfc9000:4.1]
require pkt.size <= max_packet_size; # [rfc9000:14.1, rfc9000:8.1]
ensure stream_data_delivered; # [rfc9000:2.2]
Use multi-tags ([rfc9000:14.1, rfc9000:8.1]) only when a single assertion genuinely covers multiple requirements.
| Placement | Purpose | Example |
|---|---|---|
before action(...) | Precondition guard -- what must hold before the event | require connected(the_cid); |
after action(...) | Postcondition check + state update -- what must hold after | require pkt.version = negotiated_version; |
around action(...) | Combined pre/post with access to both old and new state | Serialization dispatch logic |
For safety properties that depend on protocol state, use explicit guards:
before frame.stream.handle(f) {
if _generating {
require connected(the_cid); # Guard: only when connected
require f.stream_id <= max_stream_id(the_cid); # [rfc9000:4.6]
}
}
The if _generating guard ensures the constraint only applies to test traffic generation (Ivy-side), not to received traffic from the IUT.
The incremental loop ends when all three conditions are met:
ivy_coverage(mode="stats") -- the by_level.MUST.coverage_percent should be 100%.ivy_quality(mode="gate", level="standard") (or comprehensive for release-quality specifications). All checks must pass.ivy_verify cleanly with no counterexamples and no Z3 timeouts.After MUST requirements are complete, repeat the loop for SHOULD requirements if time permits. MAY requirements are lowest priority and may be deferred.
Wrong: Write five monitors, then run ivy_verify once.
Right: Write one monitor, lint, verify, track coverage, commit. Then the next.
Why: When verification fails after adding five requirements, you cannot tell which one caused the failure. The incremental approach gives immediate feedback and keeps the specification in a known-good state at every commit.
ivy_lintWrong: Go straight to ivy_verify after editing.
Right: Always run ivy_lint first.
Why: ivy_lint runs in milliseconds and catches structural errors (missing header, unresolved includes, syntax). ivy_verify takes seconds to minutes. Catching a typo in 50ms instead of 120 seconds compounds across dozens of iterations.
Wrong: Write require property(X) without checking that the state variable property is properly initialized and guarded.
Right: Check with ivy_coverage(mode="gaps") that state variables have initialization (after init blocks) and guard conditions in all relevant before blocks.
Why: Uninitialized state variables start with arbitrary values in Ivy. A require conn_seen(C) without after init { conn_seen(C) := false } will have unpredictable behavior. The gaps tool identifies unguarded state variables explicitly.
Wrong: Commit after ivy_verify passes but without checking the quality gate.
Right: Run ivy_quality(mode="gate", level="minimal") after each addition.
Why: Verification passing means the model is internally consistent, but it does not check naming conventions, missing bracket tags, or traceability. The quality gate catches these.
Wrong: Add 20 relations and functions at the start "in case we need them."
Right: Add state variables as each requirement demands them.
Why: Unused state variables inflate the verification state space, slow down Z3, and create false gaps in coverage reports. Add what you need, when you need it.
Related skills:
Related agents:
npx claudepluginhub elniak/panther-ivy-plugin --plugin panther-ivy-pluginGuides creation, editing, and verification of skills for AI coding agents using test-driven development with subagent scenarios. Use when authoring or debugging skills.