diff --git a/doc/genindex.rst b/doc/genindex.rst
new file mode 100644
index 0000000000000000000000000000000000000000..6b82d211189bd8ee39eb91553e5986dc0b996c8b
--- /dev/null
+++ b/doc/genindex.rst
@@ -0,0 +1,8 @@
+:orphan:
+
+.. dummy file so that an "index" entry appears in the sidebar
+
+.. only:: html
+
+   Index
+   =====
diff --git a/doc/index.rst b/doc/index.rst
index 5c99e5fbb42f7d00c02b6451fc5b776410ecd321..6bc69d14bca6d3dc061625a7539a23ff886b6aa2 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -6,72 +6,35 @@
 .. _index:
 
 The CAISAR Platform
-====================
+===================
 
 .. image:: _static/media/caisar_logo.png
+   :scale: 50 %
+   :alt: The CAISAR logo
+   :align: center
 
-*version:* |version|
+:Authors:
+  Michele Alberti,
+  François Bobot,
+  Julien Girard
 
-CAISAR is an open-source platform for the Characterization of Artificial
-Intelligence Safety And Robustness. Its expressive modelling language allows the
-description of a wide variety of specifications to enforce on a machine learning
-system. The specification is then decomposed into subproblems that are then sent
-to specialized provers. CAISAR aims to be component-agnostic: it can model and
-assess the trustworthiness of an hybrid artificial intelligence system that
-mixes symbolic and data-driven approaches.
+:Version: |version|, December 2022
+:Copyright: 2020--2022 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
 
-It is available as a free software under the LGPLV2.1 license. The code is
-hosted in our `GitLab instance <https://git.frama-c.com/pub/caisar>`_.
+.. _Confiance.ai: https://www.confiance.ai/
 
-Architecture and components
----------------------------
-
-CAISAR relies on the `Why3 verification platform <https://why3.lri.fr/>`_ to
-provide both the basis of the specification language (WhyML), and an
-intermediate representation of logical formulas and goals.
-
-CAISAR supports the verification of multiple machine learning models. Neural
-Network (NN) are handled through the `ONNX exchange format <https://onnx.ai/>`_.
-Support Vector Machines (SVM) are supported through an ad-hoc CSV format.
-Gradient boosting models and decision trees will soon be supported.
-
-.. _supported_provers:
-
-Provers
--------
-
-CAISAR heavily relies on external software to provide answers on proof
-obligations. Those programs are called *provers*, altough some of them may not
-directly provide a logical proof.
-
-The supported provers are the following:
-
-* `PyRAT <https://laiser.frama-c.com/laiser-websites/pyrat-website/>`_,
-  a neural network verifier powered by abstract interpretation (some developers of CAISAR are also working on PyRAT)
-* `Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_, a
-  Satisfiability Modulo Theory (SMT) solver specialized in Neural Network
-  verification
-* `SAVer <https://github.com/abstract-machine-learning/saver>`_, a tool for
-  verifying reachability properties on SVM
-* `nnenum <https://github.com/stanleybak/nnenum>`_
-* "Traditional" SMT solvers that support SMT-LIBv2 input language (including
-  `Alt-Ergo <https://alt-ergo.ocamlpro.com/>`_, `Z3
-  <https://github.com/Z3Prover/z3/wiki>`_, `Colibri
-  <https://colibri.frama-c.com/>`_)
-
-If you would like for CAISAR to support a tool you are
-developping, please reach out so we can discuss about it!
-
-Browse the documentation
-------------------------
-
-Installation instructions for CAISAR are available at :ref:`installation`.
-A description of core usage is available at :ref:`usage`.
-Finally, we provide some :ref:`examples` as well.
+This work has been partly supported by the `Confiance.ai`_ program.
 
 .. toctree::
    :maxdepth: 3
+   :numbered:
 
+   foreword
    installation
    usage
    examples
+   genindex
+
+.. * :ref:`genindex`
+.. * :ref:`search`
+.. * :ref:`modindex`