mirror of
https://github.com/hanzoai/papers.git
synced 2026-10-30 14:58:42 +00:00
24 lines
1021 B
TeX
24 lines
1021 B
TeX
\section{Related Work}
|
|
|
|
\label{sec:related}
|
|
% ============================================================================
|
|
|
|
\textbf{seL4}~\cite{sel4} verified an OS microkernel with 200,000 lines of
|
|
Isabelle/HOL proofs. Our scope is narrower (infrastructure properties, not
|
|
kernel correctness) but covers more systems.
|
|
|
|
\textbf{CompCert}~\cite{compcert} verified a C compiler in Coq. We verify at
|
|
the specification level rather than implementation level, trading completeness
|
|
for broader coverage.
|
|
|
|
\textbf{IronFleet}~\cite{ironfleet} verified distributed systems (Paxos, a
|
|
sharded KV store) in Dafny. Our work addresses AI-specific properties (agent
|
|
delegation, inference scheduling) not present in traditional distributed
|
|
systems.
|
|
|
|
\textbf{Lux Network}~\cite{luxwhitepaper} has its own formal verification
|
|
suite for consensus properties. Our proofs complement the Lux proofs by
|
|
verifying the application-layer infrastructure built on top.
|
|
|
|
% ============================================================================
|