Add README

README.md

+The Proof Format -- Speculative Specification
+=============================================
+
+This repository hosts a specification of the proof format used by veriT
+right now.  It will also soon be available on CVC5.
+
+Right now the specification is speculative: rather than being cast
+in stone, it will improve as solvers, proof reconstructions, and
+tools develop.  Our approach is pragmatic.  We refine the format
+and especially the rules as we gather experience.
+
+## Building the Specifications
+
+The specification are in the folder `spec`.  The main source file is the
+`doc.tex` file.
+
+Syntax highlighting uses the `pygments` tool.  Hence, this tool must
+be installed.  Furthermore, Latex must be compiled with shell escaping
+allowed.  To do this the argument `-shell-escape` must be given to the
+Latex command. `latexmk` also accepts this argument and hands it to Latex.