From panther-ivy-plugin
Use when ivy_verify fails with a counterexample to understand the failure, trace the violated property, and identify the fix. Guides interpretation of structured counterexample traces.
How this skill is triggered — by the user, by Claude, or both
Slash command
/panther-ivy-plugin:counterexample-guideThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
When `ivy_verify` returns a verification failure, it may include structured counterexample data that shows exactly how the property was violated. This skill provides a systematic workflow for reading counterexample traces, diagnosing the root cause, and applying the correct fix.
When ivy_verify returns a verification failure, it may include structured counterexample data that shows exactly how the property was violated. This skill provides a systematic workflow for reading counterexample traces, diagnosing the root cause, and applying the correct fix.
Use this skill when ivy_verify output contains either of these fields:
counterexample: Structured dict with assertion, assertion_line, and steps (parsed from raw ivy_check output)counterexample_trace: Human-readable formatted trace with step-by-step state changesIf the verification fails but no counterexample is present, the failure is likely a type error, unresolved symbol, or Z3 timeout -- use the workflow-reference skill instead for those cases.
Follow these steps in order when you receive a counterexample.
Look at the counterexample_trace field first. The header tells you what failed:
Violated assertion (Line 42):
require conn_seen(C)
This gives you:
require/assert/ensure livesUse Read to view the assertion in context (surrounding before/after block, action signature).
The trace shows the sequence of actions that led to the violation:
Execution trace (2 steps):
--------------------------------------------------
Step 1: quic_connection.open
conn_seen = false
cid = 0x1234
Step 2: quic_stream.send
conn_seen = false
stream_state = open (was: idle)
bytes_sent = 0
Each step shows:
(was: X) indicates a variable that changed from a previous stepWalk through the steps and look for:
conn_seen stays false across all steps, but the assertion expects it to be true after quic_connection.open(was: X), indicating a state transition happenedUse MCP tools to understand the symbol's definition and context:
ivy_query(mode="info", symbol_name="conn_seen")
This returns the symbol's type, file, line, and references -- helping you understand where it is defined and what sets it.
Use the state machine view to see the broader state transition picture:
ivy_visualize(view="state_machine")
This shows all states and transitions, helping you spot whether the counterexample trace represents a valid but unguarded path through the state machine.
Use coverage analysis to find related gaps:
ivy_coverage(mode="gaps")
Look for unguarded state variables or orphaned monitors that relate to the failing assertion. The counterexample often exploits a gap that this tool can identify.
Symptom: The counterexample reaches an action without a required precondition being true.
Trace signature: A variable the assertion depends on is never set to the expected value because the action fired without the necessary require guard.
Step 1: stream.send <-- fires without connection being established
connected = false <-- should be guarded: require connected(the_cid)
Root cause: A before block is missing a require statement, or the require does not cover all necessary preconditions.
Fix: Add the missing require to the before block:
before stream.send(id:stream_id, data:stream_data) {
require connected(the_cid); # Add missing guard
require stream_state(id) = open; # Add missing guard
}
Symptom: A state variable has an unexpected value in Step 1 (the very first step), before any action has modified it.
Trace signature: A relation or function has an arbitrary value because no after init block sets it.
Step 1: packet_event
conn_state = closed <-- expected: should be initialized to 'idle'
Root cause: The specification does not include an after init block for this state variable, so Ivy treats it as unconstrained (any value is possible).
Fix: Add initialization:
after init {
conn_state(C) := idle; # Initialize for all connection IDs
conn_seen(C) := false; # Initialize boolean relation
}
Symptom: A monitor triggers on the wrong action, or a before/after block is attached to the wrong event.
Trace signature: The counterexample shows an action firing that should have been constrained, but the constraint is on a different action.
Step 1: frame.rst_stream.handle <-- this action is unconstrained
stream_state = open <-- violation: should require stream_state = sending
Meanwhile, the require guard exists but is attached to frame.stream.handle instead of frame.rst_stream.handle.
Root cause: The before/after monitor watches the wrong action, or uses the wrong mixin_kind (e.g., before when after is needed for state update checks).
Fix: Move or duplicate the constraint to the correct action:
before frame.rst_stream.handle(f:frame.rst_stream, scid:cid, dcid:cid) {
require stream_state(f.id) = sending; # Guard on the correct action
}
Symptom: The invariant asserts something that is temporarily false during a legitimate state transition, and the counterexample catches the transient state.
Trace signature: The state is correct at the start and end of a multi-step sequence, but the invariant fires during an intermediate step.
Step 1: connection.open
handshake_done = false <-- invariant: require handshake_done -> data_sent
data_sent = false <-- OK: both false, implication holds
Step 2: connection.handshake_complete
handshake_done = true (was: false)
data_sent = false <-- VIOLATION: handshake_done is true but data_sent is still false
Root cause: The invariant handshake_done -> data_sent is too strong -- it does not account for the state between handshake completion and the first data send.
Fix options:
handshake_done & ~in_handshake_transition -> data_sent_finalize instead of an invariant, so it only checks end-stateWhen the counterexample shows an action firing in an invalid state, add require statements to the before block:
before action_name(...) {
require precondition_1;
require precondition_2;
if _generating {
require additional_test_generation_constraint;
}
}
Use ivy_coverage(mode="gaps") to find other state variables that may also need guards.
When the counterexample shows an unexpected initial value, add after init blocks. Check all state variables used in the failing assertion:
after init {
relation_name(X) := false;
function_name(X) := default_value;
}
When a single monitor tries to handle too many cases, split it into per-action monitors:
# Instead of one broad monitor on packet_event:
before frame.stream.handle(f, scid, dcid, e) { ... }
before frame.ack.handle(f, scid, dcid, e) { ... }
before frame.rst_stream.handle(f, scid, dcid, e) { ... }
| Check Type | Where to Place |
|---|---|
| Preconditions (must hold before action) | before block with require |
| State updates (record what happened) | after block with assignment |
| Compliance checks (verify response) | after block with require |
| End-state properties (hold at test end) | _finalize action |
| Always-true properties | invariant (use sparingly) |
ivy_verify fails on quic_server_test_stream.ivy with this counterexample_trace:
Violated assertion (Line 87):
require stream_data_sent(S)
Execution trace (3 steps):
--------------------------------------------------
Step 1: quic_connection.open
conn_seen = true
cid = 0xABCD
connected = true
Step 2: frame.stream.handle
stream_id = 4
stream_state = idle (was: idle)
bytes_sent = 0
Step 3: _finalize
stream_data_sent = false
require stream_data_sent(S) at line 87, inside _finalizestream_state stays idle -- it was never transitioned to open or sending. The bytes_sent = 0 confirms no data was actually sent.frame.stream.handle fires but does not update stream_data_sent or stream_state. The after block for frame.stream.handle is missing the state update, or the before block does not require f.length > 0 to ensure meaningful data.ivy_query(mode="info", symbol_name="stream_data_sent")
Reveals stream_data_sent is set in after frame.stream.handle only when f.length > 0, but no before guard requires f.length > 0 during test generation.
Add a generation guard to ensure the test mirror only generates meaningful stream frames:
before frame.stream.handle(f:frame.stream, scid:cid, dcid:cid, e:quic_packet_type) {
if _generating {
require f.length > 0; # Ensure non-empty stream data
require stream_state(f.id) = open; # Ensure stream is open
}
}
After applying the fix, re-run ivy_verify to confirm the counterexample is resolved.
Related skills:
MCP tools used in this workflow:
ivy_verify -- Run verification (source of counterexamples)ivy_query (mode="info") -- Look up symbol definitionsivy_visualize (view="state_machine") -- View state transitionsivy_coverage (mode="gaps") -- Find related unguarded statenpx claudepluginhub elniak/panther-ivy-plugin --plugin panther-ivy-pluginDebugs issues in GRACE-structured projects via semantic navigation of knowledge graphs, verification plans, and blocks to analyze mismatches and apply targeted fixes.
Provides a structured root-cause debugging workflow for any bug, test failure, or unexpected behavior. Run before proposing fixes to avoid random or symptom-level patches.
Executes systematic debugging loop: reproduce bug, analyze root cause, apply fix, verify with independent agent challenge to confirm fundamental resolution over workarounds.