mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
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.
9 lines
347 B
TeX
9 lines
347 B
TeX
\section{Layer 7: Formal Proofs (Lean~4)}
|
|
|
|
|
|
Covered in our companion paper on Lean~4. Formal proofs provide the strongest guarantees
|
|
but are the most expensive to produce. We use them for the core consensus safety and
|
|
liveness theorems---properties where failure means chain death.
|
|
|
|
%% ============================================================
|