Part of the Hi-Lite project, GNATprove is a formal verification tool for Ada, based on the GNAT compiler, Why3 platform and Alt-Ergo prover. It can prove that subprograms respect their contracts, expressed as preconditions and postconditions in the syntax of Ada 2012. The tool automatically discovers the subset of subprograms which can be formally analyzed. GNATprove is currently available for x86 linux, x86 windows and x86-64 linux.

You should first install GNAT GPL 2012, and then GNATprove at the same location. Under Linux, put the path "your location"/bin in your PATH variable. Under Windows, the installation takes care of this step.

To use the integration of GNATprove in GPS, download the GNATprove plug-in and copy it either in the share/gps/plug-ins/ subdirectory of your GPS installation, or in $HOME/.gps/plug-ins (where $HOME is your home directory).

See GNATprove in action inside GNAT Programming Studio

• On Windows, GNATprove only works when applied to projects under the C: drive.

For questions, remarks, problems, please contact us on

Learn More about Project Hi-Lite