diff --git a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex
index 802ce565204..ff470bb7585 100644
--- a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex
+++ b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex
@@ -63,6 +63,8 @@
 \newcommand{\ProtVer}{\ensuremath{\type{ProtVer}}}
 \newcommand{\ApName}{\ensuremath{\type{ApName}}}
 \newcommand{\ApVer}{\ensuremath{\type{ApVer}}}
+\newcommand{\SystemTag}{\ensuremath{\type{SystemTag}}}
+\newcommand{\UpdateData}{\ensuremath{\type{UpdateData}}}
 \newcommand{\Metadata}{\ensuremath{\type{Mdt}}}
 \newcommand{\PPUpdate}{\type{PPUpdate}}
 \newcommand{\Applications}{\type{Applications}}
diff --git a/shelley/chain-and-ledger/formal-spec/transactions.tex b/shelley/chain-and-ledger/formal-spec/transactions.tex
index 312da654a68..336586346fa 100644
--- a/shelley/chain-and-ledger/formal-spec/transactions.tex
+++ b/shelley/chain-and-ledger/formal-spec/transactions.tex
@@ -44,7 +44,8 @@ \section{Transactions}
     \begin{array}{r@{~\in~}lr}
       \var{txid} & \TxId & \text{transaction id}\\
       \var{an} & \ApName & \text{application name}\\
-      \var{m} & \Metadata & \text{metadata}\\
+      \var{st} & \SystemTag & \text{system tag}\\
+      \var{ud} & \UpdateData & \text{update data}\\
     \end{array}
   \end{equation*}
   \emph{Derived types}
@@ -81,6 +82,11 @@ \section{Transactions}
       & \N
       & \text{application versions}
       \\
+      \var{md}
+      & \Metadata
+      & \SystemTag\mapsto\UpdateData
+      & \text{application metadata}
+      \\
       \var{apps}
       & \Applications
       & \ApName \mapsto (\ApVer \times \Metadata)
diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex
index d3414e795b6..aab9fc9546b 100644
--- a/shelley/chain-and-ledger/formal-spec/update.tex
+++ b/shelley/chain-and-ledger/formal-spec/update.tex
@@ -14,8 +14,9 @@ \section{Updates}
 Therefore $\mathsf{UPDATE}$ is the combination of the
 $\mathsf{PPUP}$ transition for the protocol parameters and the
 the $\mathsf{AVUP}$ transition for the application versions.
-Recall that $\PPUpdate$, $\AVUpdate$, and $\Update$ were defined in
-Figure~\ref{fig:defs:utxo-shelley}
+Note that $\PPUpdate$, $\AVUpdate$, and $\Update$ were defined in
+Figure~\ref{fig:defs:utxo-shelley}, and that $\fun{pvCanFollow}$
+was defined in \cite{byron_ledger_spec}.
 
 
 The signature for the keys in the proposal will be checked in the
@@ -69,6 +70,8 @@ \section{Updates}
       &
       \dom{pup}\subseteq\dom{dms}
       \\
+      \var{ppv}\mapsto\var{v}\in\var{pup}\implies\fun{pvCanFollow}~(\fun{ppv}~\var{pup_s})~\var{v}
+      \\
       \var{slot} < \firstSlot{((\epoch{slot}) + 1) - \SlotsPrior}
     }
     {
@@ -96,6 +99,8 @@ \section{Updates}
 genesis keys agree.
 This function will also be used for the protocol parameters later in Section~\ref{sec:epoch}.
 Note that $\type{T}$ is an arbitrary type.
+The function $\fun{validAV}$ uses three functions from \cite{byron_ledger_spec}, namely
+$\fun{apNameValid}$, $\fun{svCanFollow}$, and $\fun{sTagValid}$.
 
 %%
 %% Figure - Helper Function for Consensus of Update Proposals
@@ -110,13 +115,25 @@ \section{Updates}
         \end{cases}
   \end{align*}
 
+  \begin{align*}
+      & \fun{validAV} \in \ApName \to \ApVer \to \Metadata \to \Applications \to \Bool\\
+      & \fun{validAV}~\var{an}~\var{av}~\var{md}~\var{avs} = \\
+      & ~~~~\fun{apNameValid}~\var{an}
+        ~\land~\fun{svCanFollow}~\var{avs}~(\var{an},~\var{av})
+        ~\land~\forall\var{st}\in\dom{md},~\fun{sTagValid}~\var{st}
+  \end{align*}
+
   \begin{align*}
       & \fun{newAVs} \in \Applications \to (\Slot\mapsto\Applications) \to \Applications \\
       & \fun{newAVs}~\var{avs}~\var{favs} =
         \begin{cases}
-          \var{avs}' & \var{favs}\neq\emptyset
-                       ,~s_m\mapsto\var{avs'}\in\var{favs}
-                       ,~s_m=\max(\dom{\var{favs}})\\
+          \var{avs}\unionoverrideRight\var{avs}'
+                     & \var{favs}\neq\emptyset \\
+                     & ~\land~s_m\mapsto\var{avs'}\in\var{favs} \\
+                     & ~\land~s_m=\max(\dom{\var{favs}}) \\
+                     & ~\land~\forall(an\mapsto(av, mdt)\in\var{avs}'),
+                         ~\fun{validAV}~\var{an}~\var{av}~\var{md}~\var{avs}
+          \\
           \var{avs} & \text{otherwise}
         \end{cases}
   \end{align*}