# 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 di…

- **Type:** Skill
- **Install:** `agentstack add skill-arabelatso-skills-4-se-abstract-invariant-generator`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [ArabelaTso](https://agentstack.voostack.com/s/arabelatso)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [ArabelaTso](https://github.com/ArabelaTso)
- **Source:** https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/abstract-invariant-generator
- **Website:** https://ArabelaTso.github.io/Skills-4-SE/

## Install

```sh
agentstack add skill-arabelatso-skills-4-se-abstract-invariant-generator
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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  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 ) returns (max: int)
  requires arr.Length > 0
  ensures max in arr[..]
  ensures forall i :: 0  arr[i]  arr[k]  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  0;
  @ requires \valid(arr + (0..n-1));
  @ ensures \result >= 0 && \result  arr[k]  arr[k]  arr[max_idx]) {
      max_idx = i;
    }
  }
  return max_idx;
}
```

## 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)
  requires arr.Length >= 0
  ensures sorted(arr[..])
  ensures multiset(arr[..]) == multiset(old(arr[..]))
  modifies arr
{
  var i := 1;
  while i = 0 && arr[j] > key
      invariant -1  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) {
  forall i, j :: 0  s[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

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [ArabelaTso](https://github.com/ArabelaTso)
- **Source:** [ArabelaTso/Skills-4-SE](https://github.com/ArabelaTso/Skills-4-SE)
- **License:** Apache-2.0
- **Homepage:** https://ArabelaTso.github.io/Skills-4-SE/

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-arabelatso-skills-4-se-abstract-invariant-generator
- Seller: https://agentstack.voostack.com/s/arabelatso
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.