diff --git a/spec/changelog.tex b/spec/changelog.tex
index 4f0b57acda294ed0d2ee1ea0215735f792fb0845..aeec21900ec53a49aeeccefc07bdbef8e3fb6410 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,5 +1,13 @@
 \subsection*{Unreleased}
 
+Proof rules:
+\begin{itemize}
+  \item Addition of a section describing bitvector proofs.
+  \item Bitblasting rules: \proofRule{bitblast_extract},  \proofRule{bitblast_add},
+      \proofRule{bitblast_ult}.
+\end{itemize}
+
+\noindent
 Breaking changes:
 \begin{itemize}
   \item Allow arbitrary extra annotations in \texttt{assume} commands.