mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-02 11:39:52 +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.4 KiB
TeX
24 lines
1.4 KiB
TeX
\section{Conclusion}
|
|
|
|
|
|
Symbolic execution with Halmos provides a practical middle ground between testing and
|
|
formal verification. It requires minimal effort above standard Foundry testing---write
|
|
\texttt{check\_} instead of \texttt{test\_}, use \texttt{assert} instead of
|
|
\texttt{assertEq}---but provides dramatically stronger guarantees: proofs over all
|
|
inputs, not just tested ones. Our 9 Halmos proofs cover the most critical invariants of
|
|
Lux Network's smart contract suite and run in CI on every pull request.
|
|
|
|
The path from testing to symbolic verification is incremental. Start by converting your
|
|
most critical fuzz test to a symbolic test. If Halmos verifies it, you have a proof.
|
|
If it finds a counterexample, you have a bug. Either way, you win.
|
|
|
|
\begin{thebibliography}{99}
|
|
\bibitem{halmos} Park, D. et al. ``Halmos: Symbolic Testing for EVM Smart Contracts.'' a16z Crypto, 2023.
|
|
\bibitem{king1976} King, J.C. ``Symbolic Execution and Program Testing.'' Communications of the ACM, 1976.
|
|
\bibitem{z3} de Moura, L. and Bj{\o}rner, N. ``Z3: An Efficient SMT Solver.'' TACAS, 2008.
|
|
\bibitem{mythril} Mueller, B. ``Smashing Ethereum Smart Contracts for Fun and Real Profit.'' HITB, 2018.
|
|
\bibitem{manticore} Mossberg, M. et al. ``Manticore: A User-Friendly Symbolic Execution Framework.'' ASE, 2019.
|
|
\bibitem{foundry} Paradigm. ``Foundry: A Blazing Fast, Portable and Modular Toolkit for Ethereum Application Development.'' 2022.
|
|
\end{thebibliography}
|
|
|