.. _Formal Verification with GNATprove:

************************************
Formal Verification with |GNATprove|
************************************

The |GNATprove| tool is packaged as an executable called ``gnatprove``. Like
other tools in |GNAT Pro| toolsuite, |GNATprove| is based on the structure of
GNAT projects, defined in ``.gpr`` files.

A crucial feature of |GNATprove| is that it interprets annotations exactly like
they are interpreted at run time during tests. In particular, their executable
semantics includes the verification of run-time checks, which can be verified
statically with |GNATprove|. |GNATprove| also performs additional verifications
on the specification of the expected behavior itself, and its correspondence to
the code.

.. only : : core

   .. toctree::
      :maxdepth: 2

      source/how_to_run_gnatprove
      source/how_to_view_gnatprove_output
      source/how_to_use_gnatprove_in_a_team
      source/how_to_investigate_unproved_checks

.. only:: full

   .. toctree::
      :maxdepth: 2

      source/how_to_run_gnatprove
      source/how_to_view_gnatprove_output
      source/how_to_use_gnatprove_in_a_team
      source/how_to_write_subprogram_contracts
      source/how_to_write_object_oriented_contracts
      source/how_to_write_package_contracts
      source/how_to_write_loop_invariants
      source/how_to_investigate_unproved_checks
      source/gnatprove_by_example
