Claude Skill MartBrowse skillsQuick linesLearn by videoTerminal guideWhat is a Skill?
 
← Back to list

ACSL Annotation Assistant

Generates ACSL formal specifications — function contracts, loop invariants and memory-safety clauses — for C/C++ code so it can be proven with Frama-C.

Dev & CodingAdvanced★ 248⑂ 23AI score 7/10Last updated: Aug 21, 2026

What it does

  • Writes ACSL function contracts using requires / ensures / assigns.
  • Produces loop invariants, decreasing loop variant for termination, and loop assigns.
  • Adds memory-safety specs: \valid, \valid_read, \separated, null-pointer and overflow preconditions.
  • Defines reusable predicates and axiomatic blocks, and inserts intermediate assert / assume.
  • Follows a 5-step workflow: analyze function → contract → loops → assertions → helper predicates.
  • Ships a references/ folder with an ACSL syntax reference, common patterns, and Frama-C integration tips.

Who it's for

  • Engineers and researchers verifying C code with the Frama-C WP plugin.
  • High-integrity embedded teams (avionics, automotive, medical) needing certification evidence.
  • Anyone who wants array-bounds, null-pointer and overflow safety proven rather than tested.
  • Students and instructors in formal-methods courses who need specs drafted quickly.

Examples

  1. "Annotate find_max_index with a contract and loop invariants" → postconditions capturing the maximum-element property.
  2. "Add memory-safety specs to my memcpy wrapper" → \valid, \valid_read, \separated, and an assigns clause.
  3. "Split n <= 0 and n > 0 into ACSL behaviors" → a spec with complete behaviors; disjoint behaviors;.

· · · Install guide · · ·

Try it now, no install

Paste this into Claude to use the skill without installing anything.

Read the instructions in this file and follow them to help me:
https://raw.githubusercontent.com/ArabelaTso/Skills-4-SE/HEAD/skills/acsl-annotation-assistant/SKILL.md

What I want: (describe your task here)

If Claude can't open the link, open it yourself and paste the contents instead.

↓ If it works for you, download the ZIP below and install it. Then it runs on its own — no pasting each time.

Install in the Claude app (no terminal)
  1. Download the ZIP with the button below.
  2. In Claude, open Settings → Capabilities and turn on 'Code execution and file creation'. (one time)
  3. Go to Customize → Skills → + → 'Upload a skill' and upload the ZIP.
↓ Download ZIP
Install in Claude Code

Let Claude do it — paste this into Claude Code

Install the skill I found on Claude Skill Mart.
Copy the skills/acsl-annotation-assistant folder from the GitHub repo ArabelaTso/Skills-4-SE into my ~/.claude/skills/acsl-annotation-assistant/.
When it's done, tell me in one line what this skill can do.

Install with a command instead

git clone https://github.com/ArabelaTso/Skills-4-SE.git /tmp/skills-4-se && mkdir -p ~/.claude/skills && cp -r /tmp/skills-4-se/skills/acsl-annotation-assistant ~/.claude/skills/

⚠ This is a third-party skill. Check the source repository before installing.

  1. Open a terminal and clone the repo: git clone https://github.com/ArabelaTso/Skills-4-SE.git
  2. Create the skills folder if needed: mkdir -p ~/.claude/skills
  3. Copy just this skill: cp -r Skills-4-SE/skills/acsl-annotation-assistant ~/.claude/skills/
  4. Verify with ls ~/.claude/skills/acsl-annotation-assistant — you should see SKILL.md and references/.
  5. Restart Claude Code, then ask something like "add ACSL annotations to this C function".
  6. (Recommended) Install Frama-C to actually verify: brew install frama-c on macOS, sudo apt install frama-c on Ubuntu.
  7. Run frama-c -wp your_file.c and iterate on any clause the prover cannot discharge.
View source on GitHub ↗License: Apache-2.0