acsl-annotation-assistant
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.
Install with Tessl CLI
npx tessl i github:ArabelaTso/Skills-4-SE --skill acsl-annotation-assistant89
Does it follow best practices?
If you maintain this skill, you can automatically optimize it using the tessl CLI to improve its score:
npx tessl skill review --optimize ./path/to/skillValidation for skill structure
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly defines a specialized niche (ACSL formal annotations for C/C++ verification). It provides comprehensive trigger terms covering the domain vocabulary, explicitly states when to use the skill, and lists concrete capabilities. The technical specificity ensures it won't conflict with general programming skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Create ACSL formal annotations', 'adding function contracts (requires/ensures)', 'loop invariants', 'assertions', 'memory safety annotations'. These are precise, technical capabilities. | 3 / 3 |
Completeness | Clearly answers both what ('Create ACSL formal annotations for C/C++ programs') and when ('Use this skill when working with formal verification, adding function contracts...'). Has explicit 'Use this skill when' clause with specific trigger scenarios. | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural terms users would say: 'ACSL', 'formal verification', 'function contracts', 'requires/ensures', 'loop invariants', 'assertions', 'memory safety', 'Frama-C', 'C/C++'. These are the exact terms someone working in this domain would use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche - ACSL and Frama-C are very specific tools for formal verification of C code. Unlikely to conflict with general C/C++ coding skills or documentation skills due to the specialized terminology. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
72%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a strong skill with excellent actionability - all ACSL examples are complete and executable. The progressive disclosure is well-handled with clear section organization and external references. Main weaknesses are moderate verbosity (some redundant construct explanations) and missing explicit validation steps in the workflow for verifying annotations with Frama-C before proceeding.
Suggestions
Integrate Frama-C verification commands directly into the workflow steps (e.g., 'Step 6: Verify with `frama-c -wp file.c` - if errors, review and fix annotations before proceeding')
Remove or consolidate the 'Common ACSL Constructs' section since most constructs are already demonstrated in the capability examples above
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is generally efficient but includes some redundancy - the 'Common ACSL Constructs' section repeats concepts already demonstrated in examples, and some explanatory text like 'Before annotating:' lists could be tightened. The workflow section adds value but could be more concise. | 2 / 3 |
Actionability | Excellent executable examples throughout - all code snippets are complete, copy-paste ready ACSL annotations with proper syntax. The complete annotated function example at the end demonstrates real-world application with all annotation types integrated. | 3 / 3 |
Workflow Clarity | The 5-step annotation workflow is clearly sequenced, but lacks explicit validation checkpoints. Step 5 mentions 'Test incrementally: Verify annotations with Frama-C as you go' only in best practices, not integrated into the workflow with specific commands or error recovery guidance. | 2 / 3 |
Progressive Disclosure | Well-structured with clear sections progressing from core capabilities to workflow to reference constructs. References to external files (acsl_reference.md, common_patterns.md, frama_c_integration.md) are clearly signaled at the end with one-level-deep navigation. | 3 / 3 |
Total | 10 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
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.