The Why3 Platform
=================

:Authors:
  François Bobot,
  Jean-Christophe Filliâtre,
  Claude Marché,
  Guillaume Melquiond,
  Andrei Paskevich

:Version: |version|, September 2025
:Copyright: 2010--2025 University Paris-Saclay, CNRS, Inria

.. _U3CAT: http://frama-c.com/u3cat/
.. _Hi-Lite: http://www.open-do.org/projects/hi-lite/
.. _BWare: https://anr.fr/Project-ANR-12-INSE-0010/
.. _ProofInUse: http://www.spark-2014.org/proofinuse
.. _CoLiS: http://colis.irif.univ-paris-diderot.fr/
.. _VOCal: https://github.com/ocaml-gospel/vocal/
.. _GOSPEL: https://github.com/ocaml-gospel/

This work has been partly supported by the `U3CAT`_ national ANR project
(ANR-08-SEGI-021-08), the `Hi-Lite`_ FUI project of the System\@tic
competitivity cluster, the `BWare`_ ANR project (ANR-12-INSE-0010), the
Joint Laboratory `ProofInUse`_ (ANR-13-LAB3-0007), the `CoLiS`_ ANR
project (ANR-15-CE25-0001), the `VOCaL`_ ANR project
(ANR-15-CE25-008), and the `GOSPEL`_ ANR project
(ANR-22-CE48-0013).

.. toctree::
   :maxdepth: 3
   :numbered:

   foreword
   starting
   whyml
   install
   manpages
   syntaxref
   input_formats
   vcgen
   exec
   itp
   api
   technical
   changes
   zebibliography
   genindex

.. * :ref:`genindex`
.. * :ref:`search`
.. * :ref:`modindex`
