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.

Install with Tessl CLI

npx tessl i github:ArabelaTso/Skills-4-SE --skill abstract-invariant-generator

What are skills?

Review — 92%

Does it follow best practices?

Validation — 11 / 11 Passed

Validation for skill structure

SKILL.md

Review

Evals

Evaluation results

100%

Formal Verification of Insertion Sort in Dafny

Dafny loop invariants for sorting

Criteria

Without context

With context

Sorted postcondition

100%

Permutation preservation postcondition

100%

Length/modifies clause

100%

Outer loop bounds invariant

100%

Outer loop progress invariant

100%

Outer loop permutation invariant

100%

Inner loop bounds invariant

100%

Inner loop key-shift invariant

80%

100%

Outer loop decreases

100%

Inner loop decreases

100%

analysis.md documents invariants

100%

Sorted predicate helper

100%

Without context: $2.9665 · 22m 47s · 22 turns · 35 in / 97,304 out tokens

With context: $3.9240 · 29m 17s · 23 turns · 5,547 in / 115,508 out tokens

96%

ACSL Annotations for a Safety-Critical C Search Library

ACSL annotations and preconditions/postconditions

Criteria

Without context

With context

\valid memory precondition

100%

n > 0 precondition

42%

Sorted precondition

100%

Not-found postcondition

88%

100%

Found postcondition

100%

Loop invariant bounds

100%

Loop invariant lower exclusion

100%

Loop invariant upper exclusion

100%

Loop variant

100%

contracts_explanation.md preconditions

100%

contracts_explanation.md loop invariant verification

100%

Without context: $0.3046 · 2m 49s · 11 turns · 16 in / 7,205 out tokens

With context: $0.9581 · 5m 46s · 24 turns · 17,373 in / 8,608 out tokens

93%

-2%

Dafny Verification of a Quicksort Implementation

Partition invariants and frame conditions

Criteria

Without context

With context

Partition: lower region invariant

100%

Partition: upper region invariant

100%

Partition: bounds invariant

100%

Partition: permutation preservation invariant

100%

Partition: modifies clause

100%

Partition: pivot index postcondition

100%

QuickSort: sorted postcondition

100%

QuickSort: permutation postcondition

100%

Partition: decreases clause

28%

verification_notes.md: invariant explanation

100%

verification_notes.md: abstract interpretation

100%

Helper predicate

100%

Without context: $1.1915 · 8m 37s · 18 turns · 24 in / 28,712 out tokens

With context: $1.4641 · 17m 46s · 26 turns · 30 in / 20,458 out tokens

Evaluated: about 11 hours ago
Agent: Claude Code

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.