diff --git a/index.html b/index.html
index ed90894..2b2354e 100644
--- a/index.html
+++ b/index.html
@@ -233,8 +233,12 @@ <h2>Publications</h2>
 <p>
 Diego Ongaro's
 <a href="https://github.com/ongardie/dissertation#readme">Ph.D. dissertation</a>
-expands on the content of the paper in much more detail, and
-it includes a simpler cluster membership change algorithm.
+expands on the content of the paper in much more detail, and it includes a
+simpler cluster membership change algorithm. The dissertation also includes a
+formal specification of Raft written in TLA+; a slightly updated version of that
+specification is <a href="https://github.com/ongardie/raft.tla">here</a>.
+</p>
+
 </p>
 
 <p>More Raft-related papers:</p>
@@ -301,16 +305,6 @@ <h2>Publications</h2>
   </li>
 </ul>
 
-<a name="spec"></a>
-<h2>Formal specification</h2>
-
-<p>
-This is TLA+ specification for the Raft consensus algorithm, which
-describes Raft in detail: <a href="https://github.com/ongardie/raft.tla">ongardie/raft.tla</a>
-by <a href="https://twitter.com/ongardie">Diego Ongaro</a>. This is slightly
-updated compared to the dissertation version.
-</p>
-
 <a name="talks"></a>
 <h2>Talks</h2>