How do I install the Frama C Proofreader skill?

Run npx skillmds@latest add sysprog21/frama-c-proofreader in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Frama C Proofreader safe to use?

This skill has not completed SkillMD's automated safety review yet. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Frama C Proofreader?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Frama C Proofreader free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Frama C Proofreader?

sysprog21 (@sysprog21) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Frama C Proofreader by sysprog21 — Agent Skill

Name: Frama C Proofreader
Author: sysprog21

Frama C Proofreader

Verify and proofread C code with ACSL using this repository's Frama-C MCP workflow, Frama-C WP static proof, EVA alarms, and optional E-ACSL runtime checks. Use when asked to run Frama-C, check ACSL contracts, explain WP goals, inspect EVA alarms, validate C annotations, or state what a C proof does and does not establish.

sysprog21 e3b890b 9 files · 9.8 KB Updated Sep 17, 2026

File contents

Frama-C Proofreader

Workflow

Prefer the MCP server when it is available. Start with the install check and the shortest useful call:

self_check {}
reload_project {files, rte: true}
check {function?, timeout?}

If check reports alarms or non-valid goals, inspect the concrete payload before changing code:

get_eva_alarms {function?, status?}
investigate_alarm {property_key, depth}
get_wp_goals {function, status?}
get_wp_goals {function, detail: true}
context {function, want: ["current_annotations", "function_ast"]}

Validate candidate ACSL with dry-run injection first:

inject_all_annotations {function, dry_run: true, annotations: [{kind, acsl, ...}]}
inject_all_annotations {function, annotations: [{kind, acsl, ...}]}
run_wp {functions: [function]}

Use run_e_acsl only as runtime evidence for concrete executions. If it is unavailable or fails to compile instrumentation, report that runtime checking was unavailable.

Read references/mcp-workflow.md for the full MCP call order, references/wp-output.md when interpreting WP goals, and references/e-acsl-output.md before making runtime-check claims.

Reporting

Always separate these outcomes:

Environment failure: tool missing, prover not configured, instrumentation failed.
Static proof gap: WP did not prove a goal; this is not automatically a bug.
Runtime violation: E-ACSL found a violation on an executed path.
Proven under assumptions: WP proved the generated goals for the ACSL and RTE configuration that actually ran.

Do not claim proof without tool output. Report exact goal names, proof counts, and whether rte: true or -wp-rte was used.

Boundaries

WP proves obligations generated from the C program and ACSL. It does not prove requirements that were omitted from the specification.

EVA alarms and WP goals are complementary. A clean WP result does not replace checking missing frame conditions or assumed callee contracts.

E-ACSL checks only executed paths and inputs. Passing one run is evidence, not exhaustive proof.

---name: frama-c-proofreaderdescription: Verify and proofread C code with ACSL using this repository's Frama-C MCP workflow, Frama-C WP static proof, EVA alarms, and optional E-ACSL runtime checks. Use when asked to run Frama-C, check ACSL contracts, explain WP goals, inspect EVA alarms, validate C annotations, or state what a C proof does and does not establish.---# Frama-C Proofreader## WorkflowPrefer the MCP server when it is available. Start with the install check and the shortest useful call:```textself_check {}reload_project {files, rte: true}check {function?, timeout?}```If `check` reports alarms or non-valid goals, inspect the concrete payload before changing code:```textget_eva_alarms {function?, status?}investigate_alarm {property_key, depth}get_wp_goals {function, status?}get_wp_goals {function, detail: true}context {function, want: ["current_annotations", "function_ast"]}```Validate candidate ACSL with dry-run injection first:```textinject_all_annotations {function, dry_run: true, annotations: [{kind, acsl, ...}]}inject_all_annotations {function, annotations: [{kind, acsl, ...}]}run_wp {functions: [function]}```Use `run_e_acsl` only as runtime evidence for concrete executions. If it is unavailable or fails to compile instrumentation, report that runtime checking was unavailable.Read `references/mcp-workflow.md` for the full MCP call order, `references/wp-output.md` when interpreting WP goals, and `references/e-acsl-output.md` before making runtime-check claims.## ReportingAlways separate these outcomes:- Environment failure: tool missing, prover not configured, instrumentation failed.- Static proof gap: WP did not prove a goal; this is not automatically a bug.- Runtime violation: E-ACSL found a violation on an executed path.- Proven under assumptions: WP proved the generated goals for the ACSL and RTE configuration that actually ran.Do not claim proof without tool output. Report exact goal names, proof counts, and whether `rte: true` or `-wp-rte` was used.## BoundariesWP proves obligations generated from the C program and ACSL. It does not prove requirements that were omitted from the specification.EVA alarms and WP goals are complementary. A clean WP result does not replace checking missing frame conditions or assumed callee contracts.E-ACSL checks only executed paths and inputs. Passing one run is evidence, not exhaustive proof.

Frequently asked questions