mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
f4ee7a0525
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
91 lines
2.9 KiB
TeX
91 lines
2.9 KiB
TeX
\documentclass[11pt,a4paper]{article}
|
|
\usepackage{../shared/luxcover}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath,amssymb,amsfonts,amsthm}
|
|
\usepackage{graphicx}
|
|
\usepackage{hyperref}
|
|
\usepackage{booktabs}
|
|
\usepackage{listings}
|
|
\input{../shared/lstlang}
|
|
\usepackage{xcolor}
|
|
\usepackage{enumitem}
|
|
\usepackage{float}
|
|
|
|
\newtheorem{theorem}{Theorem}
|
|
\newtheorem{lemma}[theorem]{Lemma}
|
|
\newtheorem{definition}{Definition}
|
|
\newtheorem{remark}{Remark}
|
|
|
|
\lstdefinelanguage{TLA}{
|
|
morekeywords={MODULE,EXTENDS,CONSTANTS,VARIABLES,Init,Next,Spec,THEOREM,
|
|
ASSUME,LET,IN,IF,THEN,ELSE,CASE,OTHER,CHOOSE,SUBSET,UNION,DOMAIN,
|
|
UNCHANGED,ENABLED,TRUE,FALSE,Nat,Int,Seq,TLC,Integers,Sequences,FiniteSets},
|
|
morekeywords=[2]{TypeOK,Safety,Liveness,Fairness,Inv},
|
|
keywordstyle=[2]\color{purple}\bfseries,
|
|
morecomment=[l]{\\*},
|
|
morestring=[b]",
|
|
sensitive=true,
|
|
}
|
|
|
|
\lstset{
|
|
basicstyle=\small\ttfamily,
|
|
keywordstyle=\color{blue}\bfseries,
|
|
commentstyle=\color{gray},
|
|
stringstyle=\color{red},
|
|
breaklines=true,
|
|
frame=single,
|
|
numbers=left,
|
|
numberstyle=\tiny\color{gray}
|
|
}
|
|
|
|
\hypersetup{
|
|
colorlinks=true,
|
|
linkcolor=blue,
|
|
citecolor=blue,
|
|
urlcolor=blue
|
|
}
|
|
|
|
\title{Model Checking Distributed Protocols with TLA+}
|
|
\author{
|
|
Lux Research \\
|
|
Lux Industries, Inc.\thanks{Corresponding author: [email protected]}\\
|
|
\texttt{[email protected]}
|
|
}
|
|
\date{2025}
|
|
|
|
\begin{document}
|
|
|
|
\luxcoverpage
|
|
|
|
\begin{abstract}
|
|
Model checking exhaustively explores every reachable state of a system to verify that a
|
|
property holds universally. TLA+ (Temporal Logic of Actions) is a specification language
|
|
designed by Leslie Lamport for describing and verifying concurrent and distributed systems.
|
|
Its model checker, TLC, can enumerate billions of states to find subtle bugs that testing
|
|
misses. This paper teaches TLA+ from first principles: the temporal logic, the specification
|
|
language, the model checker, and the techniques for managing state space explosion. We then
|
|
apply these tools to two Lux Network protocols---Teleport (cross-chain bridge) and Wave
|
|
(sub-second finality)---showing the complete specifications, the properties checked, the
|
|
bugs found during specification, and the techniques used to make model checking tractable.
|
|
The reader will learn to write TLA+ specifications, run TLC, interpret violations, and
|
|
integrate model checking into a protocol development workflow.
|
|
\end{abstract}
|
|
|
|
\tableofcontents
|
|
\newpage
|
|
|
|
%% ============================================================
|
|
|
|
\input{sections/01-why-model-checking}
|
|
\input{sections/02-tla-fundamentals}
|
|
\input{sections/03-modeling-consensus-protocols}
|
|
\input{sections/04-the-teleport-specification}
|
|
\input{sections/05-the-wave-specification}
|
|
\input{sections/06-state-space-explosion}
|
|
\input{sections/07-from-specification-to-implementation}
|
|
\input{sections/08-practical-guide-your-first-tla-specifica}
|
|
\input{sections/99-conclusion}
|
|
|
|
\end{document}
|