invariant-inference
Infers likely loop invariants and function contracts by observing execution traces, synthesizing candidates, and checking them inductively. Use when a verifier rejects a loop because the invariant is missing or too weak, when a Daikon-style tool is needed, or before translating code to a verification language.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill invariant-inference97
Quality
96%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly defines a specialized formal verification capability. It provides specific actions, comprehensive trigger scenarios, and uses domain-appropriate terminology that would help Claude accurately select this skill when users need invariant inference. The description is well-structured with explicit 'Use when' guidance covering multiple relevant scenarios.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'infers likely loop invariants and function contracts', 'observing execution traces', 'synthesizing candidates', and 'checking them inductively'. These are precise technical operations. | 3 / 3 |
Completeness | Clearly answers both what ('Infers likely loop invariants and function contracts by observing execution traces, synthesizing candidates, and checking them inductively') AND when ('Use when a verifier rejects a loop because the invariant is missing or too weak, when a Daikon-style tool is needed, or before translating code to a verification language'). | 3 / 3 |
Trigger Term Quality | Includes natural keywords users in this domain would use: 'loop invariants', 'function contracts', 'execution traces', 'verifier', 'Daikon-style tool', 'verification language'. Good coverage of terms a formal verification user would naturally mention. | 3 / 3 |
Distinctiveness Conflict Risk | Highly specialized niche in formal verification with distinct triggers like 'loop invariants', 'verifier rejects', 'Daikon-style', and 'verification language'. Unlikely to conflict with general coding or documentation skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
92%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a high-quality skill that efficiently teaches invariant inference with both dynamic and static approaches. The worked example with actual trace data is excellent, and the explicit validation steps (inductive check, sufficiency check) provide clear feedback loops. Minor improvement could come from linking to related skills or reference materials for advanced topics mentioned.
Suggestions
Consider adding links to related skills or reference files for advanced topics like polynomial domains, ghost variables, or SMT solver usage
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is lean and efficient, assuming Claude's competence with verification concepts. No unnecessary explanations of basic programming or what invariants are conceptually—jumps straight to actionable methodology. | 3 / 3 |
Actionability | Provides concrete executable guidance with a complete worked example, specific template library, step-by-step process, and clear output format. The find_max example is fully traced with actual values. | 3 / 3 |
Workflow Clarity | Clear 5-step sequence with explicit validation checkpoints (inductive check, sufficiency check). The workflow includes feedback loops—if a candidate fails inductiveness, it's pruned; if insufficient, seek stronger invariants. | 3 / 3 |
Progressive Disclosure | Content is well-organized with clear sections and tables, but it's a moderately long single file. The reference to 'abstract-invariant-generator' suggests related tools that could be linked. No external file references for advanced topics like polynomial domains or ghost variables. | 2 / 3 |
Total | 11 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.