abstract-invariant-generator

Uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions for formal verification. Generates invariants that capture program behavior and support correctness proofs in Dafny, Isabelle, Coq, and other verification systems. Use when adding formal specifications to code, generating verification conditions, inferring contracts for functions, or discovering loop invariants for proofs.

1.00x

Quality

92%

Does it follow best practices?

Impact

96%

1.00x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Quality

Content

85%

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

This is a strong skill with excellent actionability and workflow clarity, providing concrete executable examples across multiple verification systems. The main weakness is verbosity - the content could be more concise by consolidating similar examples and reducing explanatory text that Claude would already understand about abstract interpretation concepts.

Suggestions

Consolidate similar loop invariant examples (counter, accumulator, search) into a single table or more compact format rather than repeating the full code-then-invariant pattern for each

Remove explanatory text like 'For each loop, generate an invariant that: 1. Holds before the loop (initialization)...' as Claude understands invariant properties

Dimension	Reasoning	Score
Conciseness	The skill is comprehensive but includes some redundancy, particularly in the multiple similar examples for different loop types and the extensive explanations that could be condensed. The content is useful but could be tightened significantly.	2 / 3
Actionability	Provides fully executable code examples across multiple verification languages (Dafny, Isabelle, Coq, ACSL). Each pattern includes concrete, copy-paste ready invariant specifications with clear input/output examples.	3 / 3
Workflow Clarity	Clear 6-step workflow with explicit sequencing from identification through expression in target language. Each step has concrete examples and the complete insertion sort example demonstrates the full process with detailed explanations.	3 / 3
Progressive Disclosure	Well-structured with clear sections progressing from overview to detailed patterns. References to external files (loop_invariants.md, function_contracts.md, etc.) are clearly signaled at the end for deeper exploration.	3 / 3
	Total	11 / 12 Passed

Description

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 uses third person voice correctly, lists specific concrete actions, names relevant tools and techniques, and provides explicit 'Use when' guidance with natural trigger terms. The description effectively carves out a distinct niche that would not conflict with other skills.

Dimension	Reasoning	Score
Specificity	Lists multiple specific concrete actions: 'infer loop invariants', 'function preconditions', 'postconditions', 'generates invariants', 'support correctness proofs'. Names specific tools (Dafny, Isabelle, Coq) and techniques (abstract interpretation).	3 / 3
Completeness	Clearly answers both what ('uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions') AND when ('Use when adding formal specifications to code, generating verification conditions, inferring contracts for functions, or discovering loop invariants for proofs').	3 / 3
Trigger Term Quality	Excellent coverage of natural terms users would say: 'loop invariants', 'preconditions', 'postconditions', 'formal verification', 'Dafny', 'Isabelle', 'Coq', 'verification conditions', 'contracts', 'proofs'. These are the exact terms someone working in formal methods would use.	3 / 3
Distinctiveness Conflict Risk	Highly distinctive niche in formal verification with specific triggers like 'abstract interpretation', 'loop invariants', 'Dafny', 'Isabelle', 'Coq'. Unlikely to conflict with general coding or documentation skills due to specialized domain terminology.	3 / 3
	Total	12 / 12 Passed

Validation

100%

Warnings & errors only

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.

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Reviewed: 4 months ago

Table of Contents

Discovery Implementation Validation

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.