--- 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 ...` 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. ```bash gnatprove -P -j0 --output=oneline --output-header 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](references/gnatprove/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`) - `--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. ## 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](references/gnatprove/gnatprove.md) 2. **Writing SPARK.** Contracts, types, access types, loops, ghost code and lemmas. Read [spark.md](references/spark/spark.md) 3. **Proving SPARK with `gnatprove`.** Proof campaigns, debugging proof failures, improving provability. Read [proof.md](references/proof/proof.md)