diff --git a/docs/iris.tex b/docs/iris.tex
index ca5b8ff168a3ca08831fc40d54bc08451f6524f3..4813b2701d568ce4d350f269b1f7fe1c796308d5 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -15,15 +15,24 @@
 
 \input{setup}
 
-\begin{document}
 
 \title{\bfseries The Iris 2.0 Documentation}
 \author{\url{http://plv.mpi-sws.org/iris/}}
-\maketitle
 
-\thispagestyle{empty}
 
-%\clearpage
+\begin{document}
+
+\maketitle
+\thispagestyle{empty}
+\vfill
+\begin{abstract}
+This document describes formally the Iris program logic.
+Every result in this document has been fully verified in Coq.
+The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/FP/iris-coq/}.
+For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
+\end{abstract}
+
+\clearpage
 \tableofcontents
 
 \clearpage\begingroup