mirror of
https://github.com/hanzoai/papers.git
synced 2026-10-30 14:58:42 +00:00
zeekay
277439999d
Lux Partners Limited is the Isle of Man company and does not appear on a public surface. Lux Industries Inc, a Delaware C corporation, is the one these copyright lines, citations and terms name. Lines binding the name to another legal fact — a domicile, a signed counterparty, a quoted third-party article — are left alone, because renaming those would falsify a record rather than correct one.
74 lines
2.6 KiB
TeX
74 lines
2.6 KiB
TeX
\section{Conclusion}
|
|
|
|
\label{sec:conclusion}
|
|
% ============================================================================
|
|
|
|
The Hanzo formal verification suite provides mechanically-checked proofs of
|
|
173 critical properties across five infrastructure systems. The formalization
|
|
effort discovered 8 bugs undetected by testing, including a permission
|
|
escalation via revocation race, a path traversal in route matching, and a
|
|
rolling update failure mode leaving zero healthy replicas. All 12,000 lines of
|
|
Lean 4 proofs are checked by the Lean kernel with no \texttt{sorry} axioms,
|
|
providing mathematical certainty that the specified properties hold. The proof
|
|
suite runs in CI in 47 seconds, ensuring that specification changes are
|
|
continuously verified.
|
|
|
|
% ============================================================================
|
|
% BIBLIOGRAPHY
|
|
% ============================================================================
|
|
\begin{thebibliography}{15}
|
|
|
|
\bibitem{hanzoagentsdk}
|
|
{Hanzo AI Research}.
|
|
\newblock Hanzo Agent {SDK}: Framework for building {AI} agents.
|
|
\newblock \emph{Hanzo AI Research}, 2025.
|
|
|
|
\bibitem{hanzogateway}
|
|
{Hanzo AI Research}.
|
|
\newblock Hanzo Gateway: {API} gateway with {KrakenD} backend.
|
|
\newblock \emph{Hanzo AI Research}, 2024.
|
|
|
|
\bibitem{hanzokms}
|
|
{Hanzo AI Research}.
|
|
\newblock Hanzo {KMS}: Secrets management with per-environment rotation and audit trail.
|
|
\newblock \emph{Hanzo AI Research}, September 2021.
|
|
|
|
\bibitem{hanzoaci}
|
|
{Hanzo AI Research}.
|
|
\newblock Hanzo {ACI}: {AI} Chain Infrastructure for decentralized compute markets.
|
|
\newblock \emph{Hanzo AI Research}, December 2024.
|
|
|
|
\bibitem{hanzoiam}
|
|
{Hanzo AI Research}.
|
|
\newblock Hanzo {IAM}: Identity and access management for {AI} platforms.
|
|
\newblock \emph{Hanzo AI Research}, 2024.
|
|
|
|
\bibitem{luxwhitepaper}
|
|
{Lux Industries Inc}.
|
|
\newblock Lux: A scalable multi-consensus blockchain with post-quantum cryptography.
|
|
\newblock \emph{Lux Network Technical Report}, 2024.
|
|
|
|
\bibitem{lean4}
|
|
L.~de~Moura and S.~Ullrich.
|
|
\newblock The {Lean 4} theorem prover and programming language.
|
|
\newblock In \emph{Proc.\ CADE}, 2021.
|
|
|
|
\bibitem{sel4}
|
|
G.~Klein, K.~Elphinstone, G.~Heiser, et~al.
|
|
\newblock {seL4}: Formal verification of an {OS} kernel.
|
|
\newblock In \emph{Proc.\ SOSP}, 2009.
|
|
|
|
\bibitem{compcert}
|
|
X.~Leroy.
|
|
\newblock Formal verification of a realistic compiler.
|
|
\newblock \emph{Commun.\ ACM}, 52(7):107--115, 2009.
|
|
|
|
\bibitem{ironfleet}
|
|
C.~Hawblitzel, J.~Howell, M.~Kapritsos, J.~R.~Lorch, B.~Parno, M.~L.~Roberts,
|
|
S.~Setty, and B.~Zill.
|
|
\newblock {IronFleet}: Proving practical distributed systems correct.
|
|
\newblock In \emph{Proc.\ SOSP}, 2015.
|
|
|
|
\end{thebibliography}
|
|
|