Use when designing or auditing a CAV (Computer Aided Verification) empirical evaluation, covering standard benchmark sets (SV-COMP/SMT-COMP/HWMCC/VNN-COMP), fair baseline solvers with pinned versions and equal resource limits, timeout-dominated comparisons, soundness cross-checks and proof witnesses, cactus/scatter reporting, and matching evidence to the shape of each verification claim.
SkillScore86Maintained
Automatic
◆Research pack
Last verified 8/15/2026
What it changes
Passed 19 of 22 test cases with the skill, and 3 of 22 without it.
Without skill14%
With skill86%
Checks it passed that the model alone missed
Includes `[Evaluation readiness] weak`
Includes `[Evaluation readiness] strong`
Includes `[Evaluation readiness] adequate`
and 1 more in the full report
18 fixed1 passed either way1 still failing2 broke
Pass-rate lift
+73 pp
Tokens
-7%
Agent turns
0%
Response time
-49%
Model gemini-3.6-flashMeasured 8/15/2026v119 of 22 cases passed with skill
Tokens, turns and time describe resource use, not a dollar price.
See it in action
One of 18 test cases the skill fixed. Same model, same prompt, with and without the skill.
1 of 18
Prompt
We are submitting an SMT-COMP evaluation of our string solver. We compared our system against Z3 version 4.4.1 (released in 2015) and CVC4 version 1.6 (released in 2018), even though Z3 4.12+ and CVC5 1.0+ are available. We used identical 300-second limits on identical hardware. Audit our baseline selection.
What was checked, without and with the skill
Checked
Without skill
With skill
Includes `[Evaluation readiness] weak`
Missed
Passed
Identifies comparing against outdated tool releases (such as Z3 4.4.1 or CVC4 1.6) as an unfair baseline comparison.
Passed
Passed
case-11 · gemini-3.6-flash · 8/15/2026 · answers are capped and redacted
What's inside
The instructions your model reads when the skill loads.
SKILL.md79 linessingle file
CAV Experiments
Use this before submission when the evaluation is not yet locked. CAV reviewers are verification
researchers; the empirical section is where a good technique is won or lost. The organizing principle
is evidence proportional to the claim — the evaluation must test what the paper asserts, on
benchmarks and baselines a skeptic accepts, under a resource budget that makes the comparison fair.
Evaluation audit
Match evidence to the claim shape. A soundness claim needs a proof and/or a checkable
witness, not a benchmark score. A performance claim needs a fair comparison on standard
benchmarks under equal limits. A capability claim ("solves instances prior tools cannot") needs
those instances and the prior tools actually run.
Use standard benchmark sets at a pinned revision (SV-COMP, SMT-COMP, HWMCC, VNN-COMP, or a
documented domain set). State the subset you ran and why; a hand-picked set invites the
"cherry-picked" reject.
Choose fair baselines: the strongest relevant prior tool(s), at their latest released
version, run with a documented, equal resource limit (per-instance time and memory) on the
same hardware. An outdated or mis-configured baseline is a scored weakness.
Respect that verification comparisons are timeout-dominated. Report the limit explicitly;
distinguish solved / unsolved / timeout / memout / error; and prefer cactus plots (instances
solved vs. time) and scatter plots (per-instance head-to-head) over a single mean that a few
timeouts distort.
Cross-check soundness. Run a differential check against a trusted tool on all verdicts and
report disagreements (ideally none); ship proof witnesses where correctness is the claim.
Design limits in, not on: know before you run which logics, property classes, or sizes the
method will not cover, and report them honestly.
Claim-to-evidence design table
Verification claim
Matching evidence
Reject pattern avoided
"Procedure is sound/complete"
Theorem + proof; witness + independent checker
"Soundness asserted, never checked"
"Faster than prior tool"
Standard set (pinned), latest baseline, equal limits, cactus+scatter
"Untuned/old baseline; unequal limits"
"Solves instances others cannot"
Those instances run on both tools, at the stated limit
"Only our tool was run on them"
"Scales to large systems"
Runtime/memory across realistic sizes; largest instance stated
"Only small inputs; 'large' undefined"
"General across a theory/domain"
A diverse benchmark sample + explicit out-of-scope classes
"One family, claimed universal"
Fair-comparison checklist (the reviewer's first objections)