mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-02 11:39:52 +00:00
zeekay
4a753bb639
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.
33 lines
1.7 KiB
TeX
33 lines
1.7 KiB
TeX
\section{Why Formal Verification}
|
|
|
|
|
|
Software testing can show the presence of bugs, never their absence. For blockchain systems
|
|
where bugs cause irreversible fund loss, this is insufficient. Formal verification uses
|
|
mathematical proof to establish that a program or protocol satisfies its specification for
|
|
\emph{all} inputs, not just the ones a test suite happens to exercise.
|
|
|
|
\subsection{The Cost of Bugs in Blockchain}
|
|
|
|
The DAO hack (2016, \$60M), Wormhole bridge exploit (2022, \$320M), and Ronin bridge
|
|
compromise (2022, \$625M) share a common pattern: the vulnerable code was tested, audited,
|
|
and deployed by competent teams. Testing and auditing are necessary but not sufficient.
|
|
Formal verification closes the gap by providing machine-checked guarantees.
|
|
|
|
\subsection{Why Not Just Test More?}
|
|
|
|
Consider a BFT consensus protocol with $n$ validators. Testing safety requires exploring
|
|
an exponential state space: $2^n$ possible failure combinations, arbitrary message
|
|
reorderings, unbounded network delays. Even property-based testing with millions of random
|
|
inputs covers a negligible fraction of this space. Formal proof covers it all by reasoning
|
|
about the structure of the state space rather than sampling points within it.
|
|
|
|
\subsection{Proof Assistants vs.\ Pen-and-Paper Proofs}
|
|
|
|
Peer-reviewed papers in distributed systems regularly contain subtle errors in their proofs.
|
|
Hawblitzel et al.\ found errors in published proofs of Paxos variants. A proof assistant
|
|
like Lean~4 mechanically checks every step: if the proof compiles, the theorem holds
|
|
(modulo the axioms of the underlying logic, which for Lean~4 is the Calculus of Inductive
|
|
Constructions plus propositional extensionality and quotient types).
|
|
|
|
%% ============================================================
|