papers/hanzo-formal-verification/sections/07-platform-orchestrator-verification.tex

\section{Platform Orchestrator Verification}

\label{sec:platform}
% ============================================================================

The platform orchestrator manages service deployments across Kubernetes
clusters.

\subsection{Deployment State Machine}

\begin{definition}[Deployment States]
A deployment $d$ transitions through states $\mathcal{S} = \{
\texttt{pending}, \texttt{building}, \texttt{deploying}, \texttt{running},
\texttt{rolling\_update}, \texttt{rolling\_back}, \texttt{failed},
\texttt{terminated}\}$ with well-defined transitions.
\end{definition}

\begin{theorem}[State Machine Correctness]
The deployment state machine satisfies:
\begin{enumerate}[leftmargin=1.4em]
    \item \textbf{Reachability}: Every non-terminal state can eventually reach
    $\texttt{running}$ or $\texttt{failed}$.
    \item \textbf{No stuck states}: No state has zero outgoing transitions
    (except terminal states).
    \item \textbf{Rollback safety}: From $\texttt{rolling\_update}$, the system
    can always transition to $\texttt{rolling\_back}$, which always reaches
    the previous $\texttt{running}$ configuration.
\end{enumerate}
\end{theorem}

\subsection{Health Check Liveness}

\begin{theorem}[Health Check Liveness]
If a service is healthy (responds to health probes within timeout), the
orchestrator eventually marks it as $\texttt{running}$. If a service is
unhealthy (fails $k$ consecutive health probes), the orchestrator eventually
restarts it. No healthy service is restarted, and no unhealthy service remains
running indefinitely.
\end{theorem}

\subsection{Bug Found: Rolling Update with Zero Healthy Replicas}

During a rolling update, if all new replicas fail health checks simultaneously,
the orchestrator should roll back. However, the implementation allowed the
update to proceed until $\texttt{maxUnavailable}$ was reached, leaving the
service with zero healthy replicas before triggering rollback. The fix adds
a minimum healthy replica invariant: rollback triggers immediately if healthy
replicas drop below the configured minimum.

% ============================================================================