diff --git a/doc/verification.rst b/doc/verification.rst
index 0e63a08684234d3e5360656c415bcc87825d045d..c89ad9136a4f2bd2bfb7ffe2302da3dfbd82591a 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -1,2 +1,42 @@
 Verification
 ============
+
+Software verification aims at making software safer. In its typical use case,
+it is a tool that takes as input the source code of a program with
+specifications as annotations and attempt to prove --- or disprove --- their
+validity.
+
+One of the core module of Leon is a verifier for the subset of Scala described
+in the sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`. In this
+section we describe the specification language that can be used to declare
+properties of programs, as well as the safety properties automatically checked
+by Leon. We also discuss how Leon can be used to prove mathematical theorems.
+
+Verification conditions
+-----------------------
+
+
+
+Postconditions
+**************
+
+
+Preconditions
+*************
+
+
+Loop invariants
+***************
+
+
+Array access safety
+*******************
+
+
+Pattern matching exhaustiveness
+*******************************
+
+
+
+Proving mathematical theorems with Leon
+---------------------------------------