diff --git a/reports/ref.bib b/reports/ref.bib
index 4c55b83..ea21f4e 100644
--- a/reports/ref.bib
+++ b/reports/ref.bib
@@ -44,6 +44,14 @@ @misc{tla-examples
   note         = {Accessed: 2024-10-25}
 }
 
+@misc{tla-paxos,
+  title = { {TLA}$^+$ specification of {Paxos} },
+  author = { Leslie Lamport },
+  howpublished = {\url{https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla}},
+  year         = 2024,
+  note         = {Accessed: 2024-12-17}
+}
+
 @article{DBLP:journals/lmcs/BansalBRT18,
   author       = {Kshitij Bansal and
                   Clark W. Barrett and
diff --git a/reports/spec4b.tex b/reports/spec4b.tex
index 30232ae..91f3341 100644
--- a/reports/spec4b.tex
+++ b/reports/spec4b.tex
@@ -37,7 +37,7 @@ \subsection{Constraints over set cardinalities}
 \cdot T + 1$ set elements to show that Equation~(\ref{eq:card-comparison2})
 holds true. This gives us a linear number of constraints, instead of a
 quadratic one. For example, when $T=1$ and the set may contain up to~$n$
-elements, the model checker produces $3 \cdot O(n)$ constraints to check
+elements, the model checker produces $O(n)$ constraints to check
 Equation~(\ref{eq:card-comparison2}). A similar optimization is used in the
 specification of Tendermint~\cite{TendermintSpec2020}.
 
@@ -45,10 +45,7 @@ \subsection{Quorum sets}
 
 To further optimize the constraints over set cardinalities, we have applied the
 well-known pattern of replacing cardinality tests with quorum sets. For
-example, this approach is used in the specification of Paxos\footnote{%
-    \tlap{} specification of Paxos:
-\url{https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla}.}
-
+example, this approach is used in the specification of Paxos~\cite{tla-paxos}.
 To this end, we introduce quorum sets such as in Figure~\ref{fig:quorum-sets}.
 
 \begin{figure}[!h]