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.
111 lines
3.4 KiB
TeX
111 lines
3.4 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}
|
||
\usepackage{listingsutf8}
|
||
\input{../shared/lstlang}
|
||
\usepackage{xcolor}
|
||
\usepackage{enumitem}
|
||
\usepackage{float}
|
||
|
||
\newtheorem{theorem}{Theorem}
|
||
\newtheorem{lemma}[theorem]{Lemma}
|
||
\newtheorem{proposition}[theorem]{Proposition}
|
||
\newtheorem{definition}{Definition}
|
||
\newtheorem{corollary}[theorem]{Corollary}
|
||
\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},
|
||
extendedchars=true,
|
||
inputencoding=utf8,
|
||
literate=%
|
||
{×}{{$\times$}}1
|
||
{→}{{$\to$}}1
|
||
{←}{{$\leftarrow$}}1
|
||
{≥}{{$\geq$}}1
|
||
{≤}{{$\leq$}}1
|
||
{μ}{{$\mu$}}1
|
||
{►}{{\ensuremath{\blacktriangleright}}}1
|
||
{✓}{{\ensuremath{\checkmark}}}1
|
||
{✅}{{\ensuremath{\checkmark}}}1
|
||
{—}{{--}}1
|
||
{–}{{-}}1
|
||
{¬}{{\ensuremath{\neg}}}1
|
||
{·}{{\ensuremath{\cdot}}}1
|
||
{∀}{{\ensuremath{\forall}}}1
|
||
{∃}{{\ensuremath{\exists}}}1
|
||
{∈}{{\ensuremath{\in}}}1
|
||
{∉}{{\ensuremath{\notin}}}1
|
||
{∧}{{\ensuremath{\wedge}}}1
|
||
{∨}{{\ensuremath{\vee}}}1
|
||
{∩}{{\ensuremath{\cap}}}1
|
||
{≠}{{\ensuremath{\neq}}}1
|
||
{⟨}{{\ensuremath{\langle}}}1
|
||
{⟩}{{\ensuremath{\rangle}}}1
|
||
}
|
||
|
||
\hypersetup{
|
||
colorlinks=true,
|
||
linkcolor=blue,
|
||
citecolor=blue,
|
||
urlcolor=blue
|
||
}
|
||
|
||
\title{Formal Verification with Lean~4 for Blockchain Systems}
|
||
\author{
|
||
Lux Research \\
|
||
Lux Industries, Inc.\thanks{Corresponding author: [email protected]}\\
|
||
\texttt{[email protected]}
|
||
}
|
||
\date{2025}
|
||
|
||
\begin{document}
|
||
|
||
\luxcoverpage
|
||
|
||
\begin{abstract}
|
||
Formal verification provides mathematical certainty that software satisfies its specification.
|
||
This paper teaches formal verification from first principles using Lean~4, a dependently typed
|
||
proof assistant and programming language developed at Microsoft Research. We cover the
|
||
foundations---propositions as types, tactics, induction---then apply them to blockchain-specific
|
||
problems: consensus safety and liveness, BFT threshold arithmetic, and cryptographic
|
||
primitive correctness. We present 384 machine-checked theorems with zero uses of
|
||
\texttt{sorry} (Lean's axiom-of-trust escape hatch), covering Lux Network's Quasar
|
||
consensus, BLS signature aggregation, and post-quantum threshold schemes. Every proof
|
||
compiles with \texttt{lake build} and is maintained in \texttt{luxfi/formal}. This is a
|
||
builder's guide: each concept is followed by working Lean~4 code that the reader can type,
|
||
compile, and modify.
|
||
\end{abstract}
|
||
|
||
\tableofcontents
|
||
\newpage
|
||
|
||
%% ============================================================
|
||
|
||
\input{sections/01-why-formal-verification}
|
||
\input{sections/02-lean-4-fundamentals}
|
||
\input{sections/03-modeling-consensus-in-lean-4}
|
||
\input{sections/04-induction-on-chain-height}
|
||
\input{sections/05-bft-threshold-proofs}
|
||
\input{sections/06-cryptographic-primitive-verification}
|
||
\input{sections/07-our-proof-corpus-384-theorems-0-sorry}
|
||
\input{sections/08-practical-guide-writing-your-first-block}
|
||
\input{sections/09-common-patterns}
|
||
\input{sections/10-lessons-learned}
|
||
\input{sections/99-conclusion}
|
||
|
||
\end{document}
|