gnatprove

name	gnatprove
description	This skill should be used when the user wants to "prove SPARK code", "run GNATprove", "investigate unproved checks", "write contracts or invariants", "add loop invariants", "write ghost code or lemmas", or is working on SPARK formal verification. Covers running gnatprove, writing SPARK (contracts, types, loops, ghost code), and conducting proof campaigns.
license	Apache-2.0
metadata	{"version":"0.2.0"}

gnatprove

gnatprove 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 ...".

Locating gnatprove

Unless the user has already told you how to invoke gnatprove, determine the right invocation in this order:

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

2. 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).

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.

Quick Start

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:

• Scoped runs (--limit-subp, --limit-line): minimum 300000ms (5 min)
• Whole-unit or whole-program runs: 600000ms (10 min) or more

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)
• Generics need -U: to scope --limit-subp/--limit-line to a subprogram inside a generic (analysed only through instantiations), add -U (analyse all units in the project). Without it you get warning: no checks generated by GNATprove. -U runs the whole project, so expect unrelated warnings/checks from other units — filter to the file/line you care about and ignore the rest.
• --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:

1. Information about gnatprove's phase of operation. When there are errors, knowing where gnatprove stopped is helpful.
2. Warnings and check messages. These tell you about flow or proof problems.
3. Summary. 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.

Beware the difference between proved and not analyzed. warning: no checks generated by GNATprove (or a suspiciously low check count) means code you expected to verify was skipped — not that it is correct. This bites with generic instantiations: a library-level package P is new G (...); defaults to SPARK_Mode off and its body's VCs are silently never generated, so add with SPARK_Mode => On; to it. Run scoped to the unit (-u file) to surface per-unit warnings. See gnatprove.md § "absence of error or check messages".

Use Cases

There are three broad use cases for this skill.

1. Working with gnatprove. Invoking the tool, CLI options, interpreting output. Read gnatprove.md
2. Writing SPARK. Contracts, types, access types, loops, ghost code and lemmas. Read spark.md
3. Proving SPARK with gnatprove. Proof campaigns, debugging proof failures, improving provability. Read proof.md