diff --git a/Makefile b/Makefile
index 8f7ad37cba7477dadd34f187f655d02330d700cf..de002d3287462d7ba94b0a04550b67137987647a 100644
--- a/Makefile
+++ b/Makefile
@@ -53,4 +53,4 @@ release:
 	dune-release opam pkg
 	dune-release opam submit
 
-.PHONY: release clean clean doc view-doc promote test docker uninstall install all
+.PHONY: release clean doc view-doc promote test docker uninstall install all
diff --git a/doc/contents.rst b/doc/contents.rst
new file mode 100644
index 0000000000000000000000000000000000000000..daa46db69729e3f5b7d11b30c01926ca8b00c326
--- /dev/null
+++ b/doc/contents.rst
@@ -0,0 +1,10 @@
+Table of content
+================
+
+.. toctree::
+   :maxdepth: 2
+   :caption: Contents:
+
+   installation
+   usage
+   modules
diff --git a/doc/index.rst b/doc/index.rst
index c171f56e9dac4412ab9178bc28e58dd7a0c8e9ac..7a26e02ada6f54db0dce86889e8a1ab5b1a7fa87 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -4,17 +4,33 @@
    contain the root `toctree` directive.
 
 Welcome to Caisar's documentation!
-==================================
+**********************************
+
+CAISAR (Characterizing AI Safety And Robustness) is a platform
+under active development at CEA LIST, aiming to provide a
+wide range of features to characterize the robustness of
+artificial intelligence based software.
+It is available as a free software under the LGPLV2.1
+license. Code is hosted at
+https://git.frama-c.com/pub/caisar.
+
+You may browse the documentation for :ref:`installation` and :ref:`usage`.
+
+
+Content
+=======
 
 .. toctree::
    :maxdepth: 2
    :caption: Contents:
 
+   installation
+   usage
+   modules
+
 
 
 Indices and tables
 ==================
 
-* :ref:`genindex`
-* :ref:`modindex`
 * :ref:`search`
diff --git a/doc/installation.rst b/doc/installation.rst
new file mode 100644
index 0000000000000000000000000000000000000000..e914f07f416d3fa642677fc5c6ebf074eba9264a
--- /dev/null
+++ b/doc/installation.rst
@@ -0,0 +1,27 @@
+.. _installation:
+
+Installation
+============
+
+For now, no binaries are provided. Installation must be made
+directly by compiling the source.
+It requires Ocaml package manager Opam, v2.1 or higher.
+
+
+For development, it is recommended you set-up your own
+Opam switch (an OCaml installation isolated from system
+libraries)::
+
+  git clone https://git.frama-c.com/pub/laiser/caisar.git && cd caisar
+  opam switch create --yes --no-install . ocaml-base-compiler.4.13.1  
+
+Install external dependencies:::
+
+  opam depext --yes ocplib-endian base fmt alt-ergo.2.4.0  
+  opam install . --deps-only --with-test --yes  
+
+Finally, run the compilation and the unit tests:::
+
+  make  
+  make test  
+
diff --git a/doc/modules.rst b/doc/modules.rst
new file mode 100644
index 0000000000000000000000000000000000000000..1196f67e8c5dfb8364ee91f2d8a2e0c67ece9fde
--- /dev/null
+++ b/doc/modules.rst
@@ -0,0 +1,7 @@
+API documentation
+=================
+
+.. toctree::
+   :maxdepth: 4
+
+   nier_cfg
diff --git a/doc/usage.rst b/doc/usage.rst
new file mode 100644
index 0000000000000000000000000000000000000000..07606ae4920c770072607e49a5038451dd342845
--- /dev/null
+++ b/doc/usage.rst
@@ -0,0 +1,31 @@
+.. _usage:
+
+Usage
+=====
+
+Property verification
+---------------------
+
+CAISAR can be used to verify properties on neural networks.
+The prototype command is ``caisar verify --solver=SOLVER property.mlw``
+File property.mlw defines the goal you want to verify,
+written in the Whyml language.
+Example of .mlw files can be seen in tests folder.
+
+External verifiers detection
+----------------------------
+
+CAISAR relies on external verifiers to work. You must install
+them first, then point CAISAR to their location.
+To do so,
+use ``DIR=/path/to/solver/exec caisar config -d.``
+
+List of supported verifiers:
+
+* PyRAT
+* `Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_
+* `SAVer <https://github.com/abstract-machine-learning/saver>`_
+
+List of actively developed supports:
+
+* Tools that support SMTLIB as inputs: `Alt-Ergo <https://alt-ergo.ocamlpro.com/>`_, `Z3 <https://github.com/Z3Prover/z3/wiki>`_, `Colibri <https://colibri.frama-c.com/>`_