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.
19 lines
647 B
TeX
19 lines
647 B
TeX
\section{Formal Verification}
|
|
|
|
\label{sec:formal}
|
|
%% =====================================================================
|
|
|
|
The hash chain integrity property is mechanized in Lean~4:
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{Crypto.HashChainIntegrity}: proof that any modification
|
|
to any block in the chain is detectable by comparing the
|
|
recomputed head hash against the stored head hash.
|
|
\end{itemize}
|
|
|
|
The cache consistency and crash recovery properties are modeled in
|
|
TLA+ in the \texttt{lux/proofs/tla/} directory as the
|
|
\texttt{VaultSync} specification.
|
|
|
|
%% =====================================================================
|