Minor tweaks to the abstract.

paper/0_abstract.tex

 % \subsection*{Abstract}
 \begin{abstract}
+  We formally prove that the C implementation of
+  the X25519 key-exchange protocol
+  in the TweetNaCl library is correct.
+  We prove both that it correctly implements the protocol from
+  Bernstein's 2006 paper, as standardized in RFC~7748,
+  well as the absence of undefined behavior
+  like arithmetic overflows
+  and array out of bound errors.
+  We also formally prove, based on the work of Bartzia and Strub,
+  that X25519 is mathematically correct, i.e.,
+  that it correctly computes scalar multiplication on 
+  the elliptic curve Curve25519.
 
-We formally prove that the C implementation of
-the X25519 key exchange protocol
-in the TweetNaCl library is correct.
-We prove both that it correctly implements the protocol from
-Bernstein's 2006 paper, as standardized in RFC 7748,
-as well that there are no undefined behaviors
-like arithmetic overflows
-and array out of bound errors.
-We also formally prove, based on the work of Bartzia and Strub,
-that X25519 is mathematically correct
-in that it correctly computes multiplication in the elliptic curve 
-Curve25519.
-
-The proofs are all computer-verified using the Coq theorem prover.
-To establish the link between C and Coq we use the 
-Verified Software Toolchain (VST).
-
+  The proofs are all computer-verified using the Coq theorem prover.
+  To establish the link between C and Coq we use the 
+  Verified Software Toolchain (VST).
 \end{abstract}