New: 98,000+ skills indexed from GitHub repos with 100+ stars · every skill safety-checkedBrowse top skillsTop skills
Esc to closeBrowse all skills
Submit a skillBrowse skills
Submit a skillBrowse skills

Agent skill

Abstract Invariant Generator

by ArabelaTso in ArabelaTso/Skills-4-SE

Uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions for formal verification.

Apache-2.0Auto-check passed

Install Abstract Invariant Generator

skills CLI
$ npx skills add ArabelaTso/Skills-4-SE --skill abstract-invariant-generator -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI
$ gh skill install ArabelaTso/Skills-4-SE abstract-invariant-generator --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy
$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .claude/skills && cp -r skills-src/skills/abstract-invariant-generator .claude/skills/abstract-invariant-generator && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Facts

Skill name
abstract-invariant-generator
GitHub stars
253
Token cost
~2.4k tokens
SKILL.md length
422 words
Files
5 (incl. references)
Skills in repo
170
Repo updated
First seen
Licence
Apache-2.0

At a glance

Uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions for formal verification.

  • Works in 6 steps: Identify Specification Points → Perform Abstract Interpretation → Generate Loop Invariants → …
  • Adding formal specifications to code
  • SKILL.md covers Overview, Invariant Generation Workflow, Complete Example and Invariant Patterns, plus 3 more sections
  • Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Abstract Invariant Generator is an agent skill from ArabelaTso/Skills-4-SE. 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.

Its SKILL.md is about 2.4k tokens, which your agent loads only when the skill is triggered. The skill folder holds 5 other files, including reference files (for example `references/function_contracts.md`, `references/invariant_templates.md` and `references/loop_invariants.md`).

The repository describes itself as: A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows. The licence is Apache-2.0.

When your agent uses it

  • Adding formal specifications to code
  • Generating verification conditions
  • Inferring contracts for functions
  • Discovering loop invariants for proofs

Example prompts

  • “Use the abstract-invariant-generator skill to use abstract interpretation to automatically infer loop invariants, function preconditions, and…”
  • “/abstract-invariant-generator”

Requirements

  • Python 3

Workflow steps

6 steps, taken from the step headings in SKILL.md.

  1. Identify Specification Points
  2. Perform Abstract Interpretation
  3. Generate Loop Invariants
  4. Generate Function Preconditions
  5. Generate Function Postconditions
  6. Express in Target Language

What it can do on your machine

Read from SKILL.md and the folder at commit 4f38503. It shows what the files ask for, not the result of running them.

  • Tool permissions

    Pre-approves nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.

    From allowed-tools in the SKILL.md frontmatter.

  • Runs code

    No scripts in the folder and no shell commands in SKILL.md (its code samples are python, dafny, isabelle, coq and c).

    From the folder's file list and the shell code blocks in SKILL.md.

  • Network

    No URLs in SKILL.md.

    From URLs in SKILL.md, links to its own repository left out.

  • Credentials

    Names no API keys, tokens, secrets or passwords.

    From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Abstract Invariant Generator loads about 2.4k tokens when it runs, and up to ~12k if it reads all its reference files. Until then it costs about 116 tokens; SKILL.md has 422 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it
~116
When it runs · the whole SKILL.md, loaded when a task matches
~2.4k
With references · SKILL.md plus every file in references/, read only if the agent opens them
~12k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check passed

The automated check found no risky patterns in SKILL.md.

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from ArabelaTso/Skills-4-SE at commit 4f38503, republished under its Apache-2.0 licence (© ArabelaTso). 422 words, ~2,418 tokens.

