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

80%

Does it follow best practices?

Impact

96%

1.00x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Quality

Content

68%Weight 40%Scale 1-5

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

Highly actionable with concrete multi-language examples and a clear workflow, but held back by length/repetition and by the absence of an explicit verification feedback loop for a fundamentally proof-based task.

Suggestions

Add an explicit verification checkpoint step to the workflow: after expressing invariants in the target language, run the prover/verifier; if it fails, strengthen the flagged invariant and re-run until it discharges.

Trim redundancy by consolidating the 'Invariant Patterns'/'Numeric Bounds'/'Array Properties'/'Data Structure Properties' sections, which largely restate invariants already shown in Steps 3-5.

Move the bulk of the per-language syntax reference (Step 6) and the pattern catalog into the existing reference files, keeping SKILL.md as a concise overview that links out.

Dimension	Reasoning	Score
Conciseness	Mostly efficient with no concept-explaining fluff, but the ~440-line body repeats invariant forms across Steps 3-6 and the 'Invariant Patterns' sections restate already-shown invariants, so it could be tightened.	3 / 5
Actionability	Provides copy-paste-ready generated invariants and complete, spec-ready code in Dafny, Isabelle, Coq, and ACSL, with concrete examples covering common loop and contract cases.	5 / 5
Workflow Clarity	A clear six-step sequence with a complete worked example is present, but verification/proof generation is fragile work and the body lacks an explicit validate-in-prover -> strengthen -> re-run checkpoint loop, capping this dimension.	3 / 5
Progressive Disclosure	Four real, clearly-labeled reference files are linked one level deep, but substantial pattern/template and multi-language-syntax content that could live in those files remains fully inlined, leaving the split only partial.	4 / 5
	Total	15 / 20 Passed

Description

92%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

A strong, third-person description that concretely names capabilities and target verification systems while providing explicit 'Use when...' trigger guidance. Only minor gap is missing a few synonyms a user might naturally invoke.

Dimension	Reasoning	Score
Specificity	Lists multiple concrete actions (infer loop invariants, preconditions, postconditions; generate verification conditions) across named target systems (Dafny, Isabelle, Coq), giving comprehensive coverage of contract types.	5 / 5
Completeness	Explicitly states both what it does ('Uses abstract interpretation to automatically infer...') and when to use it ('Use when adding formal specifications...'), with concrete trigger phrases.	5 / 5
Trigger Term Quality	Good natural-term coverage ('loop invariants', 'contracts', 'formal specifications', 'preconditions/postconditions'), but a few relevant synonyms a user might say (e.g. 'Hoare logic', 'assertions', 'specifications') are not present.	4 / 5
Distinctiveness Conflict Risk	Occupies a clear niche (abstract interpretation for formal verification) with distinct triggers and named verification systems, giving minimal conflict risk with other skills.	5 / 5
	Total	19 / 20 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 — 16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository: ArabelaTso/Skills-4-SE
Path: skills/abstract-invariant-generator/SKILL.md
Commit: 4f38503

Reviewed: 19 days 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.