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.
86 lines
2.8 KiB
TeX
86 lines
2.8 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}
|
|
\usepackage{tikz}
|
|
\usetikzlibrary{arrows.meta,positioning}
|
|
|
|
\newtheorem{theorem}{Theorem}
|
|
\newtheorem{definition}{Definition}
|
|
\newtheorem{remark}{Remark}
|
|
|
|
\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{Testing Distributed Systems:\\From Unit Tests to Jepsen}
|
|
\author{
|
|
Lux Research \\
|
|
Lux Industries, Inc.\thanks{Corresponding author: [email protected]}\\
|
|
\texttt{[email protected]}
|
|
}
|
|
\date{2025}
|
|
|
|
\begin{document}
|
|
|
|
\luxcoverpage
|
|
|
|
\begin{abstract}
|
|
Distributed systems bugs are the hardest bugs: they only manifest under specific timing,
|
|
network conditions, and failure combinations that cannot be reproduced by running the
|
|
system once. This paper presents the full testing pyramid for distributed blockchain
|
|
systems: unit tests for individual components, integration tests for subsystem
|
|
interactions, property-based tests for algorithmic correctness, model checking for
|
|
protocol design, and formal proofs for mathematical certainty. We then cover fault
|
|
injection (Jepsen-style testing): how to inject network partitions, clock skew, process
|
|
crashes, and disk corruption, and how to verify linearizability and consistency under
|
|
these faults. We present Lux Network's testing stack: Go unit tests (12,847 tests),
|
|
Playwright E2E (342 tests), Foundry smart contract tests (832 tests), Halmos symbolic
|
|
tests (9 proofs), TLA+ model checking (2 protocols), and Lean~4 formal proofs (384
|
|
theorems). Each layer catches different bugs. Skipping any layer leaves a blind spot
|
|
where production failures hide.
|
|
\end{abstract}
|
|
|
|
\tableofcontents
|
|
\newpage
|
|
|
|
%% ============================================================
|
|
|
|
\input{sections/01-the-testing-pyramid-for-distributed-syst}
|
|
\input{sections/02-layer-1-unit-tests}
|
|
\input{sections/03-layer-2-integration-tests}
|
|
\input{sections/04-layer-3-property-based-and-fuzz-tests}
|
|
\input{sections/05-layer-4-end-to-end-tests}
|
|
\input{sections/06-layer-5-fault-injection-jepsen-style-tes}
|
|
\input{sections/07-layer-6-model-checking-tla}
|
|
\input{sections/08-layer-7-formal-proofs-lean-4}
|
|
\input{sections/09-our-testing-stack-by-the-numbers}
|
|
\input{sections/10-how-to-find-bugs-that-only-appear-under-}
|
|
\input{sections/11-practical-advice}
|
|
\input{sections/99-conclusion}
|
|
|
|
\end{document}
|