mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-03 05:07:46 +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.
30 lines
1.0 KiB
TeX
30 lines
1.0 KiB
TeX
\section{Halmos vs.\ Fuzzing vs.\ Formal Verification}
|
|
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}llll@{}}
|
|
\toprule
|
|
& \textbf{Fuzzing} & \textbf{Symbolic (Halmos)} & \textbf{Formal (Lean~4)} \\
|
|
\midrule
|
|
Coverage & Random sampling & All paths (bounded) & All inputs \\
|
|
Finds bugs & Yes (common bugs) & Yes (subtle bugs) & Proves absence \\
|
|
Speed & Fast & Medium & Slow \\
|
|
Setup & Easy & Easy & Hard \\
|
|
Limitations & Misses edge cases & Path explosion & Manual effort \\
|
|
Best for & Implementation bugs & Logic bugs & Protocol correctness \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Verification technique comparison.}
|
|
\end{table}
|
|
|
|
Use all three. They are complementary:
|
|
\begin{enumerate}[nosep]
|
|
\item \textbf{Fuzzing} (Foundry) catches implementation bugs quickly.
|
|
\item \textbf{Symbolic execution} (Halmos) proves properties of individual contracts.
|
|
\item \textbf{Formal verification} (Lean~4) proves properties of the protocol design.
|
|
\end{enumerate}
|
|
|
|
%% ============================================================
|