Agent skill

Acsl Annotation Assistant

Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs.

Apache-2.0Auto-check passed

Install Acsl Annotation Assistant

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant -a claude-code

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

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE acsl-annotation-assistant --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/acsl-annotation-assistant .claude/skills/acsl-annotation-assistant && 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/

Paste into Claude Code

Install the "acsl-annotation-assistant" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant into .claude/skills/acsl-annotation-assistant/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "acsl-annotation-assistant", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE acsl-annotation-assistant --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .agents/skills && cp -r skills-src/skills/acsl-annotation-assistant .agents/skills/acsl-annotation-assistant && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "acsl-annotation-assistant" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant into .agents/skills/acsl-annotation-assistant/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "acsl-annotation-assistant", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE acsl-annotation-assistant --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/skills/acsl-annotation-assistant .cursor/skills/acsl-annotation-assistant && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "acsl-annotation-assistant" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant into .cursor/skills/acsl-annotation-assistant/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "acsl-annotation-assistant", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/ArabelaTso/Skills-4-SE.git --path skills/acsl-annotation-assistant

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE acsl-annotation-assistant --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/skills/acsl-annotation-assistant .gemini/skills/acsl-annotation-assistant && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "acsl-annotation-assistant" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant into .gemini/skills/acsl-annotation-assistant/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "acsl-annotation-assistant", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE acsl-annotation-assistant

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .github/skills && cp -r skills-src/skills/acsl-annotation-assistant .github/skills/acsl-annotation-assistant && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "acsl-annotation-assistant" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant into .github/skills/acsl-annotation-assistant/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "acsl-annotation-assistant", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE acsl-annotation-assistant --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/skills/acsl-annotation-assistant .opencode/skills/acsl-annotation-assistant && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "acsl-annotation-assistant" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant into .opencode/skills/acsl-annotation-assistant/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "acsl-annotation-assistant", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: acsl-annotation-assistant
GitHub stars: 253
Token cost: ~1.8k tokens
SKILL.md length: 414 words
Files: 4 (incl. references)
Skills in repo: 170
Repo updated: Aug 21, 2026
First seen: Oct 7, 2026
Licence: Apache-2.0

At a glance

Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs.

Works in 10 steps: Function Contracts → Loop Annotations → Memory Safety Specifications → …
Working with formal verification
SKILL.md covers Core Capabilities, Annotation Workflow, Common ACSL Constructs and Verification Considerations, plus 4 more sections
Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Acsl Annotation Assistant is an agent skill from ArabelaTso/Skills-4-SE. Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs. Use this skill when working with formal verification, adding function contracts (requires/ensures), loop invariants, assertions, memory safety annotations, or any ACSL specifications. Supports Frama-C verification and generates comprehensive formal specifications for C/C++ code.

Its SKILL.md is about 1.8k tokens, which your agent loads only when the skill is triggered. The skill folder holds 4 other files, including reference files (for example `references/acsl_reference.md`, `references/common_patterns.md` and `references/frama_c_integration.md`).

It works with C++. 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

Working with formal verification
Adding function contracts (requires/ensures)
Loop invariants
Memory safety annotations

Example prompts

“/acsl-annotation-assistant”

Workflow steps

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

Function Contracts
Loop Annotations
Memory Safety Specifications
Assertions and Assumptions
Axiomatic Definitions and Predicates
Analyze the Function
Add Function Contract
Annotate Loops
Add Assertions
Define Helper Predicates

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 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

Acsl Annotation Assistant loads about 1.8k tokens when it runs, and up to ~9.3k if it reads all its reference files. Until then it costs about 98 tokens; SKILL.md has 414 words of instructions outside code blocks.

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

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). 414 words, ~1,751 tokens.

