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.
24 lines
1.3 KiB
TeX
24 lines
1.3 KiB
TeX
\section{Conclusion}
|
|
|
|
|
|
Formal verification with Lean~4 transforms security claims from marketing into
|
|
mathematics. We have demonstrated how to model BFT consensus, prove safety and liveness,
|
|
verify threshold arithmetic, and maintain a corpus of 384 machine-checked theorems with
|
|
zero \texttt{sorry}. The techniques are accessible to any engineer willing to invest
|
|
a few weeks learning Lean~4. The reward is certainty: not ``we tested it,'' but ``we
|
|
proved it.''
|
|
|
|
All proofs are available at \texttt{luxfi/formal} and compile with \texttt{lake build}
|
|
on Lean~4 v4.8.0 or later.
|
|
|
|
\begin{thebibliography}{99}
|
|
\bibitem{lean4} de Moura, L. and Ullrich, S. ``The Lean~4 Theorem Prover and Programming Language.'' CADE, 2021.
|
|
\bibitem{mathlib} The mathlib Community. ``The Lean Mathematical Library.'' CPP, 2020.
|
|
\bibitem{quasar} Lux Industries. ``Quasar: Triple-Proof BFT Consensus.'' 2024.
|
|
\bibitem{castro1999} Castro, M. and Liskov, B. ``Practical Byzantine Fault Tolerance.'' OSDI, 1999.
|
|
\bibitem{lamport2001} Lamport, L. ``Paxos Made Simple.'' ACM SIGACT News, 2001.
|
|
\bibitem{hawblitzel2015} Hawblitzel, C. et al. ``IronFleet: Proving Practical Distributed Systems Correct.'' SOSP, 2015.
|
|
\bibitem{yin2019} Yin, M. et al. ``HotStuff: BFT Consensus with Linearity and Responsiveness.'' PODC, 2019.
|
|
\end{thebibliography}
|
|
|