From adacore
Proves SPARK code with gnatprove: checks validity, analyzes data flows, and runs proof campaigns. Covers writing contracts, invariants, and ghost code.
How this skill is triggered — by the user, by Claude, or both
Slash command
/adacore:gnatproveThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
`gnatprove` is the tool that checks the validity of, analyzes data flows for,
README.mdreferences/gnatprove/command-reference.mdreferences/gnatprove/gnatprove-out.mdreferences/gnatprove/gnatprove.mdreferences/proof/floating-point.mdreferences/proof/loops.mdreferences/proof/overflow-patterns.mdreferences/proof/proof-debugging.mdreferences/proof/proof.mdreferences/proof/refactoring-for-proof.mdreferences/proof/workflow-subagent.mdreferences/proof/workflow.mdreferences/spark/access-types.mdreferences/spark/contracts.mdreferences/spark/ghost-code-and-lemmas.mdreferences/spark/idioms.mdreferences/spark/spark.mdgnatprove is the tool that checks the validity of, analyzes data flows for,
and proves SPARK code. SPARK is a subset of Ada (it restricts the use of
certain Ada features) and a superset of Ada (it offers some aspects that
extend the semantics of the Ada language).
Note: when a user says "SPARK", they may be talking about either the language
or gnatprove. This should be clear from context. E.g., "Run SPARK and ..."
means "Run gnatprove and ..."; "Update the SPARK to ..." means "Update the
SPARK source code to ...".
Unless the user has already told you how to invoke gnatprove, determine the right invocation in this order:
Check for an alire.toml in the project root. Its presence means the project
is an Alire crate; use alr gnatprove -P <project.gpr> ... rather than bare
gnatprove. Alire computes and injects the correct environment (including
GPR_PROJECT_PATH for multi-crate projects) before calling gnatprove, so this
is the correct invocation for Alire-managed projects even when gnatprove is
also on PATH.
Check if gnatprove is already on PATH. Run which gnatprove. If found,
use it — but if proof runs fail with project-file resolution errors, the
environment may be incomplete (see step 3).
Ask the user. SPARK Pro installations (commonly under /usr/gnat or
/opt/gnat) typically require environment setup beyond a binary path. If
gnatprove is not on PATH and there's no alire.toml, don't guess — ask the
user how they want to configure the environment.
To prove SPARK code, run GNATprove via Bash with the project's environment.
gnatprove -P <project.gpr> -j0 --output=oneline --output-header <arguments> 2>&1 | tee gnatprove-run.txt
--output-header is mandatory on every invocation. It writes a header into
gnatprove.out recording the exact command line, gnatprove version, host, and
timestamp. This is how a reader — a returning user, or the main agent
verifying a subagent's run — confirms how gnatprove was invoked without
guessing or asking. See gnatprove-out.md § Invocation header.
Never run two gnatprove instances concurrently. gnatprove assumes
exclusive ownership of its output directories; parallel runs corrupt results.
Bash tool timeout: gnatprove can take tens of minutes — there is no way to
predict duration in advance. Always set a large timeout on the Bash tool call:
--limit-subp, --limit-line): minimum 300000ms (5 min)Common arguments:
-jN (where 0 means as many threads as possible and N>0 means use that many
parallel threads)--level=1 (proof level 0-4; start low, increase only if needed; never use
3 or 4 without user approval)--limit-subp=file.adb:NN (prove one subprogram; NN = declaration line,
not body. Line numbers shift after any edit; always confirm you have the
right NN)--limit-line=file.adb:MM (prove exactly one check; assumes assertions
above. Line numbers shift after any edit; always confirm you have the right
MM)--output=oneline (one check per line; good for status assessment)--output-header (write invocation header into gnatprove.out; mandatory)-f (force full reanalysis)Note: with --limit-subp or --limit-line, the filename must NOT include
the src/ prefix -- the GPR file handles source directories.
Piping through tee saves output to gnatprove-run.txt so you can re-filter
it (grep, etc.) without re-running.
Important: Never re-run gnatprove solely to re-examine output.
A re-run without a code or contract change produces the same result at
significant cost. Even should gnatprove time out but produce output,
work with that output — a partial run is still useful and re-running would
violate the no-redundant-runs rule. Only re-run with a larger timeout if the
run produced no output at all. Note the timeout for future runs. Never rely
on the default 120s timeout.
gnatprove's output is all meaningful, and breaks into three parts:
gnatprove's phase of operation. When there are errors,
knowing where gnatprove stopped is helpful.gnatprove tells you the location of gnatprove.out. Newer
versions of gnatprove will print a success message when all checks are
proved.gnatprove check messages may be low, medium or high - these reflect
confidence that the check is a true positive. high check messages should be
treated as errors.
gnatprove's exit code does not tell you if all checks are proved. You know
all checks are proved when there are no warning or check messages.
There are three broad use cases for this skill.
gnatprove.
Invoking the tool, CLI options, interpreting output.
Read gnatprove.mdgnatprove.
Proof campaigns, debugging proof failures, improving provability.
Read proof.mdProvides behavioral guidelines to reduce common LLM coding mistakes, focusing on simplicity, surgical changes, assumption surfacing, and verifiable success criteria.
Searches, retrieves, and installs Agent Skills from prompts.chat registry using MCP tools like search_skills and get_skill. Activates for finding skills, browsing catalogs, or extending Claude.
Creates, edits, and optimizes skills for Claude Code, including drafting, evaluating with test prompts, iterating on performance, and improving skill descriptions for better triggering accuracy.
npx claudepluginhub adacore/skills --plugin adacore