mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
55 lines
2.7 KiB
TeX
55 lines
2.7 KiB
TeX
\section{Formal Verification}
|
|
|
|
\label{sec:formal}
|
|
|
|
FPC's safety and liveness properties have been formally verified in Lean~4, with machine-checked proofs available at \texttt{github.com/luxfi/formal}~\cite{luxformal2025}.
|
|
|
|
\subsection{Proof Architecture}
|
|
|
|
The formalization is organized into three layers, each mapping directly to the Go implementation:
|
|
|
|
\begin{table}[h]
|
|
\centering
|
|
\begin{tabular}{llll}
|
|
\toprule
|
|
\textbf{Lean Module} & \textbf{Go Source} & \textbf{Theorems} & \textbf{Properties} \\
|
|
\midrule
|
|
\texttt{Consensus.Safety} & \texttt{core/consensus.go} & 3 & No conflicting finality \\
|
|
\texttt{Consensus.Liveness} & \texttt{core/consensus.go} & 2 & Guaranteed termination \\
|
|
\texttt{Consensus.BFT} & \texttt{core/consensus.go} & 4 & $f < n/3$ tolerance \\
|
|
\texttt{Protocol.Wave} & \texttt{protocol/wave/wave.go} & 4 & Confidence monotonicity \\
|
|
\texttt{Protocol.Flare} & \texttt{protocol/wave/fpc/fpc.go} & 3 & Threshold range invariant \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Lean~4 formalization of FPC consensus properties}
|
|
\label{tab:formal}
|
|
\end{table}
|
|
|
|
\subsection{Key Theorems}
|
|
|
|
\begin{theorem}[Machine-Checked Safety]
|
|
\label{thm:formal-safety}
|
|
For any two honest nodes $i$, $j$ that finalize values $v_1$, $v_2$ at the same height:
|
|
$$\forall\, i, j, v_1, v_2.\; \mathsf{honest}(i) \land \mathsf{honest}(j) \land \mathsf{finalized}(i, v_1) \land \mathsf{finalized}(j, v_2) \implies v_1 = v_2$$
|
|
Proved in \texttt{Consensus.Safety.safety} via unique-threshold lemma and confidence monotonicity.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}[Machine-Checked Finalization]
|
|
\label{thm:formal-finalization}
|
|
After $\beta$ consecutive rounds where the yes-vote count meets the $\alpha$ threshold and matches the current preference, the item is decided:
|
|
$$\mathsf{confidence}(s) + 1 \geq \beta \implies \mathsf{step}(\mathit{cfg}, s, r).\mathsf{decided} = \mathsf{true}$$
|
|
Proved in \texttt{Protocol.Wave.finalization\_after\_beta} by unfolding the step function.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}[Machine-Checked Decision Stability]
|
|
\label{thm:formal-stability}
|
|
Once a Wave item is decided, no further round changes its state:
|
|
$$\mathsf{decided}(s) = \mathsf{true} \implies \mathsf{step}(\mathit{cfg}, s, r) = s$$
|
|
Proved in \texttt{Protocol.Wave.decided\_is\_stable} by the early-return guard in the step function.
|
|
\end{theorem}
|
|
|
|
\subsection{Verification Methodology}
|
|
|
|
Each Lean theorem maps to a specific code path in the Go implementation via comments that reference exact file paths and line numbers (e.g., \texttt{wave.go:98-102} for the early-return guard). This traceability ensures that the formal model accurately reflects the deployed code. The Lean proofs are type-checked by the Lean~4 compiler and verified in CI on every commit to the \texttt{luxfi/formal} repository.
|
|
|