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

Preview

This is a new way to view eval results. We're still working on it, so the layout may change.

Run	Type	Date	Status
baseline vs usage-spec With / without context 7 months ago Completed	With / without context	7 months ago	Completed

Eval run

019cc47a-d3eb-767b-9038-f317ba8b60f8

Run 7 months ago

Stats are not available yet

The run is available. Its result stats will appear here when they are ready.

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

Evaluated: 7 months ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Formal Verification of Insertion Sort in Dafny ACSL Annotations for a Safety-Critical C Search Library Dafny Verification of a Quicksort Implementation

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.