papers/lux-consensus/sections/10-formal-verification.tex

\section{Formal Verification}

\label{sec:formal}

We have mechanized the core safety, liveness, and cryptographic properties of the Lux
consensus protocol family in the Lean~4 interactive theorem prover~\cite{moura2021lean4},
using the Mathlib library (v4.14.0)~\cite{mathlib4} for foundational mathematics. The
formalization covers all twelve Lux protocol components and four cryptographic primitives,
producing 36 machine-checked theorems and 27 axioms across 18 source files.
The complete proof development is publicly available.\footnote{\url{https://github.com/luxfi/formal}}

\subsection{Scope and Methodology}

The formal development is organized into four libraries, following the modular
architecture of the Lux implementation:

\begin{enumerate}
\item \textbf{Consensus}: Core safety, liveness, and BFT threshold properties
(3~files, 10~statements).
\item \textbf{Protocol}: Models of all nine protocol components---Wave, Flare,
Ray, Field, Quasar, Nova, Nebula, Photon, Prism (9~files, 24~statements).
\item \textbf{Crypto}: Axiomatization of BLS, FROST, Pulsar, and ML-DSA
(4~files, 20~statements).
\item \textbf{Warp}: Cross-chain delivery and causal ordering guarantees
(2~files, 9~statements).
\end{enumerate}

Each protocol component is modeled as a state machine with explicit transition
functions, mirroring the Go implementation. Axioms are used to encapsulate cryptographic
hardness assumptions (e.g., bilinear pairings for BLS, discrete logarithm for FROST,
LWE for Pulsar) and probabilistic sampling properties that are established by
independent cryptographic arguments.

\subsection{BFT Threshold Theorems}

The Byzantine fault tolerance threshold $f < n/3$ is formalized through five theorems
that establish the structural arithmetic underpinning all Lux consensus modes.

\begin{theorem}[Quorum Intersection (Lean: \texttt{Consensus.BFT.quorum\_intersection})]
\label{thm:formal-quorum}
For $n$ validators with $f < n/3$ Byzantine,
any two quorums $q_1, q_2 > 2n/3$ satisfy $q_1 + q_2 > n + f$.
\end{theorem}

This guarantees that any two supermajority quorums share at least one honest validator,
which is the foundation of BFT safety. The Lean proof is completed by the \texttt{omega}
tactic (linear arithmetic decision procedure).

\begin{theorem}[Honest Majority Sufficiency (Lean: \texttt{Consensus.BFT.honest\_majority\_sufficient})]
\label{thm:formal-honest}
With $n = 3f + 1$ validators, the honest count $2f + 1 > 2(3f+1)/3$.
\end{theorem}

\begin{theorem}[Unique Alpha Threshold (Lean: \texttt{Consensus.BFT.unique\_alpha\_threshold})]
\label{thm:formal-alpha}
For sample size $k$ and threshold $\alpha > 2k/3$, two distinct values cannot both
receive $\geq \alpha$ votes in the same round, since $v_1 + v_2 > k$.
\end{theorem}

This theorem mechanizes the argument from Section~\ref{sec:analysis}: the supermajority
threshold ensures that at most one value can exceed $\alpha$ in any single query round.

\begin{theorem}[Certificate Quorum Overlap (Lean: \texttt{Consensus.BFT.certificate\_quorum\_overlap})]
For $3f < n$, any two certificates of size $\geq 2f+1$ satisfy $\text{cert}_1 + \text{cert}_2 > n$.
\end{theorem}

\begin{theorem}[BFT Intersection (Lean: \texttt{Consensus.BFT.bft\_intersection})]
Two sets of size $2f+1$ from $n = 3f+1$ validators overlap by at least $f+1$ members:
$2(2f+1) > n + f$.
\end{theorem}

All five BFT theorems are fully proved (no \texttt{sorry}) using Lean's \texttt{omega} decision
procedure for linear arithmetic over natural numbers.

\subsection{Safety and Liveness}

The main consensus correctness theorems formalize the arguments of Section~\ref{sec:analysis}.

\begin{theorem}[Safety (Lean: \texttt{Consensus.safety})]
\label{thm:formal-safety}
If two honest nodes $i, j$ both finalize values $v_1, v_2$ respectively, and the honest
count exceeds $2f$, and $\alpha > 2k/3$, then $v_1 = v_2$.
\end{theorem}

The proof relies on two axioms that capture protocol invariants verified at the
implementation level:
\begin{itemize}[nosep]
\item \texttt{finalized\_preference\_stable}: Once a node finalizes, its preference is
immutable across all future rounds. This corresponds to the early-return guard in
\texttt{wave.go:98--102}.
\item \texttt{unique\_threshold}: At most one value can achieve $\alpha$-threshold in a
round when honest nodes dominate. This follows from Theorem~\ref{thm:formal-alpha}.
\end{itemize}

\begin{theorem}[Liveness (Lean: \texttt{Consensus.Liveness.liveness})]
\label{thm:formal-liveness}
Under partial synchrony, if round $r_0$ is synchronous, the honest count exceeds $2f$,
and honest nodes preferring $v$ exceed $\alpha$, then there exist a round
$r \leq r_0 + \beta + \delta$ and a node $i$ such that $i$ is honest and has finalized $v$.
\end{theorem}

The liveness proof depends on three axioms modeling the partial synchrony assumption:
\begin{itemize}[nosep]
\item \texttt{post\_gst\_delivery}: After GST, messages between honest nodes arrive within
$\delta$ rounds.
\item \texttt{honest\_sample\_dominance}: After GST, honest majority preference propagates
across rounds.
\item \texttt{confidence\_accumulation}: Under honest majority and synchrony, confidence
counters increment monotonically.
\end{itemize}

\subsection{Protocol Component Verification}

Each of the nine protocol components is formalized as a state machine with
transition functions and invariant theorems.

\begin{table}[h]
\centering
\caption{Formal verification coverage by protocol component}
\label{tab:formal}
\begin{tabular}{@{}llll@{}}
\toprule
Component & Theorems & Axioms & Key Properties \\
\midrule
Wave     & 3 & 0 & Decision stability, confidence monotonicity, finalization \\
Flare    & 3 & 0 & Cert/skip exclusivity, honest support, classification totality \\
Ray      & 3 & 0 & Prefix ordering, no-gaps, monotonicity \\
Field    & 2 & 0 & Consistent cut preservation, committed set monotonicity \\
Quasar   & 3 & 1 & Height monotonicity, BLS quorum, dual-signature finality \\
Nova     & 1 & 0 & Height strictly increasing \\
Nebula   & 1 & 0 & Committed set monotonicity \\
Photon   & 2 & 0 & Selection frequency, committee size \\
Prism    & 1 & 2 & Fisher-Yates uniformity, prefix-$k$ uniformity \\
\bottomrule
\end{tabular}
\end{table}

\paragraph{Wave (threshold voting engine).}
The Wave model formalizes the core voting loop. The step function \texttt{Protocol.Wave.step}
mirrors \texttt{wave.go:Tick}, encoding the confidence counter increment, preference
flipping, and finalization logic. Three theorems are fully proved:
\begin{itemize}[nosep]
\item \texttt{decided\_is\_stable}: Once \texttt{decided = true}, the step function
returns the same state for any round result.
\item \texttt{confidence\_monotone\_on\_match}: When the threshold is met and matches
the current preference, confidence increments by exactly one.
\item \texttt{finalization\_after\_beta}: When confidence reaches $\beta$, the item
transitions to the decided state.
\end{itemize}

\paragraph{Flare (DAG commit rule).}
The Flare model formalizes the certificate and skip classification from
\texttt{core/dag/flare.go}. The key result is:

\begin{theorem}[Certificate--Skip Exclusivity (Lean: \texttt{Protocol.Flare.cert\_skip\_exclusive})]
For $3f < n$, a proposer vertex cannot simultaneously hold a certificate ($\geq 2f+1$
support) and a skip ($\geq 2f+1$ non-support).
\end{theorem}

The proof proceeds by contradiction: if both held, total votes
$\geq 2(2f+1) = 4f + 2$, but total votes $\leq n < 3f + 1 < 4f + 2$ for $f > 0$.

\paragraph{Field (DAG consensus driver).}
Field formalizes the consistent cut property for DAG commits. The ancestry relation is
defined inductively, and a consistent cut is a downward-closed set under ancestry.
The theorem \texttt{committed\_is\_consistent\_cut} establishes that the commit operation
preserves this invariant.

\paragraph{Quasar (quantum finality engine).}
The Quasar model captures the dual BLS + Pulsar signature requirement for
quantum-resistant finality:

\begin{theorem}[Quantum Finality Requires Both Signatures
(Lean: \texttt{Protocol.Quasar.quantum\_finality\_requires\_both})]
A valid quantum signature $\texttt{isValidQuantumSig}(qs) = \texttt{true}$ implies both
$qs.\texttt{bls.valid} = \texttt{true}$ and $qs.\texttt{corona.valid} = \texttt{true}$.
\end{theorem}

\subsection{Cryptographic Axiomatization}

Cryptographic primitives are axiomatized rather than fully proved, following standard
practice in formal verification of distributed protocols~\cite{hawblitzel2015ironfleet}.
The axioms encapsulate hardness assumptions that are established by independent
cryptographic reductions.

\paragraph{BLS signatures.}
The BLS formalization introduces abstract types $\mathbb{G}_1$, $\mathbb{G}_2$, $\mathbb{G}_T$ for the
pairing groups, and axiomatizes the bilinear pairing $e : \mathbb{G}_1 \times \mathbb{G}_2 \to \mathbb{G}_T$
with left and right bilinearity:
\begin{align}
e(a + b, c) &= e(a, c) \cdot e(b, c) \label{eq:bilinear-left} \\
e(a, b + c) &= e(a, b) \cdot e(a, c) \label{eq:bilinear-right}
\end{align}

From these axioms, the aggregation soundness theorem is derived constructively:

\begin{theorem}[BLS Aggregation Soundness (Lean: \texttt{Crypto.BLS.aggregate\_two\_sound})]
\label{thm:formal-bls}
If $\texttt{verify}(s_1) \Leftrightarrow e(\sigma_1, g_2) = e(m, \text{pk}_1)$ and
$\texttt{verify}(s_2) \Leftrightarrow e(\sigma_2, g_2) = e(m, \text{pk}_2)$ for the same
message $m$, then
$e(\sigma_1 + \sigma_2, g_2) = e(m, \text{pk}_1 + \text{pk}_2)$.
\end{theorem}

The proof chains the bilinearity axioms~(\ref{eq:bilinear-left}) and~(\ref{eq:bilinear-right})
with the individual verification equations, corresponding directly to the BLS aggregate
verification in \texttt{quasar/bls.go}.

\paragraph{FROST threshold signatures.}
FROST (Flexible Round-Optimized Schnorr Threshold~\cite{komlo2020frost}) is axiomatized
with correctness and unforgeability:
\begin{itemize}[nosep]
\item \texttt{frost\_correctness}: If $\geq t$ honest participants execute the protocol,
a valid Schnorr signature is produced.
\item \texttt{frost\_unforgeability}: With $< t$ compromised shares, no valid signature
can be forged (random oracle model, discrete logarithm assumption).
\end{itemize}

\paragraph{Pulsar post-quantum signatures.}
The Pulsar lattice-based threshold scheme is axiomatized with LWE parameters
$(n_{\text{lwe}} = 630, q = 2^{32}, \sigma \approx 13{,}744)$ providing 128-bit
post-quantum security:
\begin{itemize}[nosep]
\item \texttt{corona\_correctness}: Valid threshold execution produces a verifiable
signature.
\item \texttt{corona\_pq\_unforgeability}: Under the LWE hardness assumption, quantum
adversaries cannot forge with fewer than $t$ shares.
\item \texttt{noise\_bound\_correct} (proved): Gaussian noise within $q/4$ is strictly
less than $q$, ensuring correct decryption.
\end{itemize}

\paragraph{ML-DSA (FIPS 204).}
The NIST post-quantum signature standard is axiomatized with:
\begin{itemize}[nosep]
\item \texttt{mldsa\_correctness}: Sign-then-verify always succeeds for valid key pairs.
\item \texttt{mldsa\_euf\_cma}: Existential unforgeability under chosen-message attack
(Module-LWE hardness).
\item \texttt{sig\_size\_bounded} (proved): All ML-DSA security levels produce signatures
$\leq 5{,}000$ bytes.
\end{itemize}

\subsection{Warp Cross-Chain Delivery}

The Warp messaging protocol is formalized with four delivery theorems and two
ordering theorems, establishing exactly-once causal delivery.

\begin{theorem}[No Replay (Lean: \texttt{Warp.Delivery.no\_replay})]
\label{thm:formal-noreplay}
If a message nonce has been processed ($\texttt{nonce} \in \texttt{processedNonces}$),
the message is rejected: $\texttt{processMessage}(s, \texttt{msg}) = \texttt{none}$.
\end{theorem}

\begin{theorem}[Authenticity (Lean: \texttt{Warp.Delivery.authenticity})]
If $\texttt{msg.sigValid} = \texttt{false}$, then
$\texttt{processMessage}(s, \texttt{msg}) = \texttt{none}$.
\end{theorem}

\begin{theorem}[Valid Delivery (Lean: \texttt{Warp.Delivery.valid\_message\_succeeds})]
If $\texttt{msg.sigValid} = \texttt{true}$ and
$\texttt{nonce} \notin \texttt{processedNonces}$, then
$\exists\, s', \texttt{processMessage}(s, \texttt{msg}) = \texttt{some}\; s'$.
\end{theorem}

Together, these three theorems establish exactly-once delivery semantics: every
valid message is accepted exactly once. The ordering module additionally proves
version monotonicity (\texttt{version\_monotone}) and stale-version rejection
(\texttt{stale\_rejected}), guaranteeing causal ordering of cross-chain settings
updates.

\subsection{Proof Status and Completeness}

Of the 36 theorems in the development, 33 are fully proved (the proof term type-checks
in Lean~4 without \texttt{sorry}). Three theorems carry \texttt{sorry} annotations,
indicating that the proof obligation is stated but the inductive argument is deferred:

\begin{enumerate}
\item \texttt{Consensus.safety}: The full proof requires round-indexed state traces
and induction over the $\beta$-length confirmation window. The core combinatorial
argument (unique alpha threshold) is fully proved.
\item \texttt{Consensus.Liveness.liveness}: Requires induction on $\beta$ under the
partial synchrony axioms. The supporting axioms are stated precisely.
\item \texttt{Protocol.Ray.decided\_is\_prefix}: Requires induction over the
\texttt{decideNext} step sequence.
\end{enumerate}

All 27 axioms are explicitly documented with their cryptographic or system-model
justification. No axiom introduces logical inconsistency; each is either a standard
cryptographic assumption (bilinearity, LWE hardness, random oracle model) or a
system-model postulate (partial synchrony, honest majority).

\begin{table}[h]
\centering
\caption{Summary of formal verification results}
\label{tab:formal-summary}
\begin{tabular}{@{}lrr@{}}
\toprule
Category & Proved (no \texttt{sorry}) & With \texttt{sorry} \\
\midrule
BFT threshold & 5 & 0 \\
Safety \& liveness & 1 & 2 \\
Protocol components & 19 & 1 \\
Cryptographic & 8 & 0 \\
Warp delivery & 6 & 0 \\
\midrule
\textbf{Total theorems} & \textbf{33} & \textbf{3} \\
Axioms (assumptions) & \multicolumn{2}{c}{27} \\
\bottomrule
\end{tabular}
\end{table}

\subsection{Relationship to Paper Proofs}

The mechanized theorems serve two roles. First, they independently verify the
algebraic and arithmetic arguments presented in Sections~\ref{sec:analysis}
and~\ref{sec:security}---in particular, the BFT threshold arithmetic
(Theorem~\ref{thm:bft}), the unique-threshold argument underlying safety
(Theorem~\ref{thm:safety}), and the quorum intersection property. Second, they
formalize protocol-level invariants (decision stability, confidence monotonicity,
consistent cuts) that are implicit in the prose proofs but critical for correctness
of the implementation.

The axiomatization of cryptographic primitives is standard practice: formal
verification of BLS pairing correctness or LWE hardness would require formalization
of elliptic curve arithmetic or lattice reduction algorithms, which is outside the
scope of a consensus protocol verification effort. The axioms we state are precisely
the properties assumed by the protocol and independently established by the
cryptographic literature~\cite{boneh2001short,komlo2020frost,ducas2018crystals}.

%% -----------------------------------------------------------------------
%%  11. CONCLUSION
%% -----------------------------------------------------------------------