GNATprove, which provides automatic formal verification of SPARK code, is based on the open-source SPARK Pro by AdaCore. The SPARK Pro User’s Guide provides extensive documentation on how to use GNATprove. Note that because this version of GNATprove is built from an intermediate commit of SPARK Pro, it is not representative of any specific SPARK Pro release, and the SPARK Pro documentation may describe features or capabilities that are not yet available in this version of GNATprove.

To use GNATprove, simply add it to your Alire project using

alr with gnatprove

Then, configure your environment by running:

eval "$( alr printenv )"

You will then be able to run GNATprove:

gnatprove

For more details on getting started using GNATprove, see Getting Started with SPARK from the SPARK Pro User’s Guide.

To get started with the SPARK language, see the Introduction to SPARK course on learn.adacore.com.