Download SKILL.mdSave it as .claude/skills/acsl-annotation-assistant/SKILL.md (or your agent's skills folder). This skill also uses 3 other files; get the full folder from GitHub.

name: acsl-annotation-assistant
description: Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs. Use this skill when working with formal verification, adding function contracts (requires/ensures), loop invariants, assertions, memory safety annotations, or any ACSL specifications. Supports Frama-C verification and generates comprehensive formal specifications for C/C++ code.

ACSL Annotation Assistant

Generate comprehensive ACSL (ANSI/ISO C Specification Language) annotations for C/C++ programs to support formal verification with tools like Frama-C.

Core Capabilities

1. Function Contracts

Add complete function specifications with preconditions and postconditions:

/*@
  requires \valid(array + (0..n-1));
  requires n > 0;
  ensures \result >= 0 && \result < n;
  ensures \forall integer i; 0 <= i < n ==> array[\result] >= array[i];
  assigns \nothing;
*/
int find_max_index(int *array, int n);

2. Loop Annotations

Generate loop invariants, variants, and assigns clauses:

/*@
  loop invariant 0 <= i <= n;
  loop invariant \forall integer k; 0 <= k < i ==> sum == \sum(0, k, array);
  loop assigns i, sum;
  loop variant n - i;
*/
for (i = 0; i < n; i++) {
    sum += array[i];
}

3. Memory Safety Specifications

Add pointer validity and separation annotations:

/*@
  requires \valid(dest + (0..n-1));
  requires \valid_read(src + (0..n-1));
  requires \separated(dest + (0..n-1), src + (0..n-1));
  ensures \forall integer i; 0 <= i < n ==> dest[i] == \old(src[i]);
  assigns dest[0..n-1];
*/
void memcpy_safe(char *dest, const char *src, size_t n);

4. Assertions and Assumptions

Insert runtime and verification assertions:

//@ assert 0 <= index && index < array_length;
//@ assume divisor != 0;

5. Axiomatic Definitions and Predicates

Define reusable logical predicates and axioms:

/*@
  predicate sorted{L}(int *a, integer n) =
    \forall integer i, j; 0 <= i <= j < n ==> a[i] <= a[j];
*/

/*@
  axiomatic Sum {
    logic integer sum{L}(int *a, integer low, integer high);

    axiom sum_empty{L}:
      \forall int *a, integer i; sum(a, i, i) == 0;

    axiom sum_next{L}:
      \forall int *a, integer low, high;
        low < high ==> sum(a, low, high) == sum(a, low, high-1) + a[high-1];
  }
*/

Annotation Workflow

Step 1: Analyze the Function

Before annotating:

Identify inputs, outputs, and side effects
Determine memory access patterns
Understand algorithmic properties (sorting, searching, etc.)
Note any implicit assumptions

Step 2: Add Function Contract

Start with the function-level specification:

Preconditions (requires): What must be true when function is called
Postconditions (ensures): What will be true when function returns
Assigns clause: What memory locations may be modified
Behavioral specification: Normal and exceptional behaviors if applicable

Step 3: Annotate Loops

For each loop, specify:

Loop invariant: Properties that hold before and after each iteration
Loop variant: Decreasing measure proving termination
Loop assigns: Memory modified within the loop

Step 4: Add Assertions

Insert intermediate assertions to:

Document algorithmic properties
Help verification tools
Clarify complex logic

Step 5: Define Helper Predicates

Create reusable logical definitions for:

Common patterns (sorted arrays, valid ranges)
Domain-specific properties
Complex mathematical relationships

Common ACSL Constructs

Memory Validity

\valid(ptr)                    // Single valid pointer
\valid(ptr + (low..high))      // Valid range
\valid_read(ptr)               // Read-only validity
\separated(ptr1, ptr2)         // No aliasing

Quantifiers

\forall type var; condition ==> property
\exists type var; condition && property

Logic Functions

\old(expr)                     // Value at function entry
\at(expr, Label)               // Value at specific point
\result                        // Function return value
\nothing                       // Empty set (for assigns)

Integer Ranges

\forall integer i; low <= i < high ==> array[i] >= 0

Behaviors

/*@
  behavior valid_input:
    assumes n > 0;
    requires \valid(array + (0..n-1));
    ensures \result >= 0;

  behavior invalid_input:
    assumes n <= 0;
    ensures \result == -1;

  complete behaviors;
  disjoint behaviors;
*/

Verification Considerations

Show full SKILL.md (176 more words)Show less

For Frama-C WP Plugin

When generating annotations for WP verification:

Use assigns clauses to specify frame conditions
Prefer \valid over raw pointer checks
Use \separated for pointer disjointness
Add loop assigns for all loops
Include loop variant for termination proofs

Common Verification Patterns

Array bounds safety:

/*@ requires 0 <= index < length;
    requires \valid(array + index);
*/

Null pointer checks:

/*@ requires ptr != \null;
    requires \valid(ptr);
*/

Overflow prevention:

/*@ requires INT_MIN <= a + b <= INT_MAX; */

Output Format

Generate annotations in standard ACSL comment syntax:

Multi-line contracts: /*@ ... */
Single-line assertions: //@ assertion
Place contracts immediately before function declarations
Place loop annotations immediately before loop headers
Include explanatory comments when annotations are complex

Best Practices

Start simple: Begin with basic contracts, then refine
Be precise: Avoid over-specification or under-specification
Document assumptions: Make implicit assumptions explicit
Use predicates: Factor out common patterns
Test incrementally: Verify annotations with Frama-C as you go
Include rationale: Add comments explaining non-obvious specifications

Example: Complete Annotated Function

/*@
  predicate valid_array(int *a, integer n) =
    \valid(a + (0..n-1)) && n > 0;
*/

/*@
  requires valid_array(array, n);
  ensures \result >= 0 && \result < n;
  ensures \forall integer i; 0 <= i < n ==> array[\result] >= array[i];
  assigns \nothing;
*/
int find_max_index(int *array, int n) {
    int max_idx = 0;

    /*@
      loop invariant 0 <= i <= n;
      loop invariant 0 <= max_idx < n;
      loop invariant \forall integer k; 0 <= k < i ==>
                     array[max_idx] >= array[k];
      loop assigns i, max_idx;
      loop variant n - i;
    */
    for (int i = 1; i < n; i++) {
        if (array[i] > array[max_idx]) {
            max_idx = i;
        }
    }

    return max_idx;
}

Resources

This skill includes reference materials for ACSL:

references/

acsl_reference.md - Comprehensive ACSL syntax reference
common_patterns.md - Frequently used annotation patterns
frama_c_integration.md - Tips for using with Frama-C

Load these references as needed for detailed syntax information or advanced patterns.

Files

SKILL.md and 3 other files (references) in skills/acsl-annotation-assistant of ArabelaTso/Skills-4-SE.

SKILL.md
references/acsl_reference.md
references/common_patterns.md
references/frama_c_integration.md

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Acsl Annotation Assistant 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.

Acsl Annotation Assistant compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Acsl Annotation Assistant this skillArabelaTso/Skills-4-SE	253	—	~1.8k	Automated safety check: Pass	Apache-2.0	1 mo ago
Paddle BuildPaddlePaddle/Paddle	24k	—	~1k	Automated safety check: Pass	Apache-2.0	today
Fory Releaseapache/fory	4.6k	—	~2.9k	Automated safety check: Pass	Apache-2.0	yesterday
ONNX Runtime Shape Inference Safety Auditmicrosoft/onnxruntime	22k	—	~3.3k	Automated safety check: Pass	MIT	today
Code Audit3stoneBrother/code-audit	892	1 repos	~2.7k	Automated safety check: Pass	None	7 mo ago
Qt C++ Code Reviewx-tools-author/x-tools	1.1k	2 repos	~4.3k	Automated safety check: Pass	BSD-3-Clause	6 days ago

Similar skills

Paddle Build
PaddlePaddle/Paddle
A skill your agent uses when needing to compile, rebuild, or install Paddle from source after code changes.
24k GitHub stars~1k tokensUpdated today
AI & LLM EngineeringAuto-check passed
Fory Release
apache/fory
Prepare an Apache Fory release candidate from a clean release branch, including the version bump, RC tag, JVM staging, ASF source artifacts, SVN upload, and vote email.
4.6k GitHub stars~2.9k tokensUpdated yesterday
Auto-check passed
ONNX Runtime Shape Inference Safety Audit
microsoft/onnxruntime
Official
Finds and fixes out-of-range output writes in ONNX Runtime operator shape-inference functions where a getNumOutputs guard admits too few outputs.
22k GitHub stars~3.3k tokensUpdated today
SecurityAuto-check passed
Code Audit
3stoneBrother/code-audit
Professional code security audit skill covering 55+ vulnerability types.
892 GitHub starsUsed in 1 repo~2.7k tokens
SecurityAuto-check passed
Qt C++ Code Review
x-tools-author/x-tools
Read-only review of Qt6 C++ code that combines a deterministic lint script with six parallel analysis agents and reports only high-confidence issues.
1.1k GitHub starsUsed in 2 repos~4.3k tokens
DevelopmentAuto-check passed
Translation
doxygen/doxygen
Keeps all Doxygen and Doxywizard translations up to date across three mechanisms: translator C++ classes (src/translatorxx.h), Qt .ts locale files for the Doxywizard GUI (addon/doxywizard/i18n/)…
6.6k GitHub stars~5.2k tokensUpdated 9 days ago
Writing & ContentAuto-check passed

Questions about Acsl Annotation Assistant

What does Acsl Annotation Assistant do?

Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs. Acsl Annotation Assistant is an agent skill from ArabelaTso/Skills-4-SE. Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs.

When should I use Acsl Annotation Assistant?

Acsl Annotation Assistant fits situations like: working with formal verification; adding function contracts (requires/ensures); loop invariants; memory safety annotations.

How do I install Acsl Annotation Assistant in Claude Code?

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

How do I install Acsl Annotation Assistant in Codex?

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

Can I use Acsl Annotation Assistant 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 acsl-annotation-assistant -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/acsl-annotation-assistant, .gemini/skills/acsl-annotation-assistant, .github/skills/acsl-annotation-assistant and .opencode/skills/acsl-annotation-assistant in your project.

What does Acsl Annotation Assistant need to run?

SKILL.md names no scripts, command-line tools or credentials: Acsl Annotation Assistant is instructions for the agent only.

Does Acsl Annotation Assistant 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 Acsl Annotation Assistant 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 Acsl Annotation Assistant use?

Acsl Annotation Assistant 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 Acsl Annotation Assistant use?

About 1.8k tokens (SKILL.md is roughly 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 7.6k tokens, read only when the agent opens those files.

What are the alternatives to Acsl Annotation Assistant?

Skills that share tags, products or a category with Acsl Annotation Assistant: Paddle Build (PaddlePaddle/Paddle, 24k stars), Fory Release (apache/fory, 4.6k stars), ONNX Runtime Shape Inference Safety Audit (microsoft/onnxruntime, 22k stars) and Code Audit (3stoneBrother/code-audit, 892 stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Acsl Annotation Assistant?

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.

Install Acsl Annotation Assistant

Facts

At a glance

What it does

When your agent uses it

Example prompts

Workflow steps

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

ACSL Annotation Assistant

Core Capabilities

1. Function Contracts

2. Loop Annotations

3. Memory Safety Specifications

4. Assertions and Assumptions

5. Axiomatic Definitions and Predicates

Annotation Workflow

Step 1: Analyze the Function

Step 2: Add Function Contract

Step 3: Annotate Loops

Step 4: Add Assertions

Step 5: Define Helper Predicates

Common ACSL Constructs

Memory Validity

Quantifiers

Logic Functions

Integer Ranges

Behaviors

Verification Considerations

For Frama-C WP Plugin

Common Verification Patterns

Output Format

Best Practices

Example: Complete Annotated Function

Resources

references/

Files

Compare with similar skills

Similar skills

More from ArabelaTso/Skills-4-SE

Related

Questions about Acsl Annotation Assistant