Download SKILL.mdSave it as .claude/skills/abstract-invariant-generator/SKILL.md (or your agent's skills folder). This skill also uses 4 other files; get the full folder from GitHub.
name
abstract-invariant-generator
description
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.

Abstract Invariant Generator

Overview

This skill uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions. It generates formal specifications that support verification and reasoning about program correctness.

Invariant Generation Workflow

Step 1: Identify Specification Points

Analyze the code to identify where invariants are needed:

Loop Invariants: For each loop

python
while condition:
    # Need: invariant that holds before/after each iteration
    body

Function Contracts: For each function

python
def function(params):
    # Need: precondition (what must be true on entry)
    body
    # Need: postcondition (what is guaranteed on exit)

Assertions: For verification points

python
# Need: invariant that holds at this point
assert property
Step 2: Perform Abstract Interpretation

Use abstract domains to infer properties:

Interval Analysis: Infer numeric ranges

python
i = 0
while i < n:
    # Inferred: 0 ≤ i < n
    i += 1
# Inferred: i = n

Relational Analysis: Infer relationships between variables

python
i = 0
j = 0
while i < n:
    # Inferred: i = j
    i += 1
    j += 1

Shape Analysis: Infer data structure properties

python
while node is not None:
    # Inferred: node is in the linked list
    node = node.next
Step 3: Generate Loop Invariants

For each loop, generate an invariant that:

  1. Holds before the loop (initialization)
  2. Is preserved by the loop body (maintenance)
  3. Combined with loop exit, implies desired property (termination)

Template-Based Generation:

Counter Loop:

python
i = 0
while i < n:
    arr[i] = 0
    i += 1

Generated Invariant:

invariant 0 ≤ i ≤ n
invariant ∀k. 0 ≤ k < i ⟹ arr[k] = 0

Accumulator Loop:

python
sum = 0
i = 0
while i < len(arr):
    sum += arr[i]
    i += 1

Generated Invariant:

invariant 0 ≤ i ≤ len(arr)
invariant sum = Σ(arr[0..i-1])

Search Loop:

python
i = 0
found = False
while i < len(arr) and not found:
    if arr[i] == target:
        found = True
    else:
        i += 1

Generated Invariant:

invariant 0 ≤ i ≤ len(arr)
invariant ∀k. 0 ≤ k < i ⟹ arr[k] ≠ target
invariant found ⟹ arr[i] = target
Step 4: Generate Function Preconditions

Infer what must be true for the function to work correctly:

Array Access Function:

python
def get_element(arr, index):
    return arr[index]

Generated Precondition:

requires 0 ≤ index < len(arr)
requires arr is not None

Division Function:

python
def divide(x, y):
    return x / y

Generated Precondition:

requires y ≠ 0

Linked List Function:

python
def get_next(node):
    return node.next

Generated Precondition:

requires node is not None
Step 5: Generate Function Postconditions

Infer what the function guarantees on exit:

Maximum Function:

python
def find_max(arr):
    max_val = arr[0]
    for i in range(1, len(arr)):
        if arr[i] > max_val:
            max_val = arr[i]
    return max_val

Generated Postcondition:

ensures result ∈ arr
ensures ∀x ∈ arr. x ≤ result

Sorting Function:

python
def sort(arr):
    # ... sorting logic ...
    return sorted_arr

Generated Postcondition:

ensures len(result) = len(arr)
ensures ∀i. 0 ≤ i < len(result)-1 ⟹ result[i] ≤ result[i+1]
ensures multiset(result) = multiset(arr)

Search Function:

python
def binary_search(arr, target):
    # ... search logic ...
    return index

Generated Postcondition:

ensures result = -1 ∨ (0 ≤ result < len(arr) ∧ arr[result] = target)
ensures result ≠ -1 ⟹ arr[result] = target
ensures result = -1 ⟹ target ∉ arr
Step 6: Express in Target Language

Format invariants for the target verification system:

Dafny:

dafny
method FindMax(arr: array<int>) returns (max: int)
  requires arr.Length > 0
  ensures max in arr[..]
  ensures forall i :: 0 <= i < arr.Length ==> arr[i] <= max
{
  max := arr[0];
  var i := 1;
  while i < arr.Length
    invariant 1 <= i <= arr.Length
    invariant max in arr[..i]
    invariant forall k :: 0 <= k < i ==> arr[k] <= max
  {
    if arr[i] > max {
      max := arr[i];
    }
    i := i + 1;
  }
}

Isabelle/HOL:

isabelle
lemma find_max_correct:
  assumes "length arr > 0"
  shows "find_max arr ∈ set arr ∧
         (∀x ∈ set arr. x ≤ find_max arr)"

Coq:

coq
Lemma find_max_correct : forall (arr : list nat),
  length arr > 0 ->
  In (find_max arr) arr /\
  (forall x, In x arr -> x <= find_max arr).

ACSL (for C):

c
/*@ requires n > 0;
  @ requires \valid(arr + (0..n-1));
  @ ensures \result >= 0 && \result < n;
  @ ensures \forall integer k; 0 <= k < n ==> arr[k] <= arr[\result];
  @*/
int find_max(int arr[], int n) {
  int max_idx = 0;
  /*@ loop invariant 1 <= i <= n;
    @ loop invariant 0 <= max_idx < i;
    @ loop invariant \forall integer k; 0 <= k < i ==> arr[k] <= arr[max_idx];
    @ loop variant n - i;
    @*/
  for (int i = 1; i < n; i++) {
    if (arr[i] > arr[max_idx]) {
      max_idx = i;
    }
  }
  return max_idx;
}
Show full SKILL.md (211 more words)Show less

Complete Example

Input Code (Python):

python
def insertion_sort(arr):
    for i in range(1, len(arr)):
        key = arr[i]
        j = i - 1
        while j >= 0 and arr[j] > key:
            arr[j + 1] = arr[j]
            j -= 1
        arr[j + 1] = key

Analysis:

Outer Loop (for i in range(1, len(arr))):

  • i ranges from 1 to len(arr)
  • After each iteration, arr[0..i] is sorted
  • Elements are permutation of original

Inner Loop (while j >= 0 and arr[j] > key):

  • j decreases from i-1 to -1
  • Shifts elements greater than key to the right
  • Maintains: arr[j+2..i+1] contains elements > key

Generated Invariants (Dafny):

dafny
method InsertionSort(arr: array<int>)
  requires arr.Length >= 0
  ensures sorted(arr[..])
  ensures multiset(arr[..]) == multiset(old(arr[..]))
  modifies arr
{
  var i := 1;
  while i < arr.Length
    invariant 1 <= i <= arr.Length
    invariant sorted(arr[..i])
    invariant multiset(arr[..]) == multiset(old(arr[..]))
  {
    var key := arr[i];
    var j := i - 1;

    while j >= 0 && arr[j] > key
      invariant -1 <= j < i
      invariant sorted(arr[..j+1])
      invariant sorted(arr[j+2..i+1])
      invariant forall k :: j+2 <= k <= i ==> arr[k] > key
      invariant multiset(arr[..]) == multiset(old(arr[..]))
    {
      arr[j + 1] := arr[j];
      j := j - 1;
    }

    arr[j + 1] := key;
    i := i + 1;
  }
}

predicate sorted(s: seq<int>) {
  forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

Explanation:

Outer Loop Invariants:

  1. 1 <= i <= arr.Length: Loop counter bounds
  2. sorted(arr[..i]): First i elements are sorted
  3. multiset(arr[..]) == multiset(old(arr[..])): Permutation preservation

Inner Loop Invariants:

  1. -1 <= j < i: Loop counter bounds
  2. sorted(arr[..j+1]): Elements before j+1 remain sorted
  3. sorted(arr[j+2..i+1]): Shifted elements remain sorted
  4. forall k :: j+2 <= k <= i ==> arr[k] > key: Shifted elements are greater than key
  5. multiset(arr[..]) == multiset(old(arr[..])): Permutation preservation

Invariant Patterns

Numeric Bounds
invariant 0 ≤ i ≤ n
invariant low ≤ mid ≤ high
Array Properties
invariant ∀k. 0 ≤ k < i ⟹ P(arr[k])
invariant sorted(arr[0..i])
invariant arr[i] = max(arr[0..i])
Relationships
invariant i + j = n
invariant i = 2 * j
invariant sum = Σ(arr[0..i-1])
Data Structure Properties
invariant acyclic(list)
invariant node ∈ reachable(head)
invariant size(tree) = n
Permutation
invariant multiset(arr) = multiset(old(arr))
invariant set(arr) = set(old(arr))

Strengthening Weak Invariants

Sometimes initial invariants are too weak. Strengthen them:

Weak:

invariant 0 ≤ i ≤ n

Strengthened:

invariant 0 ≤ i ≤ n
invariant ∀k. 0 ≤ k < i ⟹ processed(arr[k])

Technique: Add properties about what has been accomplished so far.

Handling Complex Loops

Nested Loops

Generate invariants for each level:

python
for i in range(n):
    for j in range(m):
        matrix[i][j] = 0

Invariants:

Outer loop:
  invariant 0 ≤ i ≤ n
  invariant ∀r. 0 ≤ r < i ⟹ (∀c. 0 ≤ c < m ⟹ matrix[r][c] = 0)

Inner loop:
  invariant 0 ≤ j ≤ m
  invariant ∀c. 0 ≤ c < j ⟹ matrix[i][c] = 0
Multiple Exit Conditions

Handle all exit paths:

python
while i < n and not found:
    if arr[i] == target:
        found = True
    i += 1

Invariants:

invariant 0 ≤ i ≤ n
invariant found ⟹ arr[i-1] = target
invariant ¬found ⟹ (∀k. 0 ≤ k < i ⟹ arr[k] ≠ target)

References

For detailed invariant generation techniques and patterns:

  • references/loop_invariants.md: Loop invariant patterns and generation strategies
  • references/function_contracts.md: Precondition and postcondition inference
  • references/invariant_templates.md: Common invariant templates by algorithm type
  • references/verification_languages.md: Syntax for different verification systems

© ArabelaTso, Apache-2.0. Rendered from Markdown: HTML in the file is shown as text, images as links, and headings moved down two levels. Raw file

Files

SKILL.md and 4 other files (references) in skills/abstract-invariant-generator of ArabelaTso/Skills-4-SE.

  • SKILL.md
  • references/function_contracts.md
  • references/invariant_templates.md
  • references/loop_invariants.md
  • references/verification_languages.md

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Abstract Invariant Generator next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Abstract Invariant Generator compared with similar skills
SkillStarsUsed inTokensAuto-checkLicenceRepo updated
Abstract Invariant Generator this skillArabelaTso/Skills-4-SE253—~2.4kAutomated safety check: PassApache-2.0
Generatealirezarezvani/claude-skills28k1 repos~1.1kAutomated safety check: PassMIT
Cloud Function Generatorjeremylongshore/tons-of-skills-marketplace2.8k—~568Automated safety check: PassMIT
Lambda Function Generatorjeremylongshore/tons-of-skills-marketplace2.8k—~570Automated safety check: PassMIT
Window Function Generatorjeremylongshore/tons-of-skills-marketplace2.8k—~580Automated safety check: PassMIT
Graphical Abstract Generatoraipoch/medical-research-skills1.9k—~3.2kAutomated safety check: PassMIT

Similar skills

  • Generate

    alirezarezvani/claude-skills

    Generate Playwright tests. An agent skill from alirezarezvani/claude-skills.

    28k GitHub starsUsed in 1 repo~1.1k tokens
    Testing & QAAuto-check passed

  • Cloud Function Generator

    jeremylongshore/tons-of-skills-marketplace

    Generate cloud function generator operations. An agent skill from jeremylongshore/tons-of-skills-marketplace.

    2.8k GitHub stars~568 tokensUpdated today
    Backend & APIsAuto-check passed

  • Lambda Function Generator

    jeremylongshore/tons-of-skills-marketplace

    Generate lambda function generator operations. An agent skill from jeremylongshore/tons-of-skills-marketplace.

    2.8k GitHub stars~570 tokensUpdated today
    Backend & APIsAuto-check passed

  • Window Function Generator

    jeremylongshore/tons-of-skills-marketplace

    Generate window function generator operations. An agent skill from jeremylongshore/tons-of-skills-marketplace.

    2.8k GitHub stars~580 tokensUpdated today
    DatabasesAuto-check passed

  • Graphical Abstract Generator

    aipoch/medical-research-skills

    Converts a biomedical study storyline into a graphical abstract and, when direct image capability is available, generates the graphical abstract directly; otherwise it falls back to prompts, Mermaid…

    1.9k GitHub stars~3.2k tokensUpdated 23 days ago
    DevelopmentAuto-check passed

  • Fal Generate

    nexu-io/open-design

    Generate images and videos using fal.ai AI models. An agent skill from nexu-io/open-design.

    100k GitHub stars~306 tokensUpdated today
    Media & CreativeAuto-check passed

More from ArabelaTso/Skills-4-SE

All 170 skills in this repo

  • Framework Migration Assistant

    ArabelaTso/Skills-4-SE

    Automatically migrate Python web applications between frameworks (Flask → FastAPI, Django → FastAPI).

    253 GitHub stars~1.9k tokensUpdated 1 mo ago
    Auto-check passed

  • Metamorphic Test Generator

    ArabelaTso/Skills-4-SE

    Generate test cases using metamorphic testing by applying transformations based on metamorphic properties.

    253 GitHub stars~798 tokensUpdated 1 mo ago
    Auto-check passed

  • Reproduction Trace Instrumenter

    ArabelaTso/Skills-4-SE

    Instruments programs to capture execution traces specifically for reproducing reported bugs, enabling consistent replay and diagnosis of failures.

    253 GitHub stars~2.4k tokensUpdated 1 mo ago
    Auto-check passed

  • Spring Mvc To Boot Migrator

    ArabelaTso/Skills-4-SE

    Automatically migrate Spring MVC applications to Spring Boot.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

  • State Snapshot Instrumenter

    ArabelaTso/Skills-4-SE

    Instrument programs (Python, C/C++, Java) to capture snapshots of key program states at runtime, including variables, memory, and call stacks.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

Questions about Abstract Invariant Generator

What does Abstract Invariant Generator do?

Uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions for formal verification. Abstract Invariant Generator is an agent skill from ArabelaTso/Skills-4-SE. Uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions for formal verification.

When should I use Abstract Invariant Generator?

Abstract Invariant Generator fits situations like: adding formal specifications to code; generating verification conditions; inferring contracts for functions; discovering loop invariants for proofs.

How do I install Abstract Invariant Generator in Claude Code?

Run `npx skills add ArabelaTso/Skills-4-SE --skill abstract-invariant-generator -a claude-code`. Or copy the skill folder (skills/abstract-invariant-generator in ArabelaTso/Skills-4-SE) into .claude/skills/abstract-invariant-generator in your project. Claude Code loads it when a task matches its description.

How do I install Abstract Invariant Generator in Codex?

Run `npx skills add ArabelaTso/Skills-4-SE --skill abstract-invariant-generator -a codex`. Or copy the skill folder (skills/abstract-invariant-generator in ArabelaTso/Skills-4-SE) into .agents/skills/abstract-invariant-generator in your project. Codex loads it when a task matches its description.

Can I use Abstract Invariant Generator in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add ArabelaTso/Skills-4-SE --skill abstract-invariant-generator -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/abstract-invariant-generator, .gemini/skills/abstract-invariant-generator, .github/skills/abstract-invariant-generator and .opencode/skills/abstract-invariant-generator in your project.

What does Abstract Invariant Generator need to run?

SKILL.md names no scripts, command-line tools or credentials: Abstract Invariant Generator is instructions for the agent only. Our summary lists: Python 3.

Does Abstract Invariant Generator access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Abstract Invariant Generator safe to install?

Our automated static check of SKILL.md found no risky patterns, such as piping downloads into a shell, reading credential files or hidden Unicode. It is not a guarantee. Review the folder before installing.

What licence does Abstract Invariant Generator use?

Abstract Invariant Generator is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Abstract Invariant Generator use?

About 2.4k tokens (SKILL.md is roughly 9.7k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full. Its references folder adds about 9.9k tokens, read only when the agent opens those files.

What are the alternatives to Abstract Invariant Generator?

Skills that share tags, products or a category with Abstract Invariant Generator: Generate (alirezarezvani/claude-skills, 28k stars), Cloud Function Generator (jeremylongshore/tons-of-skills-marketplace, 2.8k stars), Lambda Function Generator (jeremylongshore/tons-of-skills-marketplace, 2.8k stars) and Window Function Generator (jeremylongshore/tons-of-skills-marketplace, 2.8k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Abstract Invariant Generator?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 170 skills in this directory. The repository was last updated on August 21, 2026.

Source: ArabelaTso/Skills-4-SE on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.