mirror of
https://github.com/hanzoai/papers.git
synced 2026-11-03 02:27:30 +00:00
zeekay
f9db4f5737
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.
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{
|
|
Hanzo AI Research \\
|
|
\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}
|