mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +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.
25 lines
1.5 KiB
TeX
25 lines
1.5 KiB
TeX
\section{Conclusion}
|
|
|
|
|
|
TLA+ model checking finds bugs in distributed protocols that no amount of testing will
|
|
catch. The bugs it finds are exactly the subtle ones: race conditions, deadlocks, and
|
|
safety violations that occur only under specific message orderings. Writing a TLA+
|
|
specification forces you to think precisely about your protocol's behavior in all
|
|
scenarios---not just the happy path.
|
|
|
|
For Lux Network, TLA+ model checking found 3 bugs in the Wave protocol and verified
|
|
the safety and conservation properties of the Teleport bridge across 2.4 million states.
|
|
These specifications now serve as the canonical descriptions of these protocols, and
|
|
every protocol change requires updating the specification and re-running TLC before
|
|
modifying the Go implementation.
|
|
|
|
\begin{thebibliography}{99}
|
|
\bibitem{lamport2002} Lamport, L. ``Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.'' Addison-Wesley, 2002.
|
|
\bibitem{lamport1994} Lamport, L. ``The Temporal Logic of Actions.'' ACM TOPLAS, 1994.
|
|
\bibitem{newcombe2015} Newcombe, C. et al. ``How Amazon Web Services Uses Formal Methods.'' Communications of the ACM, 2015.
|
|
\bibitem{yin2019} Yin, M. et al. ``HotStuff: BFT Consensus with Linearity and Responsiveness.'' PODC, 2019.
|
|
\bibitem{castro1999} Castro, M. and Liskov, B. ``Practical Byzantine Fault Tolerance.'' OSDI, 1999.
|
|
\bibitem{tlc} Yu, Y., Manolios, P., and Lamport, L. ``Model Checking TLA+ Specifications.'' CHARME, 1999.
|
|
\end{thebibliography}
|
|
|