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

\section{Formal Verification}
\label{sec:formal}
%% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

The Lux Bridge security model is backed by formal proofs at two levels: Lean~4 for cryptographic primitives and consensus properties, and Halmos for Solidity contract invariants.

\subsection{Lean 4 Proofs (Consensus and Cryptography)}

The Lean~4 formal verification library\footnote{\url{https://github.com/luxfi/formal}} contains 18 proof files covering:

\begin{table}[h]
\centering
\begin{tabular}{lll}
\toprule
\textbf{Category} & \textbf{Files} & \textbf{Properties Proven} \\
\midrule
\textbf{Consensus} & \texttt{BFT.lean}, \texttt{Safety.lean}, \texttt{Liveness.lean} & BFT safety/liveness, $2f+1$ quorum \\
\textbf{Crypto} & \texttt{BLS.lean} & Aggregation soundness, bilinearity \\
& \texttt{FROST.lean} & Threshold correctness, unforgeability \\
& \texttt{MLDSA.lean} & Post-quantum signature correctness \\
& \texttt{Corona.lean} & LWE security, threshold sharing \\
\textbf{Protocol} & \texttt{Quasar.lean} & Hybrid verification correctness \\
& \texttt{Wave.lean}, \texttt{Flare.lean}, \ldots & Consensus protocol variants \\
\textbf{Warp} & \texttt{Delivery.lean}, \texttt{Ordering.lean} & Message delivery, FIFO ordering \\
\bottomrule
\end{tabular}
\caption{Lean 4 formal proof coverage}
\end{table}

\paragraph{Key theorems proven in Lean~4.}

\begin{enumerate}[leftmargin=1.1em]
  \item \textbf{BLS aggregation soundness}: If $e(\sigma_i, g_2) = e(H(m), pk_i)$ for all $i \in S$, then $e(\sum_i \sigma_i, g_2) = e(H(m), \sum_i pk_i)$. Proven from the bilinearity axiom.
  \item \textbf{FROST correctness}: A signature produced by $t$ honest participants verifies under the aggregate public key, for all messages and threshold parameters.
  \item \textbf{Corona LWE security}: The decisional LWE assumption with parameters $n = 630$, $q = 2^{32}$, $\sigma = 13744$ provides 128-bit security. Modeled axiomatically with concrete parameter verification.
  \item \textbf{Warp delivery}: Every message sent via Warp with $\geq 2/3$ stake-weighted BLS signatures is delivered exactly once on the destination chain (no duplication, no loss).
\end{enumerate}

\subsection{Halmos Symbolic Proofs (Solidity Contracts)}

Halmos \cite{halmos} performs symbolic execution of Solidity functions, proving invariants hold for \emph{all possible inputs} (not just sampled test vectors). The bridge verification suite contains 68 \texttt{check\_} functions across 7 Halmos test files:

\begin{table}[h]
\centering
\begin{tabular}{llr}
\toprule
\textbf{Test File} & \textbf{Invariants Proven} & \textbf{Proofs} \\
\midrule
\texttt{HalmosE2E.t.sol} & Bridge conservation, daily limit, teleport, lifecycle & 23 \\
\texttt{HalmosLiquidLUX.t.sol} & Vault share math, fee monotonicity, solvency & 9 \\
\texttt{HalmosAMM.t.sol} & Constant product, LP share fairness & 9 \\
\texttt{HalmosMarkets.t.sol} & Lending solvency, collateral ratio & 7 \\
\texttt{AMMInvariant.t.sol} & AMM deep invariants & 3 \\
\texttt{LiquidSolvency.t.sol} & Liquid protocol solvency & 3 \\
\texttt{MarketsSolvency.t.sol} & Markets deep solvency & 3 \\
\midrule
& \textbf{Total} & \textbf{57} \\
\bottomrule
\end{tabular}
\caption{Halmos symbolic proof coverage (standard + formal repos). An additional 11 proofs cover the liquid protocol transmuter earmark conservation, totaling 68 across the ecosystem.}
\end{table}

\paragraph{Bridge-specific invariants proven by Halmos.}

\begin{enumerate}[leftmargin=1.1em]
  \item \textbf{Conservation}: $\texttt{bridgeMint}(a) \circ \texttt{bridgeBurn}(a)$ returns total supply to its original value.
  \item \textbf{Daily limit}: For any sequence of mints $a_1, a_2, \ldots$ within a single period, $\sum a_i \leq \texttt{dailyMintLimit}$ (no overflow bypass).
  \item \textbf{Teleport conservation}: For a two-chain teleport (lock on source, mint on destination), the combined supply is invariant: $\text{supply}_A + \text{supply}_B = \text{const}$.
  \item \textbf{Multi-hop conservation}: For 3-chain teleport $A \to B \to C$, the total supply across all three chains is conserved.
  \item \textbf{Fee accounting}: Performance fees extracted during yield distribution satisfy $\text{fee} + \text{net} = \text{gross}$ (no rounding leakage above 1 wei).
  \item \textbf{Exchange rate monotonicity}: The vault share exchange rate never decreases after fee injection: $\frac{\text{totalAssets}_{t+1}}{\text{totalShares}_{t+1}} \geq \frac{\text{totalAssets}_t}{\text{totalShares}_t}$.
\end{enumerate}

\subsection{Invariant Test Suite}

Beyond Halmos, the codebase includes 9 Foundry invariant test contracts that run stateful fuzzing over extended operation sequences:

\begin{table}[h]
\centering
\begin{tabular}{lr}
\toprule
\textbf{Invariant Test} & \textbf{Properties} \\
\midrule
\texttt{InvariantBridge.t.sol} & Supply conservation, rate limits \\
\texttt{InvariantStaking.t.sol} & Staking ratio monotonicity \\
\texttt{InvariantGovernance.t.sol} & Voting power conservation \\
\texttt{InvariantMarkets.t.sol} & Lending solvency \\
\texttt{InvariantAMM.t.sol} & Constant product invariant \\
\texttt{InvariantStableSwap.t.sol} & StableSwap D invariant \\
\texttt{InvariantPerps.t.sol} & AUM conservation \\
\texttt{InvariantTreasury.t.sol} & Fee distribution totals \\
\texttt{InvariantKarma.t.sol} & Soul-bound non-transferability \\
\texttt{InvariantLiquidLUX.t.sol} & Vault solvency \\
\bottomrule
\end{tabular}
\caption{Foundry invariant test suite (stateful fuzzing)}
\end{table}

The total verification coverage across the Lux ecosystem: \textbf{1,041 unit/integration tests} (forge test), \textbf{68 Halmos symbolic proofs}, \textbf{10 invariant fuzz suites}, and \textbf{30/45 Lean~4 consensus theorems} proven (18 files).

%% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++