mirror of
https://github.com/hanzoai/papers.git
synced 2026-11-03 02:27:30 +00:00
zeekay
0d1d121451
Fix shared/ include paths to ../shared/ for 55 subdirectory papers so
that hanzocover.sty and lstlang.tex resolve when building from each
paper's own directory (the build pattern used by latexmk per paper).
Build fixes:
- hanzo-operative/sections/03-screen-understanding-pipeline.tex: move
\COMMENT from after \FOR{...} onto the \STATE line so the algorithmic
env doesn't mis-parse.
- hanzo-network-architecture (abstract + sections 04, 12, 13): escape
unicode mu (U+03BC) as $\mu$ for pdflatex.
- ntt-transform/sections/08-benchmark-results.tex: same mu escape.
All 55 Tier-2/3 papers now build clean with latexmk -pdf.
87 lines
3.1 KiB
TeX
87 lines
3.1 KiB
TeX
% Hanzo Formal Verification: Proving Infrastructure Correctness with Lean 4
|
|
\documentclass[11pt]{article}
|
|
\usepackage{../shared/hanzocover}
|
|
\usepackage{amsmath, amssymb, amsthm}
|
|
\usepackage{mathtools}
|
|
\usepackage{bm}
|
|
\usepackage{graphicx}
|
|
\usepackage{booktabs}
|
|
\usepackage{hyperref}
|
|
\usepackage{enumitem}
|
|
\usepackage{xcolor}
|
|
\usepackage{float}
|
|
\usepackage{multirow}
|
|
\usepackage{listings}
|
|
|
|
\hypersetup{colorlinks=true,linkcolor=black,citecolor=blue,urlcolor=blue}
|
|
|
|
\lstset{
|
|
basicstyle=\ttfamily\small,
|
|
breaklines=true,
|
|
frame=single,
|
|
numbers=left,
|
|
numberstyle=\tiny,
|
|
xleftmargin=2em,
|
|
language=Haskell,
|
|
morekeywords={theorem,lemma,def,structure,where,instance,namespace,section,
|
|
variable,axiom,inductive,noncomputable,sorry,have,show,by,exact,intro,
|
|
apply,simp,omega,decide,rfl},
|
|
}
|
|
|
|
\newtheorem{theorem}{Theorem}
|
|
\newtheorem{lemma}[theorem]{Lemma}
|
|
\newtheorem{proposition}[theorem]{Proposition}
|
|
\newtheorem{corollary}[theorem]{Corollary}
|
|
\newtheorem{definition}{Definition}
|
|
\newtheorem{remark}{Remark}
|
|
|
|
\title{HANZO FORMAL VERIFICATION\\[0.3em]
|
|
{\large Proving Infrastructure Correctness\\with Lean 4}}
|
|
\author{
|
|
Zach Kelling \\
|
|
\textit{Hanzo Industries Inc (Techstars '17)} \\
|
|
\texttt{[email protected]}
|
|
}
|
|
\date{March 2026}
|
|
|
|
\begin{document}
|
|
|
|
\hanzocoverpage
|
|
|
|
% ============================================================================
|
|
% ABSTRACT
|
|
% ============================================================================
|
|
\begin{abstract}
|
|
We present the formal verification suite for Hanzo infrastructure, comprising
|
|
over 12,000 lines of Lean 4 proofs covering critical correctness and security
|
|
properties of five core systems: (i)~the agent framework, proving safe
|
|
delegation, permission bound propagation, and credential chain validity,
|
|
(ii)~the API gateway, proving request routing correctness, rate limiter
|
|
fairness, and authentication chain soundness, (iii)~KMS secrets management,
|
|
proving envelope encryption correctness, key rotation safety (no secret exposure
|
|
during rotation), and access control policy consistency, (iv)~the compute
|
|
scheduler, proving resource allocation fairness, deadlock freedom, and SLA
|
|
compliance bounds, and (v)~the platform orchestrator, proving deployment state
|
|
machine correctness, rollback safety, and health check liveness. Each proof
|
|
is mechanically verified by the Lean 4 kernel---no axioms beyond the Lean
|
|
standard library are assumed. We describe the verification methodology,
|
|
present the key theorems and their proof structures, and report on the 8 bugs
|
|
discovered during formalization that were present in the production codebase
|
|
but undetected by testing.
|
|
\end{abstract}
|
|
|
|
% ============================================================================
|
|
|
|
\input{sections/01-introduction}
|
|
\input{sections/02-proof-suite-overview}
|
|
\input{sections/03-agent-framework-verification}
|
|
\input{sections/04-api-gateway-verification}
|
|
\input{sections/05-kms-secrets-verification}
|
|
\input{sections/06-compute-scheduler-verification}
|
|
\input{sections/07-platform-orchestrator-verification}
|
|
\input{sections/08-proof-engineering}
|
|
\input{sections/09-related-work}
|
|
\input{sections/99-conclusion}
|
|
|
|
\end{document}
|