diff --git a/formal-spec/docs/leios-components-diag.tex b/formal-spec/docs/leios-components-diag.tex
new file mode 100644
index 00000000..92da507b
--- /dev/null
+++ b/formal-spec/docs/leios-components-diag.tex
@@ -0,0 +1,42 @@
+\documentclass{standalone}
+\usepackage{tikz-uml}
+
+\definecolor{bleudefrance}{rgb}{0.19, 0.55, 0.91}
+\definecolor{jasper}{rgb}{0.84, 0.23, 0.24}
+
+\begin{document}
+  \begin{tikzpicture}
+    \begin{umlpackage}{Leios}
+      \begin{umlcomponent}[x=0,y=0]{SpecStructure}
+        \umlbasiccomponent[x=-6,y=-4, fill=bleudefrance]{LeiosAbstract}
+        \umlbasiccomponent[y=0]{Blocks}
+        \umlbasiccomponent[y=-2, fill=bleudefrance]{Base Ledger}
+        \umlbasiccomponent[y=-4, fill=bleudefrance]{Key Registration Functionality}
+        \umlbasiccomponent[y=-6, fill=bleudefrance]{VRF Functionality}
+        \umlbasiccomponent[y=-8, fill=bleudefrance]{FFD Functionality}
+
+        \umlassemblyconnector[with port] {LeiosAbstract}{Blocks}
+        \umlassemblyconnector[with port] {LeiosAbstract}{Base Ledger}
+        \umlassemblyconnector[with port] {LeiosAbstract}{Key Registration Functionality}
+        \umlassemblyconnector[with port] {LeiosAbstract}{VRF Functionality}
+        \umlassemblyconnector[with port] {LeiosAbstract}{FFD Functionality}
+      \end{umlcomponent}
+
+      \begin{umlcomponent}[x=6,y=-1]{Protocol}
+        \umlbasiccomponent[x=2,y=0]{LeiosState}
+        \umlbasiccomponent[x=0,y=-2]{LeiosInput}
+        \umlbasiccomponent[x=4,y=-2]{LeiosOutput}
+      \end{umlcomponent}
+
+      \begin{umlcomponent}[x=6,y=-6]{Simplified Leios}
+      \end{umlcomponent}
+
+      \begin{umlcomponent}[x=10,y=-6]{Short-Pipeline Leios}
+      \end{umlcomponent}
+
+      \umlassemblyconnector[with port] {SpecStructure}{Protocol}
+      \umlassemblyconnector[with port] {Protocol-south-port}{Simplified Leios-north-port}
+      \umlassemblyconnector[with port] {Protocol-south-port}{Short-Pipeline Leios-north-port}
+    \end{umlpackage}
+  \end{tikzpicture}
+\end{document}
diff --git a/formal-spec/docs/leios-state-transition-diag.tex b/formal-spec/docs/leios-state-transition-diag.tex
new file mode 100644
index 00000000..701aa6a4
--- /dev/null
+++ b/formal-spec/docs/leios-state-transition-diag.tex
@@ -0,0 +1,30 @@
+\documentclass[tikz, border=3mm]{standalone}
+
+\tikzset{->, >=stealth, shorten >=2pt, shorten <=2pt, node distance=4cm }
+\definecolor{bleudefrance}{rgb}{0.19, 0.55, 0.91}
+\definecolor{jasper}{rgb}{0.84, 0.23, 0.24}
+
+\begin{document}
+\begin{tikzpicture}
+    \node (init) [circle, draw, align=center] {LeiosState\\$slot_0$};
+    \node[right of=init] (prev) [circle, draw, align=center, dotted] {LeiosState\\$slot_{n-1}$};
+    \node[right of=prev] (focus) [circle, draw, align=center] {LeiosState\\$slot_n$};
+    \node[right of=focus] (next) [circle, draw, align=center, dotted] {LeiosState\\$slot_{n+1}$};
+    \node[right of=next] (last) [circle, draw=none, align=center] {};
+    \draw[->] (init) edge node[above] {$\cdots$}(prev) [dotted];
+    \draw[->] (prev) edge node[above] {Slot} (focus);
+    \draw[->] (focus) edge node[above] {Slot} (next);
+    \draw[->] (next) edge node[above] {} (last) [dotted];
+
+    \path[-stealth] (init) edge[out=45,in=135,looseness=5] node[above] {Init} (init);
+    \path[-stealth] (focus) edge[out=45,in=135,looseness=5, color=bleudefrance] node[above] {\textcolor{black}{IB Role}} (focus);
+    \path[-stealth] (focus) edge[out=45,in=135,looseness=10, color=bleudefrance] node[above] {\textcolor{black}{EB Role}} (focus);
+    \path[-stealth] (focus) edge[out=45,in=135,looseness=15, color=bleudefrance] node[above] {\textcolor{black}{Vote Role}} (focus);
+    \path[-stealth] (focus) edge[out=45,in=135,looseness=20, color=jasper] node[above] {\textcolor{black}{$Base_{2}$}} (focus);
+    \path[-stealth] (focus) edge[out=45,in=135,looseness=25, color=jasper, dashed] node[above] {\textcolor{black}{$Base_{1}$}} (focus);
+    \path[-stealth] (focus) edge[out=45,in=135,looseness=30, dashed] node[above] {\textcolor{black}{Ftch}} (focus);
+    \path[-stealth] (focus) edge[out=225,in=315,looseness=5] node[above] {\textcolor{black}{Not IB Role}} (focus);
+    \path[-stealth] (focus) edge[out=225,in=315,looseness=10] node[above] {\textcolor{black}{Not EB Role}} (focus);
+    \path[-stealth] (focus) edge[out=225,in=315,looseness=15] node[above] {\textcolor{black}{Not Vote Role}} (focus);
+\end{tikzpicture}
+\end{document}